awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ'.len + 1))
zero :
  ∀ (θ : ⦋0⦌ ⟶ Δ')
    (hθ :
      ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
          (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))),
    Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
      (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty 0 : X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
      (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0)
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n : X.obj (Opposite.op Δ') ⟶ X _⦋n⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n)
have succ : ∀ (n : ℕ) (θ : ⦋n + 1⦌ ⟶ Δ')
  (hθ :
    ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))),
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: cases n
Cleared hypotheses: n, θ, hθ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty 0 : X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0)
have zero : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
⊢ False
have zero : Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
  (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
Tactic: apply hθ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
x y : Fin (⦋0⦌.len + 1)
h :
  Eq (α := Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
⊢ x = y
have zero : ∀
  (h :
    Eq (α := Fin (Δ'.len + 1))
      ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩) :
        Fin (Δ'.len + 1))
      ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))),
  (fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩ = y
Tactic: fin_cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
θ : ⦋0⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
y : Fin (⦋0⦌.len + 1)
h :
  Eq (α := Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
        ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      Fin (Δ'.len + 1))
    ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1)) y : Fin (Δ'.len + 1))
⊢ (fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩ = y
have zero : ∀
  (h :
    Eq (α := Fin (Δ'.len + 1))
      ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
        ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
      ((SimplexCategory.Hom.toOrderHom θ : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))
        ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩))),
  Eq (α := Fin (⦋0⦌.len + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have succ : ∀ (i : Fin (n + 1)) (α : ⦋n⦌ ⟶ Δ') (h : θ = SimplexCategory.σ i ≫ α),
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
i : Fin (n + 1)
α : ⦋n⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have succ : Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (X.map (SimplexCategory.σ i ≫ α).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
i : Fin (n + 1)
α : ⦋n⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
succ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (SimplexCategory.σ i ≫ α).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have succ₁ : Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (X.map (α.op ≫ (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
    X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
i : Fin (n + 1)
α : ⦋n⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
succ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (SimplexCategory.σ i ≫ α).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₁ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (α.op ≫ (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have succ₂ : Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  ((X.map α.op ≫ X.map (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
    X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
i : Fin (n + 1)
α : ⦋n⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
succ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (SimplexCategory.σ i ≫ α).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₁ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (α.op ≫ (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₂ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    ((X.map α.op ≫ X.map (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have succ₃ : Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (X.map α.op ≫ X.map (SimplexCategory.σ i).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
    X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
i : Fin (n + 1)
α : ⦋n⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
succ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (SimplexCategory.σ i ≫ α).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₁ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (α.op ≫ (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₂ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    ((X.map α.op ≫ X.map (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₃ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map α.op ≫ X.map (SimplexCategory.σ i).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have succ₄ : Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (X.map α.op ≫ X.σ i ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
  (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
Tactic: rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
i : Fin (n + 1)
α : ⦋n⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
succ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (SimplexCategory.σ i ≫ α).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₁ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (α.op ≫ (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₂ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    ((X.map α.op ≫ X.map (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₃ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map α.op ≫ X.map (SimplexCategory.σ i).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₄ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map α.op ≫ X.σ i ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have succ₅ : Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌) (X.map α.op ≫ 0) 0
Tactic: rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
θ : ⦋n + 1⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1))
i : Fin (n + 1)
α : ⦋n⦌ ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
succ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (SimplexCategory.σ i ≫ α).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₁ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map (α.op ≫ (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₂ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    ((X.map α.op ≫ X.map (SimplexCategory.σ i).op) ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₃ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map α.op ≫ X.map (SimplexCategory.σ i).op ≫ HomologicalComplex.Hom.f PInfty (n + 1) :
      X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₄ :
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map α.op ≫ X.σ i ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
succ₅ : Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌) (X.map α.op ≫ 0) 0
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have succ₆ : Eq.{v_1 + 1} (α := X.obj (Opposite.op Δ') ⟶ X _⦋n + 1⦌) 0 0
Tactic: rw [h, op_comp, X.map_comp, assoc, ← SimplicialObject.σ_def,
      σ_comp_PInfty, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
T : C
f : X _⦋n⦌ ⟶ T
hf : DegeneraciesVanish f
U : C
g : T ⟶ U
⊢ DegeneraciesVanish (f ≫ g)
have zero : ∀ {f : X _⦋0⦌ ⟶ T} (hf : DegeneraciesVanish f), DegeneraciesVanish (f ≫ g)
Tactic: obtain _ | n := n
Cleared hypotheses: n, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
T : C
f : X _⦋n⦌ ⟶ T
hf : DegeneraciesVanish f
U : C
g : T ⟶ U
zero : ∀ {f : X _⦋0⦌ ⟶ T} (hf : DegeneraciesVanish f), DegeneraciesVanish (f ≫ g)
⊢ DegeneraciesVanish (f ≫ g)
have succ : ∀ (n : ℕ) {f : X _⦋n + 1⦌ ⟶ T} (hf : DegeneraciesVanish f), DegeneraciesVanish (f ≫ g)
Tactic: obtain _ | n := n
Cleared hypotheses: n, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
⊢ DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (T := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n)
    (HomologicalComplex.Hom.f PInfty n)
have zero : DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (n := 0) (T := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0)
  (HomologicalComplex.Hom.f PInfty 0)
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
zero :
  DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (n := 0) (T :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0) (HomologicalComplex.Hom.f PInfty 0)
⊢ DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (T := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n)
    (HomologicalComplex.Hom.f PInfty n)
have succ : ∀ (n : ℕ),
  DegeneraciesVanish.{v_1, u_1} (C := C) (X := X) (n := n + 1) (T :=
    HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) (HomologicalComplex.Hom.f PInfty (n + 1))
Tactic: obtain _ | n := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
T : C
f : X _⦋n⦌ ⟶ T
⊢ DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n ⟶ T) (HomologicalComplex.Hom.f QInfty n ≫ f) 0
have zero : ∀ (f : X _⦋0⦌ ⟶ T),
  DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0 ⟶ T) (HomologicalComplex.Hom.f QInfty 0 ≫ f) 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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 : ℕ
T : C
f : X _⦋n⦌ ⟶ T
zero :
  ∀ (f : X _⦋0⦌ ⟶ T),
    DegeneraciesVanish f ↔
      Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0 ⟶ T) (HomologicalComplex.Hom.f QInfty 0 ≫ f) 0
⊢ DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n ⟶ T) (HomologicalComplex.Hom.f QInfty n ≫ f) 0
have succ : ∀ (n : ℕ) (f : X _⦋n + 1⦌ ⟶ T),
  DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
      (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
Tactic: obtain _ | n := n
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
⊢ DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
      (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
have succ : ∀ (hf : DegeneraciesVanish f),
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
succ :
  ∀ (hf : DegeneraciesVanish f),
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
      (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
⊢ DegeneraciesVanish f ↔
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
      (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
have succ₁ : ∀
  (hf :
    Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
      (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0),
  DegeneraciesVanish f
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩