Skip to content

Commit

Permalink
chore: fix align linebreaks (#3127)
Browse files Browse the repository at this point in the history
Same as #3103, I missed those before, probably because I didn't rebase on HEAD before. This shouldnow include all cases of aligns with linebreak.

```
find . -type f -name "*.lean" -exec sed -i -E 'N;s/^#align ([^[:space:]]+)\n *([^[:space:]]+)$/#align \1 \2/' {} \;
```


Co-authored-by: Moritz Firsching <firsching@google.com>
  • Loading branch information
mo271 and mo271 committed Mar 27, 2023
1 parent de17926 commit da32edd
Show file tree
Hide file tree
Showing 5 changed files with 53 additions and 106 deletions.
6 changes: 2 additions & 4 deletions Mathlib/Algebra/CharZero/Quotient.lean
Expand Up @@ -68,15 +68,13 @@ theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {
QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz

#align quotient_add_group.zmultiples_zsmul_eq_zsmul_iff
quotientAddGroup.zmultiples_zsmul_eq_zsmul_iff
#align quotient_add_group.zmultiples_zsmul_eq_zsmul_iff quotientAddGroup.zmultiples_zsmul_eq_zsmul_iff

theorem zmultiples_nsmul_eq_nsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {n : ℕ} (hz : n ≠ 0) :
n • ψ = n • θ ↔ ∃ k : Fin n, ψ = θ + (k : ℕ) • (p / n : R) := by
rw [← coe_nat_zsmul ψ, ← coe_nat_zsmul θ,
zmultiples_zsmul_eq_zsmul_iff (Int.coe_nat_ne_zero.mpr hz), Int.cast_ofNat]
rfl
#align quotient_add_group.zmultiples_nsmul_eq_nsmul_iff
quotientAddGroup.zmultiples_nsmul_eq_nsmul_iff
#align quotient_add_group.zmultiples_nsmul_eq_nsmul_iff quotientAddGroup.zmultiples_nsmul_eq_nsmul_iff

end quotientAddGroup
3 changes: 1 addition & 2 deletions Mathlib/CategoryTheory/EssentiallySmall.lean
Expand Up @@ -124,8 +124,7 @@ instance (priority := 100) locallySmall_self (C : Type u) [Category.{v} C] : Loc
instance (priority := 100) locallySmall_of_essentiallySmall (C : Type u) [Category.{v} C]
[EssentiallySmall.{w} C] : LocallySmall.{w} C :=
(locallySmall_congr (equivSmallModel C)).mpr (CategoryTheory.locallySmall_self _)
#align category_theory.locally_small_of_essentially_small
CategoryTheory.locallySmall_of_essentiallySmall
#align category_theory.locally_small_of_essentially_small CategoryTheory.locallySmall_of_essentiallySmall

/-- We define a type alias `ShrinkHoms C` for `C`. When we have `LocallySmall.{w} C`,
we'll put a `Category.{w}` instance on `ShrinkHoms C`.
Expand Down
21 changes: 7 additions & 14 deletions Mathlib/CategoryTheory/Limits/ConeCategory.lean
Expand Up @@ -62,8 +62,7 @@ def Cone.fromCostructuredArrow (F : J ⥤ C) : CostructuredArrow (const J) F ⥤
convert congr_fun (congr_arg NatTrans.app f.w) j
dsimp
simp }
#align category_theory.limits.cone.from_costructured_arrow
CategoryTheory.Limits.Cone.fromCostructuredArrow
#align category_theory.limits.cone.from_costructured_arrow CategoryTheory.Limits.Cone.fromCostructuredArrow

/-
Porting note:
Expand All @@ -80,8 +79,7 @@ def Cone.equivCostructuredArrow (F : J ⥤ C) : Cone F ≌ CostructuredArrow (co
(NatIso.ofComponents Cones.eta (by aesop_cat))
(NatIso.ofComponents (fun c => (CostructuredArrow.eta _).symm)
(by intros ; apply CostructuredArrow.ext ; aesop_cat))
#align category_theory.limits.cone.equiv_costructured_arrow
CategoryTheory.Limits.Cone.equivCostructuredArrow
#align category_theory.limits.cone.equiv_costructured_arrow CategoryTheory.Limits.Cone.equivCostructuredArrow

/-- A cone is a limit cone iff it is terminal. -/
def Cone.isLimitEquivIsTerminal {F : J ⥤ C} (c : Cone F) : IsLimit c ≃ IsTerminal c :=
Expand All @@ -90,8 +88,7 @@ def Cone.isLimitEquivIsTerminal {F : J ⥤ C} (c : Cone F) : IsLimit c ≃ IsTer
invFun := fun h s => ⟨⟨IsTerminal.from h s⟩, fun a => IsTerminal.hom_ext h a _⟩
left_inv := by aesop_cat
right_inv := by aesop_cat }
#align category_theory.limits.cone.is_limit_equiv_is_terminal
CategoryTheory.Limits.Cone.isLimitEquivIsTerminal
#align category_theory.limits.cone.is_limit_equiv_is_terminal CategoryTheory.Limits.Cone.isLimitEquivIsTerminal

theorem hasLimit_iff_hasTerminal_cone (F : J ⥤ C) : HasLimit F ↔ HasTerminal (Cone F) :=
fun _ => (Cone.isLimitEquivIsTerminal _ (limit.isLimit F)).hasTerminal, fun h =>
Expand Down Expand Up @@ -121,8 +118,7 @@ theorem IsTerminal.from_eq_liftConeMorphism {F : J ⥤ C} {c : Cone F} (hc : IsT
(s : Cone F) :
IsTerminal.from hc s = ((Cone.isLimitEquivIsTerminal _).symm hc).liftConeMorphism s :=
(IsLimit.liftConeMorphism_eq_isTerminal_from (c.isLimitEquivIsTerminal.symm hc) s).symm
#align category_theory.limits.is_terminal.from_eq_lift_cone_morphism
CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism
#align category_theory.limits.is_terminal.from_eq_lift_cone_morphism CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism

/-- If `G : Cone F ⥤ Cone F'` preserves terminal objects, it preserves limit cones. -/
def IsLimit.ofPreservesConeTerminal {F : J ⥤ C} {F' : K ⥤ D} (G : Cone F ⥤ Cone F')
Expand All @@ -134,8 +130,7 @@ def IsLimit.ofPreservesConeTerminal {F : J ⥤ C} {F' : K ⥤ D} (G : Cone F ⥤
def IsLimit.ofReflectsConeTerminal {F : J ⥤ C} {F' : K ⥤ D} (G : Cone F ⥤ Cone F')
[ReflectsLimit (Functor.empty.{0} _) G] {c : Cone F} (hc : IsLimit (G.obj c)) : IsLimit c :=
(Cone.isLimitEquivIsTerminal _).symm <| (Cone.isLimitEquivIsTerminal _ hc).isTerminalOfObj _ _
#align category_theory.limits.is_limit.of_reflects_cone_terminal
CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal
#align category_theory.limits.is_limit.of_reflects_cone_terminal CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal

/-- Construct an object of the category `(F ↓ Δ)` from a cocone on `F`. This is part of an
equivalence, see `Cocone.equivStructuredArrow`. -/
Expand Down Expand Up @@ -214,16 +209,14 @@ theorem IsInitial.to_eq_descCoconeMorphism {F : J ⥤ C} {c : Cocone F} (hc : Is
(s : Cocone F) :
IsInitial.to hc s = ((Cocone.isColimitEquivIsInitial _).symm hc).descCoconeMorphism s :=
(IsColimit.descCoconeMorphism_eq_isInitial_to (c.isColimitEquivIsInitial.symm hc) s).symm
#align category_theory.limits.is_initial.to_eq_desc_cocone_morphism
CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism
#align category_theory.limits.is_initial.to_eq_desc_cocone_morphism CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism

/-- If `G : Cocone F ⥤ Cocone F'` preserves initial objects, it preserves colimit cocones. -/
def IsColimit.ofPreservesCoconeInitial {F : J ⥤ C} {F' : K ⥤ D} (G : Cocone F ⥤ Cocone F')
[PreservesColimit (Functor.empty.{0} _) G] {c : Cocone F} (hc : IsColimit c) :
IsColimit (G.obj c) :=
(Cocone.isColimitEquivIsInitial _).symm <| (Cocone.isColimitEquivIsInitial _ hc).isInitialObj _ _
#align category_theory.limits.is_colimit.of_preserves_cocone_initial
CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial
#align category_theory.limits.is_colimit.of_preserves_cocone_initial CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial

/-- If `G : Cocone F ⥤ Cocone F'` reflects initial objects, it reflects colimit cocones. -/
def IsColimit.ofReflectsCoconeInitial {F : J ⥤ C} {F' : K ⥤ D} (G : Cocone F ⥤ Cocone F')
Expand Down

0 comments on commit da32edd

Please sign in to comment.