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

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' = 0

Tactic:
K.d₂_eq_zero' c₁₂ i₁ h₂ i₁₂'

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ 0 = 0

case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) ≠ i₁₂'
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹³ : Category.{v_1, u_1} C₁
inst✝¹² : Category.{v_2, u_2} C₁'
inst✝¹¹ : Category.{v_3, u_3} C₂
inst✝¹⁰ : Category.{v_4, u_4} C₂'
inst✝⁹ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : HasShift C₁ M
inst✝⁶ : HasShift C₂ M
inst✝⁵ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₂
⊢ CommShift (flipApp (τ ≫ τ') x✝) M

Tactic:
simp only [flipApp, flipFunctor_obj, Functor.map_comp, comp_app]

Goal state after:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹³ : Category.{v_1, u_1} C₁
inst✝¹² : Category.{v_2, u_2} C₁'
inst✝¹¹ : Category.{v_3, u_3} C₂
inst✝¹⁰ : Category.{v_4, u_4} C₂'
inst✝⁹ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : HasShift C₁ M
inst✝⁶ : HasShift C₂ M
inst✝⁵ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₂
⊢ CommShift (((flipFunctor C₁ C₂ D).map τ).app x✝ ≫ ((flipFunctor C₁ C₂ D).map τ').app x✝) M
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : HasZeroMorphisms C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
x : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
n₁ n₂ n : ℤ
h : n₁ + n₂ = n
m₁ m : ℤ
hm₁ : m₁ = n₁ + x
hm : m = n + x
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).ιMapBifunctor K₂ F n₁ n₂ n h ≫
      (K₁.mapBifunctorShift₁Iso K₂ F x).hom.f n =
    (F.map (K₁.shiftFunctorObjXIso x n₁ m₁ hm₁).hom).app (K₂.X n₂) ≫
      K₁.ιMapBifunctor K₂ F m₁ n₂ m ⋯ ≫ ((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso x n m hm).inv

Tactic:
dsimp [mapBifunctorShift₁Iso]
  simp only [HomologicalComplex₂.ιTotal_map_assoc,
    HomologicalComplex₂.ι_totalShift₁Iso_hom_f _ _ _ _ _ _ _ hm₁ _ hm]
  simp [HomologicalComplex₂.ιTotal, HomologicalComplex₂.shiftFunctor₁XXIso,
    HomologicalComplex.XIsoOfEq, eqToHom_map]

Goal state after:
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ (PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd) ≫ biprod.fst =
    s.ι ≫ biprod.fst

Tactic:
simp only [assoc, biprod.lift_fst]

Goal state after:
case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ fst = s.ι ≫ biprod.fst
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit sq.kernelFork
s : PullbackCone f g
m : s.pt ⟶ X₁
hm₁ : m ≫ fst = s.fst
hm₂ : m ≫ snd = s.snd
⊢ m = h.lift (KernelFork.ofι (biprod.lift s.fst s.snd) ⋯)

Tactic:
apply Fork.IsLimit.hom_ext h
        convert!
          (h.fac (KernelFork.ofι (biprod.lift s.fst s.snd) (by simp [s.condition])) .zero).symm
        cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
k : ℕ
x : ↑(X k)
p q : ℤ
hpq : p + -1 = q
hp : p ≤ d + ↑k
⊢ (↑(φ k x)).v p q hpq = (↑x).v p q hpq

Tactic:
by
      dsimp [φ]
      rw [add_eq_left, Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ fibrations C (prod.map f₁ f₂)

Tactic:
apply MorphismProperty.limMap

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ (fibrations C).functorCategory (Discrete WalkingPair) (mapPair f₁ f₂)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
T : Triangle Cᵒᵖ
hT : T ∈ Pretriangulated.distinguishedTriangles
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
⊢ P.op.isoClosure T.obj₂

Tactic:
rw [mem_distTriang_op_iff] at hT
    obtain ⟨X, hX, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ hT h₃ h₁
    exact ⟨Opposite.op X, hX, ⟨e.symm.op⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ t.truncLE a = t.truncLT b

Tactic:
by rw [← h]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ t.truncGT a = t.truncGE b

Tactic:
by rw [← h]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₁Toπ₂ ≫ (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)).hom =
    (t.truncLEIsoTruncLT a b h).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₁Toπ₂

pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₂Toπ₃ ≫ (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom =
    (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₂Toπ₃

pp: case refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C 1) =
    (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁

Tactic:
· cat_disch

Goal state after:
case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₂Toπ₃ ≫ (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom =
    (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₂Toπ₃

case refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C 1) =
    (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₂Toπ₃ ≫ (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom =
    (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₂Toπ₃

pp: case refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C 1) =
    (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁

Tactic:
· cat_disch

Goal state after:
case refine_3
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C 1) =
    (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ ((singleFunctor C n).obj X).IsLE n

Tactic:
by
  rw [← isLE_ι_obj_iff]
  change DerivedCategory.TStructure.t.IsLE ((DerivedCategory.singleFunctor C n).obj X) n
  infer_instance

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

Goal state before:
pp: case mpr.refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₂ ≫
      (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₃).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₂).hom ≫
      (Triangle.mk f.hom a b).mor₂

pp: case mpr.refine_3
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₃ ≫
      (shiftFunctor C 1).map
        (Iso.refl
            (A.ι.mapTriangle.obj
                (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₁).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₃).hom ≫
      (Triangle.mk f.hom a b).mor₃

Tactic:
· cat_disch

Goal state after:
case mpr.refine_3
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₃ ≫
      (shiftFunctor C 1).map
        (Iso.refl
            (A.ι.mapTriangle.obj
                (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₁).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₃).hom ≫
      (Triangle.mk f.hom a b).mor₃
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : Category.{v_3, u_3} D₁
inst✝¹⁰ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : IsTriangulated C
inst✝³ : A.IsTriangulated
inst✝² : B.IsTriangulated
inst✝¹ : B.IsClosedUnderIsomorphisms
inst✝ : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this✝ : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
⊢ (B.op.inverseImage A.op.ι).trW.IsInvertedBy (A.opEquivalence.functor ⋙ L₁.op)

Tactic:
refine fun _ _ _ hf ↦ Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_
      simpa [trW_inverseImage_ι_iff, ← op_inf, trW_op] using! hf

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case pos
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
h : a ≤ b
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

pp: case neg
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
h : ¬a ≤ b
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
· let u₁₂ := (t.natTransTruncLTOfLE a b h).app X
    let u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
    let u₁₃ : _ ⟶ X := (t.truncLTι a).app X
    have eq : u₁₂ ≫ u₂₃ = u₁₃ := by simp [u₁₂, u₂₃, u₁₃]
    have H := someOctahedron eq (t.triangleLTLTGELT_distinguished a b h X)
      (t.triangleLTGE_distinguished b X) (t.triangleLTGE_distinguished a X)
    let m₁ : (t.truncGELT a b).obj X ⟶ _ := H.m₁
    have : IsIso ((t.truncLT b).map H.m₁) :=
      t.isIso₁_truncLT_map_of_isGE _ H.mem b (by dsimp; infer_instance)
    have eq' : t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncGELTToLTGE a b).app X :=
      t.to_truncLT_obj_ext
        (by dsimp; exact t.from_truncGE_obj_ext (by simpa using H.comm₁))
    rw [← eq']
    have fac : (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫
        t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncLT b).map m₁ :=
      t.to_truncLT_obj_ext (by simp [truncGELT])
    exact IsIso.of_isIso_fac_left fac

Goal state after:
case neg
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
h : ¬a ≤ b
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsFibrant Y
h✝ : RightHomotopyRel f g
Q : Cylinder X
inst✝ : Q.IsGood
P : PathObject Y := ⋯.choose
h : ⋯.choose.RightHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
⊢ Q.i₀ ≫ sq.lift ≫ P.p₁ = f

Tactic:
by
      have := coprod.inl ≫= sq.fac_left
      rw [Q.inl_i_assoc, coprod.inl_desc] at this
      simp [reassoc_of% this]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ ∃ X', ∃ (_ : IsFibrant X'), ∃ i, Cofibration i ∧ WeakEquivalence i

Tactic:
have h := MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C)
    (terminal.from X)
  refine ⟨h.Z, ?_, h.i, inferInstance, inferInstance⟩
  rw [isFibrant_iff_of_isTerminal h.p terminalIsTerminal]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: case refine_2
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : S → CostructuredArrowDownwards e.hom g := fun s ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv ↑s ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ A : CostructuredArrowDownwards e.hom g
a : X₀ ⟶ (CostructuredArrow.left A).right
ha : T.map a = e₀.hom ≫ (CostructuredArrow.left A).hom
⊢ (CostructuredArrow.left (Z ⟨L.map a ≫ StructuredArrow.Hom.right (CostructuredArrow.hom A), ⋯⟩)).hom ≫ T.map a =
    (CostructuredArrow.left A).hom

Tactic:
· cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : W₁.ContainsIdentities
⊢ (id W₁).IsLeftDerivabilityStructure

Tactic:
rw [(LocalizerMorphism.id W₁).isLeftDerivabilityStructure_iff W₁.Q W₁.Q (𝟭 W₁.Localization)
    (Iso.refl _)]
  dsimp
  exact TwoSquare.guitartExact_id' W₁.Q

Goal state after: