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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ X.left.δ₀Iter ↑(Fin.last n) ⋯ ≫ ed.s 0 ≫ X.left.σ₀Iter ↑(Fin.last n) ⋯ ≫ X.left.δ (Fin.last (n + 1)) =
    X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)

Tactic:
X.left.σ₀Iter_δ' _ _ 1 (by grind),

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ X.left.δ₀Iter ↑(Fin.last n) ⋯ ≫ ed.s 0 ≫ X.left.δ 1 ≫ X.left.σ₀Iter ↑(Fin.last n) ⋯ =
    X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
⊢ s i.castSucc < s i.succ

Tactic:
obtain h' | h' := (stdSimplex.monotone_apply s i.castSucc_le_succ).lt_or_eq

Goal state after:
case inl
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc < (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ

case inr
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc = (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ Function.Injective
    ⇑(Hom.toOrderHom (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))))

Tactic:
intro a

Goal state after:
case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
a : Fin ((unop (op ⦋m⦌)).len + 1)
⊢ ∀ ⦃a₂ : Fin ((unop (op ⦋m⦌)).len + 1)⦄,
    (Hom.toOrderHom (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)))) a =
        (Hom.toOrderHom (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))))
          a₂ →
      a = a₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
⊢ ∀ {a b : Fin (d + 1)},
    (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b

Tactic:
intro a

Goal state after:
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a : Fin (d + 1)
⊢ ∀ {b : Fin (d + 1)}, (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯ ≫ X.left.σ i.succ =
    X.left.δ₀Iter (↑j.castSucc)
        (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_32 n j k hk) ≫
      ed.s ↑k ≫
        X.left.σ
            ⟨l, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_41 n i j k hk l hl⟩.succ ≫
          X.left.σ₀Iter ↑j.castSucc ⋯

Tactic:
X.left.σ₀Iter_σ' j i.succ ⟨l + 1, by grind⟩ (by grind)

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ X.left.δ₀Iter ↑j ⋯ ≫
      ed.s ↑k ≫
        X.left.σ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_43 n i j k hk l hl⟩ ≫
          X.left.σ₀Iter ↑j ⋯ =
    X.left.δ₀Iter (↑j.castSucc)
        (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_32 n j k hk) ≫
      ed.s ↑k ≫
        X.left.σ
            ⟨l, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_41 n i j k hk l hl⟩.succ ≫
          X.left.σ₀Iter ↑j.castSucc ⋯
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c
inst✝² : TotalComplexShape c₂ c₃ c₂₃
inst✝¹ : TotalComplexShape c₁ c₂₃ c
inst✝ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

Tactic:
by
  apply Associative.ε₁_eq_mul

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      0 =
    (((dNext 0) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD 0) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
Y : C₄
j : J
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ'
⊢ φ = φ'

Tactic:
apply mapObj_ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
Y : C₄
j : J
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ'
⊢ ∀ (i : I₁ × I₂ × I₃) (hij : p i = j),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p i j hij ≫ φ =
      ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p i j hij ≫ φ'
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:
rw [K.d₁_eq_zero' c₁₂ h₁ i₂ i₁₂']
    intro h₂
    exact h₁₂ (by simpa only [← h, ← h₂] using ComplexShape.rel_π₁ c₂ c₁₂ h₁ i₂)

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

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
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : Preadditive D
K₁ L₁ : HomologicalComplex C₁ c₁
K₂ L₂ : HomologicalComplex C₂ c₂
f₁ : K₁ ⟶ L₁
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.PreservesZeroMorphisms
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝³ : TotalComplexShape c₁ c₂ c
inst✝² : K₁.HasMapBifunctor K₂ F c
inst✝¹ : L₁.HasMapBifunctor L₂ F c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ (mapBifunctorMap f₁ f₂ F c).f j =
    (F.map (f₁.f i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h

Tactic:
by
  simp [mapBifunctorMap]

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

Goal state before:
pp: case pos
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₀
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁')

Tactic:
dsimp [totalShift₁XIso]

Goal state after:
case pos
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₀
⊢ (((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₁ (up ℤ) n₀ n₁ ≫
        ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow •
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₁ (up ℤ) n₀' n₁')
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
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₀
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
dsimp [totalShift₁XIso]

Goal state after:
case pos
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₀
⊢ (((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫
        ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow •
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₂ (up ℤ) n₀' n₁')
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n₁ : ℕ
⊢ (↑(sequence φ x₀ n₁)).EqUpTo (↑(sequence φ x₀ (n₁ + 0))) (p₀ + ↑n₁)

Tactic:
intro _ _ _ _

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n₁ : ℕ
p✝ q✝ : ℤ
hpq✝ : p✝ + d = q✝
a✝ : p✝ ≤ p₀ + ↑n₁
⊢ (↑(sequence φ x₀ n₁)).v p✝ q✝ hpq✝ = (↑(sequence φ x₀ (n₁ + 0))).v p✝ q✝ hpq✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n₁ : ℕ
⊢ (↑(sequence φ x₀ n₁)).EqUpTo (↑(sequence φ x₀ (n₁ + 0))) (p₀ + ↑n₁)

Tactic:
| zero =>

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j))) (S.X₁.cyclesMk x₁ k hk ⋯) =
    (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.opcyclesToCycles i j)))
      ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.pOpcycles i))) x₂)

Tactic:
· apply (Preadditive.mono_iff_injective (S.X₂.iCycles j)).1 inferInstance
    conv_lhs =>
      rw [← ConcreteCategory.forget₂_comp_apply, HomologicalComplex.cyclesMap_i,
        ConcreteCategory.forget₂_comp_apply, HomologicalComplex.i_cyclesMk, hx₁]
    conv_rhs =>
      rw [← ConcreteCategory.forget₂_comp_apply, ← ConcreteCategory.forget₂_comp_apply,
        HomologicalComplex.pOpcycles_opcyclesToCycles_assoc, HomologicalComplex.toCycles_i]

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

Goal state before:
pp: case neg
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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_5, u_3} 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✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : 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 ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 0 = d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
rw [d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₃]

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

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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
⊢ ∀ (a b c : ℕ), a + b = c → H a → H b → H c

Tactic:
intro a

Goal state after:
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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
a : ℕ
⊢ ∀ (b c : ℕ), a + b = c → H a → H b → H c
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
⊢ ∀ (a : ℕ), H a

Tactic:
intro a

Goal state after:
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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
⊢ H a
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case zero
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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
⊢ H 0

Tactic:
| zero =>

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

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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
⊢ ∀ (a b c : ℕ), a + b = c → H a → H b → H c

Tactic:
intro a

Goal state after:
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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
a : ℕ
⊢ ∀ (b c : ℕ), a + b = c → H a → H b → H c
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
⊢ ∀ (a : ℕ), H a

Tactic:
intro a

Goal state after:
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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
⊢ H a
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case zero
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
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
⊢ H 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h✝ : K.IsStrictlyGE 1
⊢ ∃ K x, K.IsStrictlyGE 0

Tactic:
exact ⟨K, e, K.isStrictlyGE_of_ge 0 1 (by lia)⟩

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
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : (Cocycle.equivHom K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) φ = z.rightShift n 0 ⋯
⊢ ∃ α, δ m n α = ↑z

Tactic:
rw [Cocycle.ext_iff] at hφ

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : ↑((Cocycle.equivHom K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) φ) = ↑(z.rightShift n 0 ⋯)
⊢ ∃ α, δ m n α = ↑z
Module: Mathlib.AlgebraicTopology.ModelCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝³ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst✝¹ : Fibration f
inst✝ : WeakEquivalence w
h : RetractArrow f w
⊢ WeakEquivalence f

Tactic:
by
  have hw := factorizationData (trivialCofibrations C) (fibrations C) w
  have : (trivialFibrations C).IsStableUnderRetracts := by
    rw [← cofibrations_rlp]
    infer_instance
  have sq : CommSq h.r.left hw.i f (hw.p ≫ h.r.right) := ⟨by simp⟩
  have hf : fibrations C f := by rwa [← fibration_iff]
  have : HasLiftingProperty hw.i f := hasLiftingProperty_of_wfs _ _ hw.hi hf
  have : RetractArrow f hw.p :=
    { i := Arrow.homMk (h.i.left ≫ hw.i) h.i.right
      r := Arrow.homMk sq.lift h.r.right }
  have h' : trivialFibrations C hw.p :=
    ⟨hw.hp, (weakEquivalence_iff _).1 (weakEquivalence_of_precomp_of_fac hw.fac)⟩
  simpa only [weakEquivalence_iff] using (of_retract this h').2

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
⊢ Cofibration (coprod.map P.i₀ (𝟙 A) ≫ ψ)

Tactic:
have : Cofibration ψ := by
      rw [cofibration_iff]
      exact (cofibrations C).of_isPushout
        (IsPushout.of_top sq fac (IsPushout.of_coprod_inl_with_id P.i₁ A).flip)
        (by rw [← cofibration_iff]; infer_instance)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
this : Cofibration ψ
⊢ Cofibration (coprod.map P.i₀ (𝟙 A) ≫ ψ)