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₂_1 : ∀ (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))
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
h₄ :
  Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)
simp : (n + 1) * (n + 2) + (n + 1 + (n + 1) + 2) = (n + 2 + 1) * (n + 1 + 1)
⊢ Sᶜ.card + S.card +
      (Finset.card (α := Fin (n + 1)) Finset.univ + Finset.card (α := Fin (n + 1)) Finset.univ +
        Finset.card (α := Fin (n + 2 + 1) × Fin (n + 1 + 1)) {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}) =
    Finset.card (α := Fin (n + 2 + 1) × Fin (n + 1 + 1)) Finset.univ

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₂_1 : ∀ (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))
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
h₄ :
  Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)
⊢ (n + 1) * (n + 2) + (n + 1 + (n + 1) + 2) = (n + 2 + 1) * (n + 1 + 1)

Tactic:
lia
-- 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₂_1 : ∀ (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))
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
h₄ :
  Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)
⊢ ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)ᶜ =
    ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃

Tactic:
have H : (Finset.disjUnion _ _ h₁)ᶜ = Finset.disjUnion _ _ h₃ :=
    Finset.compl_eq_of_disjoint_of_card_add_eq h₄ (by
      rw [Finset.card_disjUnion, Finset.card_disjUnion, Finset.card_disjUnion,
        Finset.card_image_of_injective _ hγ₁, Finset.card_image_of_injective _ hγ₂,
        Finset.card_image_of_injective _ hγ₃, Finset.card_image_of_injective _ hγ₄]
      simp
      lia)
-- 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_1 : 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_1.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_1.h x.2 ≫ Y.δ x.1
h₂_1 : ∀ (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_1.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H_1.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))
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
h₄ :
  Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)
H :
  ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)ᶜ =
    ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃
⊢ (0, 0) ∉ {(Fin.last (n + 2), Fin.last (n + 1))}

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_1 : 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_1.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_1.h x.2 ≫ Y.δ x.1
h₂_1 : ∀ (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_1.h 0 ≫ Y.δ 0 = β (0, 0)
eq₂ : H_1.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))
h₁ : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂ : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃ :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
h₄ :
  Disjoint ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)
    (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃)
H :
  ((Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁)ᶜ =
    ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
      {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃
⊢ -β (Fin.last (n + 2), Fin.last (n + 1)) =
    -β (Fin.last (n + 2), Fin.last (n + 1)) + -β (0, 0) +
        HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) (- -∑ x : Fin (n + 1), β (γ₃ x)) (-∑ x : Fin (n + 1), β (γ₃ x)) +
      β (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_1 H : Homotopy f g
f_1 :
  (i j : ℕ) →
    HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) i ⟶
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) j
⊢ (ComplexShape.down ℕ).Rel 1 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_1 H : Homotopy f g
⊢ ¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 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_1 H : Homotopy f g
zero :
  HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) 0 =
    HAdd.hAdd (α :=
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
      (β :=
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
      (CategoryStruct.comp (Y := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 1)
        (ToChainHomotopy.hom H 0 1) (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) 1 0))
      (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) 0)
⊢ HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) 0 =
    HAdd.hAdd (α :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
        (β :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
        ((dNext 0 :
              (a : (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                ((alternatingFaceMapComplex C).obj X).X 0 ⟶ ((alternatingFaceMapComplex C).obj Y).X 0)
            (ToChainHomotopy.hom H) :
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
        ((prevD 0 :
              (a : (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                ((alternatingFaceMapComplex C).obj X).X 0 ⟶ ((alternatingFaceMapComplex C).obj Y).X 0)
            (ToChainHomotopy.hom H) :
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0) +
      HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) 0

Tactic:
rw [prevD_eq (j' := 1) (w := by simp), dNext_eq_zero _ _ (by simp), zero_add]

Premises used: prevD_eq, zero_add, dNext_eq_zero
-- 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_1 H : Homotopy f g
⊢ HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) 0 =
    HAdd.hAdd (α :=
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
      (β :=
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) 0 ⟶
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 0)
      (CategoryStruct.comp (Y := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) 1)
        (ToChainHomotopy.hom H 0 1) (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) 1 0))
      (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) 0)

Tactic:
simp [ToChainHomotopy.comm_zero H]

Premises used: _private.0.CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.comm_zero
-- 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_1 H : Homotopy f g
n : ℕ
f_1 :
  (i j : ℕ) →
    HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) i ⟶
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) j
⊢ (ComplexShape.down ℕ).Rel (n + 1) n

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_1 H : Homotopy f g
n : ℕ
f_1 :
  (i j : ℕ) →
    HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) i ⟶
      HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) j
⊢ (ComplexShape.down ℕ).Rel (n + 2) (n + 1)

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_1 H : Homotopy f g
n : ℕ
succ :
  HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) (n + 1) =
    HAdd.hAdd (α :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
        (β :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) n ≫ ToChainHomotopy.hom H n (n + 1))
        (CategoryStruct.comp (Y := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2))
          (ToChainHomotopy.hom H (n + 1) (n + 2))
          (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2) (n + 1))) +
      HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) (n + 1)
⊢ HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) (n + 1) =
    HAdd.hAdd (α :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
        (β :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
        ((dNext (n + 1) :
              (a : (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                ((alternatingFaceMapComplex C).obj X).X (n + 1) ⟶ ((alternatingFaceMapComplex C).obj Y).X (n + 1))
            (ToChainHomotopy.hom H) :
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
        ((prevD (n + 1) :
              (a : (i j : ℕ) → ((alternatingFaceMapComplex C).obj X).X i ⟶ ((alternatingFaceMapComplex C).obj Y).X j) →
                ((alternatingFaceMapComplex C).obj X).X (n + 1) ⟶ ((alternatingFaceMapComplex C).obj Y).X (n + 1))
            (ToChainHomotopy.hom H) :
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
            HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1)) +
      HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) (n + 1)

Tactic:
rw [dNext_eq (i' := n) (w := by simp), prevD_eq (j' := n + 2) (w := by simp)]

Premises used: prevD_eq, dNext_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_1 H : Homotopy f g
n : ℕ
⊢ HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) f) (n + 1) =
    HAdd.hAdd (α :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
        (β :=
        HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) ⟶
          HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 1))
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X) (n + 1) n ≫ ToChainHomotopy.hom H n (n + 1))
        (CategoryStruct.comp (Y := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2))
          (ToChainHomotopy.hom H (n + 1) (n + 2))
          (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y) (n + 2) (n + 1))) +
      HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) g) (n + 1)

Tactic:
simp [ToChainHomotopy.comm_succ H]

Premises used: _private.0.CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.comm_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
inst_2 : CategoryWithHomology.{v, u} C
H : Homotopy f g
n : ℕ
⊢ Eq (α :=
    Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n) (Functor.obj (alternatingFaceMapComplex C) X) ⟶
      Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n) (Functor.obj (alternatingFaceMapComplex C) Y))
    (Functor.map (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n)
      (Functor.map (alternatingFaceMapComplex C) f))
    (Functor.map (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n)
      (Functor.map (alternatingFaceMapComplex C) g))

Tactic:
simpa using (H.toChainHomotopy).homologyMap_eq n

Premises used: Homotopy.homologyMap_eq, CategoryTheory.SimplicialObject.Homotopy.toChainHomotopy
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
inst_1 : ∀ (F : Functor.{0, v, 0, u} (SimplexCategory.Truncated n)ᵒᵖ C), (inclusion n).op.HasRightKanExtension F
inst_2 : X.IsCoskeletal n
⊢ CostructuredArrow.IsUniversal (rightExtensionInclusion X n)

Tactic:
apply Functor.isUniversalOfIsRightKanExtension

Premises used: CategoryTheory.Functor.isUniversalOfIsRightKanExtension