mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case pos
ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
⊢ f.f (c.next i) =
    K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

Tactic:
rw [ho.comm (c.next i)]

Goal state after:
case pos
ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
⊢ (dNext (c.next i)) ho.hom + (prevD (c.next i)) ho.hom + g.f (c.next i) =
    K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
⊢ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map (r • (quotient C (ComplexShape.up ℤ)).map f) =
    r • (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)

Tactic:
have h₁ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) f

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ quotient C (ComplexShape.up ℤ)).map f ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map f
⊢ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map (r • (quotient C (ComplexShape.up ℤ)).map f) =
    r • (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (-γ).rightUnshift n hn = -γ.rightUnshift n hn

Tactic:
by
  change (rightShiftAddEquiv K L n a n' hn).symm (-γ) = _
  apply map_neg

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq

Tactic:
(γ.comp γ' hnm).rightUnshift_v nm' hnm' p q hpq (p + n + m) (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
⊢ (γ.comp γ' hnm).v p (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
f : T₁ ⟶ T₂
⊢ f + 0 = f

Tactic:
ext <;> apply add_zero

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F₁.CommShift A
inst✝¹ : F₂.CommShift A
inst✝ : CommShift τ A
a : A
⊢ (Functor.commShiftIso F₁ a).hom ≫ Functor.whiskerRight τ (shiftFunctor D a) =
    (shiftFunctor C a).whiskerLeft τ ≫ (Functor.commShiftIso F₂ a).hom

Tactic:
by
  apply CommShift.shift_comm

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
have hnm' : n' + 1 = m' := by lia
    ext p q hpq
    dsimp
    rw [(δ n m γ).rightShift_v a m' hm' p q hpq _ rfl,
      δ_v n m hnm _ p (p + m) rfl (p + n) (p + 1) (by lia) rfl,
      δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by lia) rfl,
      γ.rightShift_v a n' hn' p (p + n') rfl (p + n) rfl,
      γ.rightShift_v a n' hn' (p + 1) q _ (p + m) (by lia)]
    simp only [shiftFunctorObjXIso, shiftFunctor_obj_d',
      Linear.comp_units_smul, assoc, HomologicalComplex.XIsoOfEq_inv_comp_d,
      add_comp, HomologicalComplex.d_comp_XIsoOfEq_inv, Linear.units_smul_comp, smul_add,
      add_right_inj, smul_smul]
    simp only [← hm', add_comm m', Int.negOnePow_add, ← mul_assoc,
      Int.units_mul_self, one_mul]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ≅ (contractibleTriangle X).invRotate

Tactic:
exact Triangle.isoMk _ _ (Functor.mapZeroObject _).symm (Iso.refl _) (Iso.refl _)
    (by simp) (by simp) (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : Epi f
Z : C
g : Y✝ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X✝
hT : Triangle.mk f g h ∈ distinguishedTriangles
⊢ 𝟙 (Triangle.mk f g h).obj₂ ≫ (Triangle.mk f g h).mor₂ = 0

Tactic:
Triangle.mor₂_eq_zero_of_epi₁ _ hT hf,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : Epi f
Z : C
g : Y✝ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X✝
hT : Triangle.mk f g h ∈ distinguishedTriangles
⊢ 𝟙 (Triangle.mk f g h).obj₂ ≫ 0 = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ (triangleh φ₁).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ (triangleh φ₂).mor₃

Tactic:
dsimp
    rw [← Functor.map_comp_assoc, triangleMapOfHomotopy_comm₃, Functor.map_comp, assoc, assoc]
    simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ

Tactic:
ext p
  dsimp [rotateHomotopyEquiv]
  -- the following list of lemmas has been obtained by doing
  -- simp? [lift_f _ _ _ _ _ (p + 1) rfl,
  --   (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by lia)]
  simp only [Int.reduceNeg, lift_f _ _ _ _ _ (p + 1) rfl, shiftFunctor_obj_X', Cocycle.coe_neg,
    Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.neg_v,
    (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by lia), mul_one,
      sub_self, mul_zero, Int.zero_ediv, add_zero, Int.negOnePow_one,
    shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Cochain.ofHom_v, id_comp,
    Units.neg_smul, one_smul, neg_neg, Preadditive.neg_comp, Preadditive.add_comp, assoc,
    inl_v_triangle_mor₃_f, Iso.refl_inv, Preadditive.comp_neg, comp_id, inr_f_triangle_mor₃_f,
    comp_zero, neg_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
⊢ T₁ ≅ T₂

Tactic:
have h := exists_iso_of_arrow_iso T₁ T₂ hT₁ hT₂ (Arrow.isoMk e₁ e₂ comm.symm)
  exact Triangle.isoMk _ _ e₁ e₂ (Triangle.π₃.mapIso h.choose) comm (by
    have eq := h.choose_spec.2
    dsimp at eq ⊢
    conv_rhs => rw [← eq, ← TriangleMorphism.comm₂]) (by
    have eq := h.choose_spec.1
    dsimp at eq ⊢
    conv_lhs => rw [← eq, TriangleMorphism.comm₃])

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
⊢ ∀ {v₂₃ : Y₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles)
    {v₁₃ : Y₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles),
    Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
v₂₃

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Y₃ ⟶ Z₂₃
⊢ ∀ {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃}
    {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles),
    Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
G : Type u_5
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ (F.shiftIso n a' a ⋯).hom.app X ≫ F.shiftMap f a a' ha' =
    (F.shift a').map ((shiftFunctor C n).map f ≫ (shiftFunctorCompIsoId C m n ⋯).hom.app Y)

Tactic:
by
  have hnm' : m + n = 0 := by
    rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
  simp [F.shiftIso_hom_app_comp_shiftMap f n 0 hnm' a' a, shiftIso_zero_hom_app,
    shiftFunctorCompIsoId]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G✝ : C ⥤ D
hG : W.IsInvertedBy G✝
G : W.FunctorsInverting D
⊢ 𝟙 W.Q ◫ natTransExtension (eqToHom ⋯ ≫ (𝟙 G).hom ≫ eqToHom ⋯) = 𝟙 W.Q ◫ 𝟙 (lift G.obj ⋯)

Tactic:
rw [natTransExtension_hcomp]

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G✝ : C ⥤ D
hG : W.IsInvertedBy G✝
G : W.FunctorsInverting D
⊢ eqToHom ⋯ ≫ (𝟙 G).hom ≫ eqToHom ⋯ = 𝟙 W.Q ◫ 𝟙 (lift G.obj ⋯)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
⊢ LeftFraction₂Rel φ ψ

Tactic:
obtain ⟨Z''', u', hu', fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ ψ.hs hα'

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac' : (t₂ ≫ α.f ≫ u) ≫ u' = (t₂' ≫ α.s ≫ u) ≫ u'
⊢ LeftFraction₂Rel φ ψ
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
inst✝² : Preadditive D
inst✝¹ : L.Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
T : Triangle D
T' : Triangle C
e' : T.rotate ≅ L.mapTriangle.obj T'
hT' : T' ∈ distinguishedTriangles
⊢ T ∈ L.essImageDistTriang

Tactic:
exact ⟨T'.invRotate, (triangleRotation D).unitIso.app T ≪≫ (invRotate D).mapIso e' ≪≫
      L.mapTriangleInvRotateIso.app T', inv_rot_of_distTriang T' hT'⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv = (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv

Tactic:
← cancel_epi (G.map (L.objObjPreimageIso X).hom),

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
this : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ
⊢ Function.Surjective (Sum.elim (fun x ↦ ⟨↑x, ⋯⟩) fun x ↦ ⟨↑x, ⋯⟩)

Tactic:
rintro ⟨x, hx | hx⟩

Goal state after:
case inl
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
this : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ
x : X
hx : P₁ x
⊢ ∃ a, Sum.elim (fun x ↦ ⟨↑x, ⋯⟩) (fun x ↦ ⟨↑x, ⋯⟩) a = ⟨x, ⋯⟩

case inr
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
this : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ
x : X
hx : P₂ x
⊢ ∃ a, Sum.elim (fun x ↦ ⟨↑x, ⋯⟩) (fun x ↦ ⟨↑x, ⋯⟩) a = ⟨x, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
i : ULift.{max v w, u} ι
⊢ HasCardinalLT (ULift.{max u w, v} (α i.down)) (Cardinal.lift.{max u v, w} κ)

Tactic:
by simpa using hα (ULift.down i)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
⊢ Cardinal.mk (Shrink.{w, u'} (J a)) < κ

Tactic:
← hasCardinalLT_iff_cardinal_mk_lt _ κ,

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
⊢ HasCardinalLT (Shrink.{w, u'} (J a)) κ
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.IsStableUnderShift A
⊢ P.shiftClosure A = P

Tactic:
by
  refine le_antisymm ?_ P.le_shiftClosure
  rintro X ⟨Y, a, i, hY⟩
  exact P.prop_of_iso i.symm (P.le_shift a Y hY)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteProducts C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
⊢ P.IsClosedUnderFiniteProducts

Tactic:
have := IsClosedUnderBinaryProducts.closedUnderIsomorphisms P
  have := hasFiniteProducts_of_has_binary_and_terminal (C := P.FullSubcategory)
  have := PreservesFiniteProducts.of_preserves_binary_and_terminal P.ι
  exact ⟨fun J _ ↦ P.isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι _⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ : MorphismProperty C
⊢ ∀ ⦃b : MorphismProperty C⦄, a✝ ≤ b → a✝.retracts ≤ b.retracts

Tactic:
_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
⊢ a✝ ≤ b✝ → a✝.retracts ≤ b✝.retracts
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
⊢ a✝.retracts ≤ b✝.retracts

Tactic:
_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), a✝.retracts f → b✝.retracts f
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), a✝.retracts f → b✝.retracts f

Tactic:
_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), a✝.retracts f → b✝.retracts f
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), a✝.retracts f → b✝.retracts f

Tactic:
_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ a✝.retracts f✝ → b✝.retracts f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f
⊢ P.retracts ≤ P

Tactic:
X

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.retracts f → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
⊢ ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ : C
⊢ ∀ {Y Z W : C} {f : X✝ ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ : C
⊢ ∀ {Y Z W : C} {f : X✝ ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f

Tactic:
_

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ : C
⊢ ∀ {Z W : C} {f : X✝ ⟶ Y✝} {g : Z ⟶ W} (h : RetractArrow f g), P g → P f