awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬Isδ₀ (SimplexCategory.δ j)
⊢ Eq (α := HomologicalComplex.X K[X] (m + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op) 0
have h₃ : ¬j = 0
Tactic: rw [Isδ₀.iff] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ 1 ≤ (↑j : ℕ)
have by_contra : ∀ (h : ¬1 ≤ (↑j : ℕ)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op) 0
have h₃ : 1 ≤ (↑j : ℕ)
Tactic: have h₃ : 1 ≤ (j : ℕ) := by
      by_contra h
      exact h₂ (by simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : ⦋n⦌.len = ⦋m⦌.len + (k + 1) + 1
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
have hk₁ : n = m + k + 1 + 1
Tactic: simp only [← add_assoc] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
h₁ : ⦋m⦌.len ≠ n
k : ℕ
hk : n = m + k + 1 + 1
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0
have mk : ∀ (i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌) (h₁ : ⦋m⦌.len ≠ m + k + 1 + 1),
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map i.op) 0
Tactic: subst hk
Cleared hypotheses: n, i, h₁, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
h :
  Function.Surjective (α := Fin (⦋m⦌.len + 1)) (β := Fin (⦋m + k + 1 + 1⦌.len + 1))
    (⇑(Hom.toOrderHom i) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + k + 1 + 1⦌.len + 1))
⊢ False
have h₂ : Epi i
Tactic: rw [← SimplexCategory.epi_iff_surjective] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map i.op) 0
have mk : ∀ (j₁ : Fin (m + k + 2 + 1)) (i : ⦋m⦌ ⟶ ⦋m + k + 1⦌),
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ j₁).op) 0
Tactic: obtain ⟨j₁ : Fin (_ + 1), i, rfl⟩ :=
      eq_comp_δ_of_not_surjective i fun h => by
        rw [← SimplexCategory.epi_iff_surjective] at h
        grind [→ le_of_epi]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : ⦋m⦌ ⟶ ⦋m + k + 1⦌
h :
  Function.Surjective (α := Fin (⦋m⦌.len + 1)) (β := Fin (⦋m + k + 1⦌.len + 1))
    (⇑(Hom.toOrderHom i) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + k + 1⦌.len + 1))
⊢ False
have h₂ : Epi i
Tactic: rw [← SimplexCategory.epi_iff_surjective] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : ⦋m⦌ ⟶ ⦋m + k + 1⦌
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ j₁).op) 0
have mk : ∀ (j₂ : Fin (m + k + 2)) (i : ⦋m⦌ ⟶ ⦋m + k⦌),
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
Tactic: obtain ⟨j₂, i, rfl⟩ :=
      eq_comp_δ_of_not_surjective i fun h => by
        rw [← SimplexCategory.epi_iff_surjective] at h
        grind [→ le_of_epi]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
have pos : ∀ (hj₁ : j₁ = 0),
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
Tactic: by_cases hj₁ : j₁ = 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
pos :
  ∀ (hj₁ : j₁ = 0),
    Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
      (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
have neg : ∀ (hj₁ : ¬j₁ = 0),
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
Tactic: by_cases hj₁ : j₁ = 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : j₁ = 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
have pos : Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
  (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ 0).op) 0
Tactic: subst hj₁
Cleared hypotheses: j₁, hj₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ 0).op) 0
have pos : Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
  (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫
    X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 sorry) ≫ SimplexCategory.δ j₂.succ).op)
  0
Tactic: rw [assoc, ← SimplexCategory.δ_comp_δ'' (Fin.zero_le _)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫
      X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 ⋯) ≫ SimplexCategory.δ j₂.succ).op)
    0
have pos : Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
  (HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
    X.map (SimplexCategory.δ j₂.succ).op ≫ X.map (SimplexCategory.δ (Fin.castLT 0 sorry)).op ≫ X.map i.op)
  0
Tactic: simp only [op_comp, X.map_comp, assoc, PInfty_f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₂.succ).op ≫ X.map (SimplexCategory.δ (Fin.castLT 0 ⋯)).op ≫ X.map i.op)
    0
have pos : m + k + 1 + 2 ≤ (↑j₂.succ : ℕ) + (m + k + 1 + 1)
Tactic: erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ j₂.succ_ne_zero, zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ m + k + 1 + 2 ≤ (↑j₂.succ : ℕ) + (m + k + 1 + 1)
have pos : m + k + 1 + 2 ≤ (↑j₂ : ℕ) + 1 + (m + k + 1 + 1)
Tactic: simp only [Fin.succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
have neg : Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
  (HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
    X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op)
  0
Tactic: simp only [op_comp, X.map_comp, assoc, PInfty_f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op)
    0
have neg : m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)
Tactic: erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ hj₁, zero_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)
have neg : ∀ (this : ¬m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
this : ¬m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)
⊢ j₁ = 0
have simp : (↑j₁ : ℕ) = 0
Tactic: simp only [Fin.ext_iff, Fin.val_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
⊢ Eq (α := HomologicalComplex.X K[X] Δ'.len ⟶ HomologicalComplex.X K[X] Δ.len)
    (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty Δ.len)
    (HomologicalComplex.Hom.f PInfty Δ'.len ≫ X.map i.op)
have mk : ∀ (n : ℕ) (i : ⦋n⦌ ⟶ Δ') [inst_3 : Mono i],
  Eq (α := HomologicalComplex.X K[X] Δ'.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
    (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty ⦋n⦌.len)
    (HomologicalComplex.Hom.f PInfty Δ'.len ≫ X.map i.op)
Tactic: induction Δ using SimplexCategory.rec with | _ n
Cleared hypotheses: Δ, i, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ' : SimplexCategory
n : ℕ
i : ⦋n⦌ ⟶ Δ'
inst_2 : Mono i
⊢ Eq (α := HomologicalComplex.X K[X] Δ'.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
    (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty ⦋n⦌.len)
    (HomologicalComplex.Hom.f PInfty Δ'.len ≫ X.map i.op)
have mk : ∀ (n' : ℕ) (i : ⦋n⦌ ⟶ ⦋n'⦌) [inst_3 : Mono i],
  Eq (α := HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
    (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty ⦋n⦌.len)
    (HomologicalComplex.Hom.f PInfty ⦋n'⦌.len ≫ X.map i.op)
Tactic: induction Δ' using SimplexCategory.rec with | _ n'
Cleared hypotheses: Δ', i, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
⊢ Eq (α := HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
    (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty ⦋n⦌.len)
    (HomologicalComplex.Hom.f PInfty ⦋n'⦌.len ≫ X.map i.op)
have mk : Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y := X _⦋n⦌)
      (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
      (HomologicalComplex.Hom.f PInfty n) :
    X _⦋n'⦌ ⟶ X _⦋n⦌)
  (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have pos : ∀ (h : n = n'),
  Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
Tactic: by_cases h : n = n'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
pos :
  ∀ (h : n = n'),
    Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
          (HomologicalComplex.Hom.f PInfty n) :
        X _⦋n'⦌ ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have neg : ∀ (h : ¬n = n'),
  Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
Tactic: by_cases h : n = n'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : n = n'
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have pos : ∀ (i : ⦋n⦌ ⟶ ⦋n⦌) [inst_3 : Mono i],
  Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op : X _⦋n⦌ ⟶ X _⦋n⦌)
Tactic: subst h
Cleared hypotheses: n', i, inst_2, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n⦌
inst_2 : Mono i
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op : X _⦋n⦌ ⟶ X _⦋n⦌)
have pos : 𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n =
  CategoryStruct.comp (Y := X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌))
Tactic: simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n⦌
inst_2 : Mono i
⊢ 𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n =
    CategoryStruct.comp (Y := X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌))
have pos : Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n : X _⦋n⦌ ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y := X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌)) :
    X _⦋n⦌ ⟶ X _⦋n⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have pos : ∀ (hi : Isδ₀ i),
  Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
Tactic: by_cases hi : Isδ₀ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
pos :
  ∀ (hi : Isδ₀ i),
    Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
          (HomologicalComplex.Hom.f PInfty n) :
        X _⦋n'⦌ ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have neg : ∀ (hi : ¬Isδ₀ i),
  Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
Tactic: by_cases hi : Isδ₀ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : Isδ₀ i
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have h' : n' = n + 1
Tactic: have h' : n' = n + 1 := hi.left
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
hi : Isδ₀ i
h' : n' = n + 1
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
have pos : ∀ (i : ⦋n⦌ ⟶ ⦋n + 1⦌) [inst_3 : Mono i] (h : ¬n = n + 1) (hi : Isδ₀ i),
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n + 1⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n + 1⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op : X _⦋n + 1⦌ ⟶ X _⦋n⦌)
Tactic: subst h'
Cleared hypotheses: n', i, inst_2, h, hi, h'