Skip to content

Commit 81d6878

Browse files
Ruben-VandeVeldeRuben-VandeVelde
committed
chore: tidy various files (#13056)
1 parent 3e4f4e9 commit 81d6878

File tree

24 files changed

+97
-113
lines changed

24 files changed

+97
-113
lines changed

‎Mathlib/Algebra/Exact.lean

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,10 @@ import Mathlib.Algebra.Module.Submodule.Range
1010
/-! # Exactness of a pair
1111
1212
* For two maps `f : M → N` and `g : N → P`, with `Zero P`,
13-
`Function.AddExact f g` says that `Set.range f = Set.preimage {0}
14-
15-
* For two maps `f : M → N` and `g : N → P`, with `One P`,
16-
`Function.Exact f g` says that `Set.range f = Set.preimage {1}
13+
`Function.Exact f g` says that `Set.range f = Set.preimage g {0}`
1714
1815
* For linear maps `f : M →ₗ[R] N` and `g : N →ₗ[R] P`,
19-
`Exact f g` says that `range f = ker g``
16+
`Exact f g` says that `range f = ker g`
2017
2118
## TODO :
2219

‎Mathlib/Algebra/Module/Injective.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -454,7 +454,7 @@ theorem extension_property_addMonoidHom (h : Module.Baer ℤ Q)
454454
/-- **Baer's criterion** for injective module : a Baer module is an injective module, i.e. if every
455455
linear map from an ideal can be extended, then the module is injective. -/
456456
protected theorem injective (h : Module.Baer R Q) : Module.Injective R Q where
457-
out := fun X Y _ _ _ _ i hi f ↦ by
457+
out X Y _ _ _ _ i hi f := by
458458
obtain ⟨h, H⟩ := Module.Baer.extension_property h i hi f
459459
exact ⟨h, DFunLike.congr_fun H⟩
460460
set_option linter.uppercaseLean3 false in
@@ -466,7 +466,7 @@ protected theorem of_injective [Small.{v} R] (inj : Module.Injective R Q) : Modu
466466
let eR := Shrink.linearEquiv R R
467467
obtain ⟨g', hg'⟩ := Module.Injective.out (eR.symm.toLinearMap ∘ₗ I.subtype ∘ₗ eI.toLinearMap)
468468
(eR.symm.injective.comp <| Subtype.val_injective.comp eI.injective) (g ∘ₗ eI.toLinearMap)
469-
exact ⟨g' ∘ₗ eR.symm.toLinearMap, fun x mx ↦ by simpa [eI,eR] using hg' (equivShrink I ⟨x, mx⟩)⟩
469+
exact ⟨g' ∘ₗ eR.symm.toLinearMap, fun x mx ↦ by simpa [eI, eR] using hg' (equivShrink I ⟨x, mx⟩)⟩
470470

471471
protected theorem iff_injective [Small.{v} R] : Module.Baer R Q ↔ Module.Injective R Q :=
472472
⟨Module.Baer.injective, Module.Baer.of_injective⟩

‎Mathlib/Algebra/Order/Hom/Monoid.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ This file used to define typeclasses for order-preserving (additive) monoid homo
4747
`OrderAddMonoidHomClass`, `OrderMonoidHomClass`, and `OrderMonoidWithZeroHomClass`.
4848
4949
In #10544 we migrated from these typeclasses
50-
to assumptions like `[FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N ]`,
50+
to assumptions like `[FunLike F M N] [MonoidHomClass F M N] [OrderHomClass F M N]`,
5151
making some definitions and lemmas irrelevant.
5252
5353
## Tags

‎Mathlib/Algebra/Polynomial/Div.lean

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -559,8 +559,8 @@ theorem rootMultiplicity_C (r a : R) : rootMultiplicity a (C r) = 0 := by
559559
split_ifs with hr
560560
· rfl
561561
have h : natDegree (C r) < natDegree (X - C a) := by simp
562-
simp_rw [multiplicity.multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]
563-
rfl
562+
simp_rw [multiplicity.multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h),
563+
PartENat.get_zero]
564564
set_option linter.uppercaseLean3 false in
565565
#align polynomial.root_multiplicity_C Polynomial.rootMultiplicity_C
566566

@@ -614,12 +614,13 @@ set_option linter.uppercaseLean3 false in
614614
#align polynomial.mod_by_monic_X_sub_C_eq_C_eval Polynomial.modByMonic_X_sub_C_eq_C_eval
615615

616616
theorem mul_divByMonic_eq_iff_isRoot : (X - C a) * (p /ₘ (X - C a)) = p ↔ IsRoot p a :=
617-
⟨fun h => by
618-
rw [← h, IsRoot.def, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul],
619-
fun h : p.eval a = 0 => by
620-
conv_rhs =>
617+
.trans
618+
⟨fun h => by rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul],
619+
fun h => by
620+
conv_rhs =>
621621
rw [← modByMonic_add_div p (monic_X_sub_C a)]
622622
rw [modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]⟩
623+
IsRoot.def.symm
623624
#align polynomial.mul_div_by_monic_eq_iff_is_root Polynomial.mul_divByMonic_eq_iff_isRoot
624625

625626
theorem dvd_iff_isRoot : X - C a ∣ p ↔ IsRoot p a :=

‎Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -142,10 +142,8 @@ instance partialOrder : PartialOrder (Prepartition I) where
142142
fun π₁ π₂ h₁ h₂ => injective_boxes (Subset.antisymm (this h₁ h₂) (this h₂ h₁))
143143
intro π₁ π₂ h₁ h₂ J hJ
144144
rcases h₁ hJ with ⟨J', hJ', hle⟩; rcases h₂ hJ' with ⟨J'', hJ'', hle'⟩
145-
obtain rfl : J = J''
146-
· exact π₁.eq_of_le hJ hJ'' (hle.trans hle')
147-
obtain rfl : J' = J
148-
· exact le_antisymm ‹_› ‹_›
145+
obtain rfl : J = J'' := π₁.eq_of_le hJ hJ'' (hle.trans hle')
146+
obtain rfl : J' = J := le_antisymm ‹_› ‹_›
149147
assumption
150148

151149
instance : OrderTop (Prepartition I) where
@@ -539,9 +537,8 @@ theorem restrict_biUnion (πi : ∀ J, Prepartition J) (hJ : J ∈ π) :
539537
exact WithBot.coe_le_coe.2 (le_of_mem _ h₁)
540538
· simp only [iUnion_restrict, iUnion_biUnion, Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion]
541539
rintro x ⟨hxJ, J₁, h₁, hx⟩
542-
obtain rfl : J = J₁
543-
· exact π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)
544-
· exact hx
540+
obtain rfl : J = J₁ := π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)
541+
exact hx
545542
#align box_integral.prepartition.restrict_bUnion BoxIntegral.Prepartition.restrict_biUnion
546543

547544
theorem biUnion_le_iff {πi : ∀ J, Prepartition J} {π' : Prepartition I} :

‎Mathlib/CategoryTheory/EffectiveEpi/Enough.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,9 +62,9 @@ instance (X : D) : EffectiveEpi (F.effectiveEpiOver X) :=
6262
/-- An effective presentation of an object with respect to an equivalence of categories. -/
6363
def equivalenceEffectivePresentation (e : C ≌ D) (X : D) :
6464
EffectivePresentation e.functor X where
65-
p := e.inverse.obj X
66-
f := e.counit.app _
67-
effectiveEpi := inferInstance
65+
p := e.inverse.obj X
66+
f := e.counit.app _
67+
effectiveEpi := inferInstance
6868

6969
instance [IsEquivalence F] : EffectivelyEnough F where
7070
presentation X := ⟨equivalenceEffectivePresentation F.asEquivalence X⟩

‎Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -64,8 +64,9 @@ The coherent sheaf condition on an essentially small site can be checked after p
6464
the equivalence with a small category.
6565
-/
6666
theorem precoherent_isSheaf_iff_of_essentiallySmall [EssentiallySmall C] (F : Cᵒᵖ ⥤ A) :
67-
IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology (SmallModel C))
68-
((equivSmallModel C).inverse.op ⋙ F) := precoherent_isSheaf_iff _ _ _
67+
IsSheaf (coherentTopology C) F ↔
68+
IsSheaf (coherentTopology (SmallModel C)) ((equivSmallModel C).inverse.op ⋙ F) :=
69+
precoherent_isSheaf_iff _ _ _
6970

7071
end Coherent
7172

‎Mathlib/Data/Finset/Sigma.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -110,8 +110,8 @@ theorem inf_sigma [SemilatticeInf β] [OrderTop β] :
110110
#align finset.inf_sigma Finset.inf_sigma
111111

112112
theorem _root_.biSup_finsetSigma [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i))
113-
(f : Sigma α → β) : ⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ :=
114-
by simp_rw [← Finset.iSup_coe, Finset.coe_sigma, biSup_sigma]
113+
(f : Sigma α → β) : ⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ := by
114+
simp_rw [← Finset.iSup_coe, Finset.coe_sigma, biSup_sigma]
115115

116116
theorem _root_.biSup_finsetSigma' [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i))
117117
(f : ∀ i, α i → β) : ⨆ (i ∈ s) (j ∈ t i), f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd :=

‎Mathlib/Data/Nat/Interval.lean

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -118,11 +118,9 @@ theorem card_Ioo : (Ioo a b).card = b - a - 1 :=
118118

119119
@[simp]
120120
theorem card_uIcc : (uIcc a b).card = (b - a : ℤ).natAbs + 1 := by
121-
refine' (card_Icc _ _).trans (Int.ofNat.inj _)
122-
change ((↑) : ℕ → ℤ) _ = _
121+
refine (card_Icc _ _).trans (Int.natCast_inj.mp ?_)
123122
rw [sup_eq_max, inf_eq_min, Int.ofNat_sub]
124-
· change _ = ↑(Int.natAbs (b - a) + 1)
125-
omega
123+
· omega
126124
· exact min_le_max.trans le_self_add
127125
#align nat.card_uIcc Nat.card_uIcc
128126

‎Mathlib/Data/Real/ConjExponents.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -197,8 +197,8 @@ lemma mul_eq_add : p * q = p + q := by
197197
@[symm]
198198
protected lemma symm : q.IsConjExponent p where
199199
one_lt := by
200-
rw [h.conj_eq]
201-
exact (one_lt_div h.sub_one_pos).mpr (tsub_lt_self h.pos zero_lt_one)
200+
rw [h.conj_eq]
201+
exact (one_lt_div h.sub_one_pos).mpr (tsub_lt_self h.pos zero_lt_one)
202202
inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
203203

204204
lemma div_conj_eq_sub_one : p / q = p - 1 := by field_simp [h.symm.ne_zero]; rw [h.sub_one_mul_conj]

0 commit comments

Comments
 (0)