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 : ℕ
α : (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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
⊢ Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ S, α x) (∑ x ∈ S, -β (γ₂ x))

Tactic:
Finset.sum_congr rfl (fun x hx ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- 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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
refine : ∀ (x : Fin (n + 1) × Fin (n + 2)) (hx : x ∈ S), α x = -β (γ₂ x)
⊢ Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ S, α x) (∑ x ∈ S, -β (γ₂ x))

Tactic:
refine Finset.sum_congr rfl (fun x hx ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- 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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ S
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)

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
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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ S
⊢ x.1.castSucc < x.2

Tactic:
simpa [S] using hx
-- 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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ S
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 (by simpa [S] using 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
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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
x : Fin (n + 1) × Fin (n + 2)
hx : x ∈ S
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
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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
⊢ Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ S, α x) (-∑ y ∈ Finset.image γ₂ S, β y)

Tactic:
have eq₄ : ∑ x ∈ S, α x = - ∑ y ∈ Finset.image γ₂ S, β y := by
    rw [← Finset.sum_neg_distrib, Finset.sum_image hγ₂.injOn]
    refine Finset.sum_congr rfl (fun x hx ↦ ?_)
    dsimp [α, β, γ₂]
    simp only [← H.h_castSucc_comp_δ_succ_of_lt x.2 x.1 (by simpa [S] using 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)
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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
eq₄ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ S, α x) (-∑ y ∈ Finset.image γ₂ S, β y)
rw : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x : Fin (n + 1), β (γ₄ x)) (∑ x : Fin (n + 1), -β (γ₃ x))
⊢ Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x : Fin (n + 1), β (γ₄ x)) (-∑ x : Fin (n + 1), β (γ₃ x))

Tactic:
rw [← Finset.sum_neg_distrib]

Premises used: Finset.sum_neg_distrib
-- 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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
eq₄ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ S, α x) (-∑ y ∈ Finset.image γ₂ S, β y)
x : Fin (n + 1)
hx : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ x
⊢ β (γ₄ x) = -β (γ₃ x)

Tactic:
simp [h_succ_comp_δ_castSucc_succ, β, γ₃, γ₄]

Premises used: CategoryTheory.SimplicialObject.Homotopy.h_succ_comp_δ_castSucc_succ
-- 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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
eq₄ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ S, α x) (-∑ y ∈ Finset.image γ₂ S, β y)
⊢ Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x : Fin (n + 1), β (γ₄ x)) (∑ x : Fin (n + 1), -β (γ₃ x))

Tactic:
exact Finset.sum_congr rfl (fun x hx ↦ by simp [h_succ_comp_δ_castSucc_succ, β, γ₃, γ₄])

Premises used: Finset.sum_congr, rfl
-- 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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
eq₄ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ S, α x) (-∑ y ∈ Finset.image γ₂ S, β y)
⊢ Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x : Fin (n + 1), β (γ₄ x)) (-∑ x : Fin (n + 1), β (γ₃ x))

Tactic:
have eq₅ : ∑ x, β (γ₄ x) = - ∑ x, β (γ₃ x) := by
    rw [← Finset.sum_neg_distrib]
    exact Finset.sum_congr rfl (fun x hx ↦ by simp [h_succ_comp_δ_castSucc_succ, β, γ₃, γ₄])
-- 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)
eq₂ : H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -β (Fin.last (n + 2), Fin.last (n + 1))
eq₃ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ Sᶜ, α x) (-∑ y ∈ Finset.image γ₁ Sᶜ, β y)
eq₄ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x ∈ S, α x) (-∑ y ∈ Finset.image γ₂ S, β y)
eq₅ : Eq.{v + 1} (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (∑ x : Fin (n + 1), β (γ₄ x)) (-∑ x : Fin (n + 1), β (γ₃ x))
rw : ∀ a ∈ Finset.image γ₁ Sᶜ, ∀ b ∈ Finset.image γ₂ S, a ≠ b
⊢ Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)

Tactic:
rw [Finset.disjoint_iff_ne]

Premises used: Finset.disjoint_iff_ne