awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
simp :
  H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (-∑ x : Fin (n + 1), ∑ x_1 : Fin (n + 2), HPow.hPow (α := ℤ) (-1) ((↑x : ℕ) + (↑x_1 : ℕ)) • X.δ x_1 ≫ H.h x)
        (-∑ x : Fin (n + 1 + 2),
            ∑ x_1 : Fin (n + 1 + 1), HPow.hPow (α := ℤ) (-1) ((↑x : ℕ) + (↑x_1 : ℕ)) • H.h x_1 ≫ Y.δ x) +
      H.h 0 ≫ Y.δ 0
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (β := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) n ≫ hom H n (n + 1) :
          X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (CategoryStruct.comp (Y := Y _⦋n + 2⦌) (hom H (n + 1) (n + 2))
          (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2) (n + 1))) +
      H.h 0 ≫ Y.δ 0

Tactic:
simp only [alternatingFaceMapComplex_obj_d, AlternatingFaceMapComplex.objD, hom_eq,
    Preadditive.comp_neg, Preadditive.neg_comp, Preadditive.comp_sum,
    Preadditive.sum_comp, Preadditive.comp_zsmul, Preadditive.zsmul_comp,
    smul_neg, Finset.sum_neg_distrib, ← Finset.sum_zsmul, smul_smul, ← pow_add]

Premises used: AlgebraicTopology.alternatingFaceMapComplex_obj_d, CategoryTheory.Preadditive.comp_neg, pow_add, smul_smul, CategoryTheory.Preadditive.sum_comp, smul_neg, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.neg_comp, Finset.sum_zsmul, CategoryTheory.Preadditive.zsmul_comp, AlgebraicTopology.AlternatingFaceMapComplex.objD, Finset.sum_neg_distrib, CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
dsimp :
  HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1 =
    -(HPow.hPow (α := ℤ) (-1) ((↑x.2 : ℕ) + 1 + (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ)
⊢ α x = -β (x.2.succ, x.1.castSucc)

Tactic:
dsimp [α, β]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
simp :
  (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
    (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ
⊢ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1 =
    -(HPow.hPow (α := ℤ) (-1) ((↑x.2 : ℕ) + 1 + (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ)

Tactic:
simp only [← H.h_castSucc_comp_δ_succ_of_lt x.2 x.1 hx,
      pow_add, pow_one, mul_neg, mul_one, neg_mul, neg_smul, neg_neg]

Premises used: neg_smul, pow_add, neg_neg, Prod.fst, pow_one, neg_mul, mul_one, Prod.snd, CategoryTheory.SimplicialObject.Homotopy.h_castSucc_comp_δ_succ_of_lt, mul_neg
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
x : Fin (n + 1) × Fin (n + 2)
hx : x.1.castSucc < x.2
rw rw₁ :
  (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
    (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ
⊢ (HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ =
    (HPow.hPow (α := ℤ) (-1) (↑x.2 : ℕ) * HPow.hPow (α := ℤ) (-1) (↑x.1 : ℕ)) • H.h x.1.castSucc ≫ Y.δ x.2.succ

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
⊢ ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)

Tactic:
have h₂ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2) :
      α x = -β ⟨x.2.succ, x.1.castSucc⟩ := by
    dsimp [α, β]
    simp only [← H.h_castSucc_comp_δ_succ_of_lt x.2 x.1 hx,
      pow_add, pow_one, mul_neg, mul_one, neg_mul, neg_smul, neg_neg]
    rw [mul_comm]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
rw :
  H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (-∑ x : Fin (n + 1) × Fin (n + 2), α x)
        (-∑ x : Fin (n + 3) × Fin (n + 2), β x) +
      H.h 0 ≫ Y.δ 0
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌)
        (-∑ x : Fin (n + 1), ∑ x_1 : Fin (n + 2), HPow.hPow (α := ℤ) (-1) ((↑x : ℕ) + (↑x_1 : ℕ)) • X.δ x_1 ≫ H.h x)
        (-∑ x : Fin (n + 1 + 2),
            ∑ x_1 : Fin (n + 1 + 1), HPow.hPow (α := ℤ) (-1) ((↑x : ℕ) + (↑x_1 : ℕ)) • H.h x_1 ≫ Y.δ x) +
      H.h 0 ≫ Y.δ 0

Tactic:
rw [← Finset.sum_product .univ .univ α, ← Finset.sum_product .univ .univ β,
    Finset.univ_product_univ, Finset.univ_product_univ]

Premises used: Finset.univ, Finset.univ_product_univ, Finset.sum_product
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
x x_1 : Fin (n + 1) × Fin (n + 2)
⊢ γ₁ x = γ₁ x_1 → x = x_1

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
⊢ Function.Injective γ₁

Tactic:
have hγ₁ : Function.Injective γ₁ := fun _ _ ↦ by aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
x x_1 : Fin (n + 1) × Fin (n + 2)
⊢ γ₂ x = γ₂ x_1 → x = x_1

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
⊢ Function.Injective γ₂

Tactic:
have hγ₂ : Function.Injective γ₂ := fun _ _ ↦ by aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
x x_1 : Fin (n + 1)
⊢ γ₃ x = γ₃ x_1 → x = x_1

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
⊢ Function.Injective γ₃

Tactic:
have hγ₃ : Function.Injective γ₃ := fun _ _ ↦ by aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
x x_1 : Fin (n + 1)
⊢ γ₄ x = γ₄ x_1 → x = x_1

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
⊢ Function.Injective γ₄

Tactic:
have hγ₄ : Function.Injective γ₄ := fun _ _ ↦ by aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
⊢ H.h 0 ≫ Y.δ 0 = β (0, 0)

Tactic:
simp [β]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
⊢ H.h 0 ≫ Y.δ 0 = β (0, 0)

Tactic:
have eq₁ : H.h 0 ≫ Y.δ 0 = β ⟨0, 0⟩ := by simp [β]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : SimplicialObject.{v, u} C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : (x : Fin (n + 1) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • X.δ x.2 ≫ H.h x.1
β : (x : Fin (n + 3) × Fin (n + 2)) → X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌ :=
  fun (x : Fin (n + 3) × Fin (n + 2)) ↦ HPow.hPow (α := ℤ) (-1) ((↑x.1 : ℕ) + (↑x.2 : ℕ)) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x.1.castSucc < x.2), α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x : Fin (n + 1) × Fin (n + 2) | x.1.castSucc < x.2}
γ₁ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.castSucc, x.1.succ)
γ₂ : (x : Fin (n + 1) × Fin (n + 2)) → Fin (n + 2 + 1) × Fin (n + 1 + 1) :=
  fun (x : Fin (n + 1) × Fin (n + 2)) ↦ (x.2.succ, x.1.castSucc)
γ₃ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.succ)
γ₄ : (i : Fin (n + 1)) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun (i : Fin (n + 1)) ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
hγ₃ : Function.Injective γ₃
hγ₄ : Function.Injective γ₄
eq₁ : H.h 0 ≫ Y.δ 0 = β (0, 0)
dsimp :
  H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) =
    -HSMul.hSMul (β := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (HPow.hPow (α := ℤ) (-1) (n + 2 + (n + 1)))
        (H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 2)))
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))

Tactic:
dsimp [β]