awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))}
⊢ 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₃)
have rw : ∀ a ∈ (Finset.image γ₁ Sᶜ).disjUnion (Finset.image γ₂ S) h₁,
  ∀
    b ∈
      ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂).disjUnion
        {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))} h₃,
    a ≠ b
Tactic: rw [Finset.disjoint_iff_ne]
-- 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₁_1 : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂_2 : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃_1 :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂_2)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt : a < n + 2 + 1
b : ℕ
isLt_1 : b < n + 1 + 1
j : ℕ
isLt_2 : j < n + 1
k : ℕ
isLt_3 : k < n + 2
h₁ : (⟨k, isLt_3⟩ : Fin (n + 2)) ≤ ⟨j, isLt_2⟩.castSucc
h₂ : (⟨k, isLt_3⟩ : Fin (n + 2)).castSucc = ⟨a, isLt⟩
h₃ : (⟨j, isLt_2⟩ : Fin (n + 1)).succ = ⟨b, isLt_1⟩
a_1 : Fin (n + 2 + 1)
b_1 : Fin (n + 1 + 1)
i : ℕ
isLt_4 : i < n + 1
h₄ : (⟨i, isLt_4⟩ : Fin (n + 1)).castSucc.succ = a_1
h₅ : (⟨i, isLt_4⟩ : Fin (n + 1)).succ = b_1
⊢ (⟨a, isLt⟩ : Fin (n + 2 + 1)) = a_1 → ¬(⟨b, isLt_1⟩ : Fin (n + 1 + 1)) = b_1
have inl : ∀ (h₁ : k ≤ j) (h₂ : k = a) (h₃ : j + 1 = b), a = (↑a_1 : ℕ) → ¬b = (↑b_1 : ℕ)
Tactic: simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢
Cleared hypotheses: h₁, h₂, 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₁_1 : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂_2 : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃_1 :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂_2)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt : a < n + 2 + 1
b : ℕ
isLt_1 : b < n + 1 + 1
j : ℕ
isLt_2 : j < n + 1
k : ℕ
isLt_3 : k < n + 2
h₁ : (⟨k, isLt_3⟩ : Fin (n + 2)) ≤ ⟨j, isLt_2⟩.castSucc
h₂ : (⟨k, isLt_3⟩ : Fin (n + 2)).castSucc = ⟨a, isLt⟩
h₃ : (⟨j, isLt_2⟩ : Fin (n + 1)).succ = ⟨b, isLt_1⟩
a_1 : Fin (n + 2 + 1)
b_1 : Fin (n + 1 + 1)
i : ℕ
isLt_4 : i < n + 1
h₄ : (⟨i, isLt_4⟩ : Fin (n + 1)).castSucc.succ = a_1
h₅ : (⟨i, isLt_4⟩ : Fin (n + 1)).castSucc = b_1
⊢ (⟨a, isLt⟩ : Fin (n + 2 + 1)) = a_1 → ¬(⟨b, isLt_1⟩ : Fin (n + 1 + 1)) = b_1
have inl : ∀ (h₁ : k ≤ j) (h₂ : k = a) (h₃ : j + 1 = b), a = (↑a_1 : ℕ) → ¬b = (↑b_1 : ℕ)
Tactic: simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢
Cleared hypotheses: h₁, h₂, 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₁_1 : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂_2 : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃_1 :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂_2)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt : a < n + 2 + 1
b : ℕ
isLt_1 : b < n + 1 + 1
j : ℕ
isLt_2 : j < n + 1
k : ℕ
isLt_3 : k < n + 2
h₁ : (⟨k, isLt_3⟩ : Fin (n + 2)) ≤ ⟨j, isLt_2⟩.castSucc
h₂ : (⟨k, isLt_3⟩ : Fin (n + 2)).castSucc = ⟨a, isLt⟩
h₃ : (⟨j, isLt_2⟩ : Fin (n + 1)).succ = ⟨b, isLt_1⟩
⊢ (⟨a, isLt⟩ : Fin (n + 2 + 1)) = 0 → ¬(⟨b, isLt_1⟩ : Fin (n + 1 + 1)) = 0
have inl : ∀ (h₁ : k ≤ j) (h₂ : k = a) (h₃ : j + 1 = b), a = 0 → ¬b = 0
Tactic: simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢
Cleared hypotheses: h₁, h₂, 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₁_1 : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂_2 : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃_1 :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂_2)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt : a < n + 2 + 1
b : ℕ
isLt_1 : b < n + 1 + 1
j : ℕ
isLt_2 : j < n + 1
k : ℕ
isLt_3 : k < n + 2
h₁ : (⟨k, isLt_3⟩ : Fin (n + 2)) ≤ ⟨j, isLt_2⟩.castSucc
h₂ : (⟨k, isLt_3⟩ : Fin (n + 2)).castSucc = ⟨a, isLt⟩
h₃ : (⟨j, isLt_2⟩ : Fin (n + 1)).succ = ⟨b, isLt_1⟩
⊢ (⟨a, isLt⟩ : Fin (n + 2 + 1)) = Fin.last (n + 2) → ¬(⟨b, isLt_1⟩ : Fin (n + 1 + 1)) = Fin.last (n + 1)
have inl : ∀ (h₁ : k ≤ j) (h₂ : k = a) (h₃ : j + 1 = b), a = n + 2 → ¬b = n + 1
Tactic: simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢
Cleared hypotheses: h₁, h₂, 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₁_1 : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂_2 : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃_1 :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂_2)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt : a < n + 2 + 1
b : ℕ
isLt_1 : b < n + 1 + 1
j : ℕ
isLt_2 : j < n + 1
k : ℕ
isLt_3 : k < n + 2
h₁ : (⟨j, isLt_2⟩ : Fin (n + 1)).castSucc < ⟨k, isLt_3⟩
h₂ : (⟨k, isLt_3⟩ : Fin (n + 2)).succ = ⟨a, isLt⟩
h₃ : (⟨j, isLt_2⟩ : Fin (n + 1)).castSucc = ⟨b, isLt_1⟩
a_1 : Fin (n + 2 + 1)
b_1 : Fin (n + 1 + 1)
i : ℕ
isLt_4 : i < n + 1
h₄ : (⟨i, isLt_4⟩ : Fin (n + 1)).castSucc.succ = a_1
h₅ : (⟨i, isLt_4⟩ : Fin (n + 1)).succ = b_1
⊢ (⟨a, isLt⟩ : Fin (n + 2 + 1)) = a_1 → ¬(⟨b, isLt_1⟩ : Fin (n + 1 + 1)) = b_1
have inr : ∀ (h₁ : j < k) (h₂ : k + 1 = a) (h₃ : j = b), a = (↑a_1 : ℕ) → ¬b = (↑b_1 : ℕ)
Tactic: simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢
Cleared hypotheses: h₁, h₂, 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₁_1 : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂_2 : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃_1 :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂_2)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt : a < n + 2 + 1
b : ℕ
isLt_1 : b < n + 1 + 1
j : ℕ
isLt_2 : j < n + 1
k : ℕ
isLt_3 : k < n + 2
h₁ : (⟨j, isLt_2⟩ : Fin (n + 1)).castSucc < ⟨k, isLt_3⟩
h₂ : (⟨k, isLt_3⟩ : Fin (n + 2)).succ = ⟨a, isLt⟩
h₃ : (⟨j, isLt_2⟩ : Fin (n + 1)).castSucc = ⟨b, isLt_1⟩
a_1 : Fin (n + 2 + 1)
b_1 : Fin (n + 1 + 1)
i : ℕ
isLt_4 : i < n + 1
h₄ : (⟨i, isLt_4⟩ : Fin (n + 1)).castSucc.succ = a_1
h₅ : (⟨i, isLt_4⟩ : Fin (n + 1)).castSucc = b_1
⊢ (⟨a, isLt⟩ : Fin (n + 2 + 1)) = a_1 → ¬(⟨b, isLt_1⟩ : Fin (n + 1 + 1)) = b_1
have inr : ∀ (h₁ : j < k) (h₂ : k + 1 = a) (h₃ : j = b), a = (↑a_1 : ℕ) → ¬b = (↑b_1 : ℕ)
Tactic: simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢
Cleared hypotheses: h₁, h₂, 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₁_1 : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂_2 : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃_1 :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂_2)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt : a < n + 2 + 1
b : ℕ
isLt_1 : b < n + 1 + 1
j : ℕ
isLt_2 : j < n + 1
k : ℕ
isLt_3 : k < n + 2
h₁ : (⟨j, isLt_2⟩ : Fin (n + 1)).castSucc < ⟨k, isLt_3⟩
h₂ : (⟨k, isLt_3⟩ : Fin (n + 2)).succ = ⟨a, isLt⟩
h₃ : (⟨j, isLt_2⟩ : Fin (n + 1)).castSucc = ⟨b, isLt_1⟩
⊢ (⟨a, isLt⟩ : Fin (n + 2 + 1)) = 0 → ¬(⟨b, isLt_1⟩ : Fin (n + 1 + 1)) = 0
have inr : ∀ (h₁ : j < k) (h₂ : k + 1 = a) (h₃ : j = b), a = 0 → ¬b = 0
Tactic: simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢
Cleared hypotheses: h₁, h₂, 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₁_1 : Disjoint (Finset.image γ₁ Sᶜ) (Finset.image γ₂ S)
h₂_2 : Disjoint (Finset.image γ₃ Finset.univ) (Finset.image γ₄ Finset.univ)
h₃_1 :
  Disjoint ((Finset.image γ₃ Finset.univ).disjUnion (Finset.image γ₄ Finset.univ) h₂_2)
    {(0, 0), (Fin.last (n + 2), Fin.last (n + 1))}
a : ℕ
isLt : a < n + 2 + 1
b : ℕ
isLt_1 : b < n + 1 + 1
j : ℕ
isLt_2 : j < n + 1
k : ℕ
isLt_3 : k < n + 2
h₁ : (⟨j, isLt_2⟩ : Fin (n + 1)).castSucc < ⟨k, isLt_3⟩
h₂ : (⟨k, isLt_3⟩ : Fin (n + 2)).succ = ⟨a, isLt⟩
h₃ : (⟨j, isLt_2⟩ : Fin (n + 1)).castSucc = ⟨b, isLt_1⟩
⊢ (⟨a, isLt⟩ : Fin (n + 2 + 1)) = Fin.last (n + 2) → ¬(⟨b, isLt_1⟩ : Fin (n + 1 + 1)) = Fin.last (n + 1)
have inr : ∀ (h₁ : j < k) (h₂ : k + 1 = a) (h₃ : j = b), a = n + 2 → ¬b = n + 1
Tactic: simp [Fin.ext_iff] at h₁ h₂ h₃ ⊢
Cleared hypotheses: h₁, h₂, h₃