awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (hypothesis)
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.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
have 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₃)
Tactic: have h₄ : Disjoint (Finset.disjUnion _ _ h₁) (Finset.disjUnion _ _ h₃) := by
    rw [Finset.disjoint_iff_ne]
    simp only [Finset.compl_filter, not_lt, Finset.disjUnion_eq_union, Finset.mem_union,
      Finset.mem_image, Finset.mem_filter, Finset.mem_univ, true_and, Prod.exists, ne_eq,
      Finset.mem_insert, Finset.mem_singleton, Prod.forall, Prod.mk.injEq, not_and,
      S, γ₁, γ₂, γ₃, γ₄]
    rintro ⟨a, _⟩ ⟨b, _⟩ (⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩ | ⟨⟨j, _⟩, ⟨k, _⟩, h₁, h₂, h₃⟩) _ _
      ((⟨⟨i, _⟩, h₄, h₅⟩ | ⟨⟨i, _⟩, h₄, h₅⟩) | (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)) <;>
        simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢ <;> grind
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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₁).card +
      (((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
          {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃).card =
    Finset.card (α := Fin (n + 2 + 1) × Fin (n + 1 + 1)) Finset.univ
have rw : 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: 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γ₄]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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₃)
⊢ 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
have simp : (n + 1) * (n + 2) + (n + 1 + (n + 1) + 2) = (n + 2 + 1) * (n + 1 + 1)
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (hypothesis)
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₃)
⊢ 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
have 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)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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)
        ((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
have 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)
Tactic: rw [prevD_eq (j' := 1) (w := by simp), dNext_eq_zero _ _ (by simp), zero_add]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy (goal)
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))
        ((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)
have 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)
Tactic: rw [dNext_eq (i' := n) (w := by simp), prevD_eq (j' := n + 2) (w := by simp)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal (goal)
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
⊢ X.IsCoskeletal n ↔ IsIso (Y := obj (truncation n ⋙ Truncated.cosk n) X) (NatTrans.app (Adjunction.unit (coskAdj n)) X)
have rw : IsRightKanExtension X (𝟙 ((inclusion n).op ⋙ X)) ↔
  IsIso (Y := obj (truncation n ⋙ Truncated.cosk n) X) (NatTrans.app (Adjunction.unit (coskAdj n)) X)
Tactic: rw [isCoskeletal_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Homotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
⊢ Eq (α := X _⦋n⦌ ⟶ Y _⦋n⦌) ((X.σ 0 ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ 0) (f.app (op ⦋n⦌))
have this : Y.σ 0 ≫ Y.δ (Fin.castSucc 0) = 𝟙 (Y _⦋n⦌)
Tactic: have := Y.δ_comp_σ_self (n := n) (i := 0)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Homotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
⊢ (X.σ (Fin.last n) ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ (Fin.last (n + 1)) = f.app (op ⦋n⦌)
have this : Y.σ (Fin.last n) ≫ Y.δ (Fin.last n).succ = 𝟙 (Y _⦋n⦌)
Tactic: have := Y.δ_comp_σ_succ (i := Fin.last n)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Homotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
j : Fin (n + 1)
⊢ (X.σ j.succ ≫ f.app (op ⦋n + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ =
    (X.σ j.castSucc ≫ f.app (op ⦋n + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ
have h₁ : Y.σ j.succ ≫ Y.δ j.succ.castSucc = 𝟙 (Y _⦋n + 1⦌)
Tactic: have h₁ := Y.δ_comp_σ_self (i := j.succ)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Homotopy (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SimplicialObject.{v, u} C
f_1 g f : X ⟶ Y
n : ℕ
j : Fin (n + 1)
h₁ : Y.σ j.succ ≫ Y.δ j.succ.castSucc = 𝟙 (Y _⦋n + 1⦌)
⊢ (X.σ j.succ ≫ f.app (op ⦋n + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ =
    (X.σ j.castSucc ≫ f.app (op ⦋n + 1 + 1⦌)) ≫ Y.δ j.castSucc.succ
have h₂ : Y.σ j.castSucc ≫ Y.δ j.castSucc.succ = 𝟙 (Y _⦋n + 1⦌)
Tactic: have h₂ := Y.δ_comp_σ_succ (i := j.castSucc)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ map' f x = Fin.last (n + 1) ↔ ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
have simp : (∀ b ∈ finset f x, b = Fin.last (n + 1)) ↔
  ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
Tactic: simp only [map', Finset.min'_eq_iff, last_mem_finset, Fin.last_le_iff, true_and]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) ↔
    ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
have mp : (∀ b ∈ finset f x, b = Fin.last (n + 1)) →
  ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
mp :
  (∀ b ∈ finset f x, b = Fin.last (n + 1)) →
    ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) ↔
    ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
have mpr : (∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x) →
  ∀ b ∈ finset f x, b = Fin.last (n + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
i : Fin (n + 1)
⊢ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
have mp : ∀ (this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 2)
hi : i ∈ finset f x
⊢ i = Fin.last (n + 1)
have mpr : ∀ (this : i ≠ Fin.last (n + 1)), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 2)
hi : i ∈ finset f x
this : i ≠ Fin.last (n + 1)
⊢ False
have mpr : ∀ (i : Fin (n + 1)) (hi : i.castSucc ∈ finset f x) (this : i.castSucc ≠ Fin.last (n + 1)), False
Tactic: obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last this
Cleared hypotheses: i, hi, this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (hypothesis)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
this : i.castSucc ≠ Fin.last (n + 1)
⊢ False
have hi₁ : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)
Tactic: simp only [castSucc_mem_finset_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
⊢ map' f x = y.castSucc ↔
    x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y) ∧
      ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
have simp : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y) →
  ((∀ b ∈ finset f x, y.castSucc ≤ b) ↔ ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x)
Tactic: simp only [map', Finset.min'_eq_iff, castSucc_mem_finset_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y)
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) ↔ ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
have mp : (∀ b ∈ finset f x, y.castSucc ≤ b) → ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y)
mp : (∀ b ∈ finset f x, y.castSucc ≤ b) → ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) ↔ ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
have mpr : (∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x) → ∀ b ∈ finset f x, y.castSucc ≤ b
Tactic: constructor