mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.toN = N.mk ↑z ⋯
⊢ ∃! f_1,
    Epi f_1 ∧
      (ConcreteCategory.hom (X.map f_1.op)) (N.mk ↑z ⋯).simplex =
        { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.simplex

Tactic:
refine existsUnique_of_exists_of_unique ⟨f, inferInstance, rfl⟩
    (fun f₁ f₂ ⟨_, hf₁⟩ ⟨_, hf₂⟩ ↦ unique_nonDegenerate_map _ _ _ _ hf₁.symm _ _ hf₂.symm)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_2 Edge._proof_2).op)) e.edge) =
    (id x).edge

Tactic:
by
    rw [← Functor.map_comp_apply, ← op_comp, δ₂_two_comp_σ₂_zero]
    simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
⊢ face S₁ ≤ face S₂ ↔ S₁ ⊆ S₂

Tactic:
refine ⟨fun h i hi ↦ ?_, fun h d a ha ↦ ha.trans h⟩
  simp only [← obj₀Equiv_symm_mem_face_iff.{u}] at hi ⊢
  exact h _ hi

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
f : ⦋d⦌ ⟶ ⦋n⦌
⊢ objEquiv.symm f ∈ Δ[n].nonDegenerate d ↔ Mono f

Tactic:
simp [mem_nonDegenerate_iff_mono]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
f : unop x✝¹ ⟶ ⦋n⦌
x✝ : objEquiv.symm f ∈ ⊤.obj x✝¹
⊢ (ConcreteCategory.hom (Δ[n].map f.op)) (objEquiv.symm (𝟙 ⦋n⦌)) = objEquiv.symm f

Tactic:
by simp [map_objEquiv_symm.{u}]

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

Goal state before:
pp: case neg
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₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : ¬c₁₂.Rel i₁₂' i₁₂''
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
rw [K.D₁_shape c₁₂ _ _ h₂, comp_zero]

Goal state after:
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₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

pp: case neg
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₁₂'' : I₁₂
h₁ : ¬c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

Tactic:
· by_cases h₂ : c₁₂.Rel i₁₂' i₁₂''
    · ext ⟨i₁, i₂⟩ h
      simp only [totalAux.ιMapObj_D₂_assoc, comp_neg, totalAux.ιMapObj_D₁_assoc]
      by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)
      · rw [totalAux.d₁_eq K c₁₂ h₃ i₂ i₁₂']; swap
        · rw [← ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₂]
        by_cases h₄ : c₂.Rel i₂ (c₂.next i₂)
        · have h₅ : ComplexShape.π c₁ c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂' := by
            rw [← c₁₂.next_eq' h₁, ← h, ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄]
          have h₆ : ComplexShape.π c₁ c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂'' := by
            rw [← c₁₂.next_eq' h₂, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, h₅]
          simp only [totalAux.d₂_eq K c₁₂ _ h₄ _ h₅, totalAux.d₂_eq K c₁₂ _ h₄ _ h₆,
            Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁, Linear.comp_units_smul,
            totalAux.d₁_eq K c₁₂ h₃ _ _ h₆, HomologicalComplex.Hom.comm_assoc, smul_smul,
            ComplexShape.ε₂_ε₁ c₁₂ h₃ h₄, neg_mul, Units.neg_smul]
        · simp only [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp, comp_zero, smul_zero, neg_zero]
      · rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp, neg_zero]
        by_cases h₄ : c₂.Rel i₂ (c₂.next i₂)
        · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂']; swap
          · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' h₁, h]
          simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
          rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, comp_zero, smul_zero]
        · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp]
    · rw [K.D₁_shape c₁₂ _ _ h₂, K.D₂_shape c₁₂ _ _ h₂, comp_zero, comp_zero, neg_zero]

Goal state after:
case neg
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₁₂'' : I₁₂
h₁ : ¬c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: 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₁₂'' : I₁₂
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

Tactic:
by_cases h₁ : c₁₂.Rel i₁₂ i₁₂'
  · by_cases h₂ : c₁₂.Rel i₁₂' i₁₂''
    · ext ⟨i₁, i₂⟩ h
      simp only [totalAux.ιMapObj_D₂_assoc, comp_neg, totalAux.ιMapObj_D₁_assoc]
      by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)
      · rw [totalAux.d₁_eq K c₁₂ h₃ i₂ i₁₂']; swap
        · rw [← ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₂]
        by_cases h₄ : c₂.Rel i₂ (c₂.next i₂)
        · have h₅ : ComplexShape.π c₁ c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂' := by
            rw [← c₁₂.next_eq' h₁, ← h, ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄]
          have h₆ : ComplexShape.π c₁ c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂'' := by
            rw [← c₁₂.next_eq' h₂, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, h₅]
          simp only [totalAux.d₂_eq K c₁₂ _ h₄ _ h₅, totalAux.d₂_eq K c₁₂ _ h₄ _ h₆,
            Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁, Linear.comp_units_smul,
            totalAux.d₁_eq K c₁₂ h₃ _ _ h₆, HomologicalComplex.Hom.comm_assoc, smul_smul,
            ComplexShape.ε₂_ε₁ c₁₂ h₃ h₄, neg_mul, Units.neg_smul]
        · simp only [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp, comp_zero, smul_zero, neg_zero]
      · rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp, neg_zero]
        by_cases h₄ : c₂.Rel i₂ (c₂.next i₂)
        · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂']; swap
          · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' h₁, h]
          simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
          rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, comp_zero, smul_zero]
        · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp]
    · rw [K.D₁_shape c₁₂ _ _ h₂, K.D₂_shape c₁₂ _ _ h₂, comp_zero, comp_zero, neg_zero]
  · rw [K.D₁_shape c₁₂ _ _ h₁, K.D₂_shape c₁₂ _ _ h₁, zero_comp, zero_comp, neg_zero]

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

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₂.π c₁ c (i₂, i₁) = j
⊢ K.flip.ιTotal c i₂ i₁ j h ≫ (K.totalFlipIso c).hom.f j = c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯

Tactic:
simp [totalFlipIso, totalFlipIsoX]

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

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j = c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯

Tactic:
simp [totalFlipIso, totalFlipIsoX]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
⊢ Function.LeftInverse
    (fun x_1 ↦
      match x_1 with
      | ⟨(a, b), h⟩ => ⟨(a - x, b), ⋯⟩)
    fun x_1 ↦
    match x_1 with
    | ⟨(a, b), h⟩ => ⟨(a + x, b), ⋯⟩

Tactic:
by
        rintro ⟨⟨a, b⟩, h⟩
        ext
        · dsimp
          lia
        · rfl

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

Goal state before:
pp: case pos.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p.negOnePow = x.negOnePow * (p + x).negOnePow

Tactic:
add_comm p,

Goal state after:
case pos.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p.negOnePow = x.negOnePow * (x + p).negOnePow
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₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit sq.cokernelCofork
s : PushoutCocone f g
m : X₄ ⟶ s.pt
hm₁ : inl ≫ m = s.inl
hm₂ : inr ≫ m = s.inr
⊢ m = h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)

Tactic:
apply Cofork.IsColimit.hom_ext h

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit sq.cokernelCofork
s : PushoutCocone f g
m : X₄ ⟶ s.pt
hm₁ : inl ≫ m = s.inl
hm₂ : inr ≫ m = s.inr
⊢ Cofork.π sq.cokernelCofork ≫ m = Cofork.π sq.cokernelCofork ≫ h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)
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
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m ≫ (PullbackCone.mk fst snd ⋯).fst =
    PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ (PullbackCone.mk fst snd ⋯).fst

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
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m ≫ (PullbackCone.mk fst snd ⋯).snd =
    PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ (PullbackCone.mk fst snd ⋯).snd

Tactic:
· replace hm := hm =≫ biprod.fst
          dsimp at hm ⊢
          simp only [assoc, biprod.lift_fst] at hm
          rw [hm]
          symm
          apply PullbackCone.IsLimit.lift_fst h

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
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m ≫ (PullbackCone.mk fst snd ⋯).snd =
    PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ (PullbackCone.mk fst snd ⋯).snd
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos.e_a
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{v_1, u_1} C₁
inst✝²² : Category.{v_2, u_2} C₂
inst✝²¹ : Category.{v_3, u_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
⊢ c₁.ε₂ c₂₃ c₄ (i₁, i₂₃) •
      (F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) ⋯) ≫
        (F.obj (K₁.X i₁)).map (mapBifunctor.D₂ K₂ K₃ G₂₃ c₂₃ i₂₃ (c₂₃.next i₂₃)) ≫
          K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂₃.next i₂₃) j' h₂ =
    d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
· rw [← Functor.map_comp_assoc, mapBifunctor.ι_D₂]
        by_cases h₃ : c₃.Rel i₃ (c₃.next i₃)
        · rw [d₃_eq _ _ _ _ _ _ _ _ _ _ h₃,
            mapBifunctor.d₂_eq _ _ _ _ _ h₃ _ (ComplexShape.next_π₂ c₂ c₂₃ i₂ h₃).symm,
            Functor.map_units_smul, Functor.map_comp, Linear.units_smul_comp, assoc,
            smul_smul, smul_left_cancel_iff]
          rw [ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ _ (by
            dsimp [ComplexShape.r]
            rw [← h₂, ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₂ c₂ c₂₃ i₂ h₃]),
            ι_eq]
        · rw [d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃,
            mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₃,
            Functor.map_zero, zero_comp, smul_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : C
P : PrepathObject A
inst✝ : HasBinaryProduct A A
⊢ P.p ≫ prod.fst = P.p₀

Tactic:
simp [p]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : C
P : PrepathObject A
inst✝ : HasBinaryProduct A A
⊢ P.p ≫ prod.snd = P.p₁

Tactic:
simp [p]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
⊢ (functor r).IsLocalization W

Tactic:
apply Functor.IsLocalization.mk'
  all_goals apply isLocalization_functor.strictUniversalPropertyFixedTarget hW hr

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

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✝³ : Preadditive D
A : Type u_3
inst✝² : Category.{v_3, u_3} A
inst✝¹ : Abelian A
F : C ⥤ D
inst✝ : F.Additive
⊢ ∀ (X : HomotopyCategory.Plus C),
    HomotopyCategory.plus D ((HomotopyCategory.Plus.ι C ⋙ F.mapHomotopyCategory (ComplexShape.up ℤ)).obj X)

Tactic:
rintro ⟨X, hX⟩
      obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective X
      dsimp
      simp only [HomotopyCategory.plus_quotient_obj_iff] at hX ⊢
      obtain ⟨n, _⟩ := hX
      exact ⟨n, inferInstanceAs (CochainComplex.IsStrictlyGE
        ((F.mapHomologicalComplex _).obj K) n)⟩

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

Goal state before:
pp: 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✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
hf : ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), B.inverseImage A.ι Z
⊢ ∃ Z g h, ∃ (_ : Triangle.mk (A.ι.map f) g h ∈ Pretriangulated.distinguishedTriangles), B Z

Tactic:
obtain ⟨Z, a, b, hT, hZ⟩ := hf

Goal state after:
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✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : A.FullSubcategory
a : Y ⟶ Z
b : Z ⟶ (shiftFunctor A.FullSubcategory 1).obj X
hT : Triangle.mk f a b ∈ Pretriangulated.distinguishedTriangles
hZ : B.inverseImage A.ι Z
⊢ ∃ Z g h, ∃ (_ : Triangle.mk (A.ι.map f) g h ∈ Pretriangulated.distinguishedTriangles), B Z
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : Plus C
f : K ⟶ L
M : Plus C
g : L ⟶ M
h : M ⟶ (shiftFunctor (Plus C) 1).obj K
mem : Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
⊢ quasiIso C f ↔ (subcategoryAcyclic C).trW f

Tactic:
have := (HomotopyCategory.subcategoryAcyclic C).trW_iff_of_distinguished _
    ((HomotopyCategory.Plus.ι C).map_distinguished _ mem)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : Plus C
f : K ⟶ L
M : Plus C
g : L ⟶ M
h : M ⟶ (shiftFunctor (Plus C) 1).obj K
mem : Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
this :
  (HomotopyCategory.subcategoryAcyclic C).trW ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).mor₁ ↔
    HomotopyCategory.subcategoryAcyclic C ((ι C).mapTriangle.obj (Pretriangulated.Triangle.mk f g h)).obj₃
⊢ quasiIso C f ↔ (subcategoryAcyclic C).trW f
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 : Plus C
n : ℤ
inst✝ : X.IsGE n
⊢ (ι.obj X).IsGE n

Tactic:
isGE_ι_obj_iff

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X : Plus C
n : ℤ
inst✝ : X.IsGE n
⊢ X.IsGE n
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ epiWithInjectiveKernel g →
    ∃ I,
      ∃ (_ : Injective I),
        ∃ f, ∃ (w : f ≫ g = 0), Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting

Tactic:
rintro ⟨_, _⟩
    let S := ShortComplex.mk (kernel.ι g) g (by simp)
    exact ⟨_, inferInstance, _, S.zero,
      ⟨ShortComplex.Splitting.ofExactOfRetraction S
        (S.exact_of_f_is_kernel (kernelIsKernel g)) (Injective.factorThru (𝟙 _) (kernel.ι g))
        (by simp [S]) inferInstance⟩⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
⊢ HomComplex.δ 1 2 (HomComplex.Cochain.mk fun p q x ↦ K.d p q ≫ Injective.ι (K.X q)) = 0

Tactic:
by
        ext p q hpq
        simp [HomComplex.δ_v 1 2 (by lia) _ p q hpq (p + 1) (p + 1) (by lia) rfl]

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
h₀ : Homotopy (𝟙 (mappingCone (𝟙 (I K)))) 0 :=
  mappingCone.liftHomotopy (𝟙 (I K)) (𝟙 (mappingCone (𝟙 (I K)))) 0 (mappingCone.snd (𝟙 (I K))) 0 ⋯ ⋯
h₁ : Homotopy (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl) (biprod.fst ≫ 0 ≫ biprod.inl) :=
  (h₀.compRight biprod.inl).compLeft biprod.fst
h₂ : Homotopy (biprod.fst ≫ 𝟙 (mappingCone (𝟙 (I K))) ≫ biprod.inl + biprod.snd ≫ biprod.inr)
  (biprod.fst ≫ 0 ≫ biprod.inl + biprod.snd ≫ biprod.inr) :=
  h₁.add (Homotopy.refl (biprod.snd ≫ biprod.inr))
⊢ p K L ≫ biprod.inr = biprod.fst ≫ 0 ≫ biprod.inl + biprod.snd ≫ biprod.inr

Tactic:
simp [p]

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
X : C
a b : ℤ
inst✝ : t.IsGE X a
h : a ≤ b
⊢ t.IsGE ((t.truncGE b).obj X) a

Tactic:
exact t.isGE_truncGE_obj ..

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
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
let u₁₃ : _ ⟶ X := (t.truncLTι a).app X

Goal state after:
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
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
⊢ IsIso ((t.truncGELTToLTGE a b).app X)