awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
k : Fin (n + 3)
hk : k ≠ i
j : Fin (n + 2)
hj : j.castSucc ≠ i
hjk : j.castSucc < k
⊢ stdSimplex.δ (k.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k hk
have succ : ∀ (k : Fin (n + 2)) (hk : k.succ ≠ i) (hjk : j.castSucc < k.succ),
  stdSimplex.δ (k.succ.pred sorry) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred sorry) ≫ ι i k.succ hk
Tactic: obtain ⟨k, rfl⟩ := k.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hjk)
Cleared hypotheses: k, hk, hjk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
have succ : (stdSimplex.δ (k.succ.pred sorry) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
  (stdSimplex.δ (j.castSucc.castPred sorry) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
Tactic: rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
succ :
  (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
have succ₁ : stdSimplex.δ (k.succ.pred sorry) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
  (stdSimplex.δ (j.castSucc.castPred sorry) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
Tactic: rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
succ :
  (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₁ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
have succ₂ : stdSimplex.δ (k.succ.pred sorry) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
  stdSimplex.δ (j.castSucc.castPred sorry) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
Tactic: rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
succ :
  (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₁ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₂ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
have succ₃ : stdSimplex.δ (k.succ.pred sorry) ≫ stdSimplex.δ j.castSucc =
  stdSimplex.δ (j.castSucc.castPred sorry) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
Tactic: rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
succ :
  (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₁ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₂ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₃ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
have succ₄ : stdSimplex.δ (k.succ.pred sorry) ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred sorry) ≫ stdSimplex.δ k.succ
Tactic: rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
succ :
  (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₁ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₂ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₃ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₄ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
have succ₅ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred sorry) ≫ stdSimplex.δ k.succ
Tactic: rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
succ :
  (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₁ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₂ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₃ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₄ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ
succ₅ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
have succ₆ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ j ≫ stdSimplex.δ k.succ
Tactic: rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
succ :
  (stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj) ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₁ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    (stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk) ≫ Λ[n + 1 + 1, i].ι
succ₂ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj ≫ Λ[n + 1 + 1, i].ι =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₃ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc =
    stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk ≫ Λ[n + 1 + 1, i].ι
succ₄ :
  stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ
succ₅ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ
succ₆ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ j ≫ stdSimplex.δ k.succ
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ ι i j.castSucc hj = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ ι i k.succ hk
have succ₇ : stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ k ≫ stdSimplex.δ j.castSucc
Tactic: rw [← cancel_mono (Subcomplex.ι _), Category.assoc, Category.assoc, ι_ι, ι_ι,
      Fin.pred_succ, Fin.castPred_castSucc, stdSimplex.δ_comp_δ (by grind)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ ι i j hj ≫ (isColimit i).desc hf.multicofork = f j hj
have rw : (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hj ≫ (isColimit i).desc hf.multicofork =
  (stdSimplex.faceSingletonComplIso j).inv ≫ f j hj
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso j).inv]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ι₀ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₀
have rw : horn.faceι 1 0 ι₀._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 0) ≫ f₀
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 0).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ι₂ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₂
have rw : horn.faceι 1 2 ι₂._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 2) ≫ f₂
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 2).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ ι₃ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₃
have rw : horn.faceι 1 3 ι₃._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 3) ≫ f₃
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 3).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ι₀ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₀
have rw : horn.faceι 2 0 ι₀._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 0) ≫ f₀
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 0).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁
have rw : horn.faceι 2 1 ι₁._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 1) ≫ f₁
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 1).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
Goal:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ι₃ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₃
have rw : horn.faceι 2 3 ι₃._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = Iso.inv (stdSimplex.faceSingletonComplIso 3) ≫ f₃
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 3).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
⊢ φ ≫ s.map = const x
have refine : Subcomplex.range φ ≤ ∂Δ[n]
Tactic: refine (Subcomplex.lift φ ?_) ≫= s.comm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
⊢ Subcomplex.range φ ≤ ∂Δ[n]
have rw : Subcomplex.range φ ≠ ⊤
Tactic: rw [stdSimplex.le_boundary_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ IsIso (Subcomplex.range φ).ι
have rw : IsIso.{u, u + 1} (X := Subcomplex.toSSet (X := Δ[n]) ⊤) (Subcomplex.ι ⊤)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ False
have this : IsIso (Subcomplex.range φ).ι
Tactic: have : IsIso (Subcomplex.range φ).ι := by rw [h]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
⊢ stdSimplex.δ i.castSucc ≫ stdSimplex.σ i ≫ f.map = f.map
have rw : f.map = f.map
Tactic: rw [CosimplicialObject.δ_comp_σ_self_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
⊢ stdSimplex.δ i.succ ≫ stdSimplex.σ i ≫ f.map = f.map
have rw : f.map = f.map
Tactic: rw [CosimplicialObject.δ_comp_σ_succ_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
j : Fin (n + 2)
hj : j < i.castSucc
⊢ stdSimplex.δ j ≫ stdSimplex.σ i ≫ f.map = const x
have obtain : ∀ (i : Fin n) (hj : j < i.succ.castSucc), stdSimplex.δ j ≫ stdSimplex.σ i.succ ≫ f.map = const x
Tactic: obtain ⟨i, rfl⟩ := i.eq_succ_of_ne_zero (by aesop)
Cleared hypotheses: i, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
j : Fin (n + 2)
i : Fin n
hj : j < i.succ.castSucc
⊢ stdSimplex.δ j ≫ stdSimplex.σ i.succ ≫ f.map = const x
have obtain : ∀ (j : Fin (n + 1)) (hj : j.castSucc < i.succ.castSucc), stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
Tactic: obtain ⟨j, rfl⟩ := j.eq_castSucc_of_ne_last (by grind)
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin n
j : Fin (n + 1)
hj : j.castSucc < i.succ.castSucc
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
have zero : ∀ (f : X.PtSimplex 0 x) (i : Fin 0) (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hj : j.castSucc < i.succ.castSucc),
  stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
Tactic: obtain _ | n := n
Cleared hypotheses: n, f, i, j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin n
j : Fin (n + 1)
hj : j.castSucc < i.succ.castSucc
zero :
  ∀ (f : X.PtSimplex 0 x) (i : Fin 0) (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hj : j.castSucc < i.succ.castSucc),
    stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
have succ : ∀ (n : ℕ) (f : X.PtSimplex (n + 1) x) (i : Fin (n + 1)) (j : Fin (n + 1 + 1)) (hj : j.castSucc < i.succ.castSucc),
  stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
Tactic: obtain _ | n := n
Cleared hypotheses: n, f, i, j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
have succ : stdSimplex.σ i ≫ stdSimplex.δ j ≫ f.map = const x
Tactic: rw [stdSimplex.δ_comp_σ_of_le_assoc (by grind), δ_map, comp_const]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
succ : stdSimplex.σ i ≫ stdSimplex.δ j ≫ f.map = const x
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
have succ₁ : stdSimplex.σ i ≫ const x = const x
Tactic: rw [stdSimplex.δ_comp_σ_of_le_assoc (by grind), δ_map, comp_const]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
succ : stdSimplex.σ i ≫ stdSimplex.δ j ≫ f.map = const x
succ₁ : stdSimplex.σ i ≫ const x = const x
⊢ stdSimplex.δ j.castSucc ≫ stdSimplex.σ i.succ ≫ f.map = const x
have succ₂ : Eq (α := Δ[n + 1] ⟶ X) (const x) (const x)
Tactic: rw [stdSimplex.δ_comp_σ_of_le_assoc (by grind), δ_map, comp_const]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
j : Fin (n + 2)
hj : i.succ < j
⊢ stdSimplex.δ j ≫ stdSimplex.σ i ≫ f.map = const x
have obtain : ∀ (i : Fin n) (hj : i.castSucc.succ < j), stdSimplex.δ j ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
Tactic: obtain ⟨i, rfl⟩ := i.eq_castSucc_of_ne_last (by grind)
Cleared hypotheses: i, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
j : Fin (n + 2)
i : Fin n
hj : i.castSucc.succ < j
⊢ stdSimplex.δ j ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
have obtain : ∀ (j : Fin (n + 1)) (hj : i.castSucc.succ < j.succ), stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
Tactic: obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (by aesop)
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin n
j : Fin (n + 1)
hj : i.castSucc.succ < j.succ
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
have zero : ∀ (f : X.PtSimplex 0 x) (i : Fin 0) (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hj : i.castSucc.succ < j.succ),
  stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
Tactic: obtain _ | n := n
Cleared hypotheses: n, f, i, j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin n
j : Fin (n + 1)
hj : i.castSucc.succ < j.succ
zero :
  ∀ (f : X.PtSimplex 0 x) (i : Fin 0) (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hj : i.castSucc.succ < j.succ),
    stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
have succ : ∀ (n : ℕ) (f : X.PtSimplex (n + 1) x) (i : Fin (n + 1)) (j : Fin (n + 1 + 1)) (hj : i.castSucc.succ < j.succ),
  stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
Tactic: obtain _ | n := n
Cleared hypotheses: n, f, i, j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : i.castSucc.succ < j.succ
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
have succ : stdSimplex.σ i ≫ stdSimplex.δ j ≫ f.map = const x
Tactic: rw [stdSimplex.δ_comp_σ_of_gt_assoc (by grind), δ_map, comp_const]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : i.castSucc.succ < j.succ
succ : stdSimplex.σ i ≫ stdSimplex.δ j ≫ f.map = const x
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
have succ₁ : stdSimplex.σ i ≫ const x = const x
Tactic: rw [stdSimplex.δ_comp_σ_of_gt_assoc (by grind), δ_map, comp_const]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : i.castSucc.succ < j.succ
succ : stdSimplex.σ i ≫ stdSimplex.δ j ≫ f.map = const x
succ₁ : stdSimplex.σ i ≫ const x = const x
⊢ stdSimplex.δ j.succ ≫ stdSimplex.σ i.castSucc ≫ f.map = const x
have succ₂ : Eq (α := Δ[n + 1] ⟶ X) (const x) (const x)
Tactic: rw [stdSimplex.δ_comp_σ_of_gt_assoc (by grind), δ_map, comp_const]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ stdSimplex.δ i.castSucc ≫ r.map = f'.map
have rw : f.map = f'.map
Tactic: rw [δ_castSucc_map, hf]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
rw : f.map = f'.map
⊢ stdSimplex.δ i.castSucc ≫ r.map = f'.map
have rw₁ : f'.map = f'.map
Tactic: rw [δ_castSucc_map, hf]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ stdSimplex.δ i.succ ≫ r.map = g'.map
have rw : g.map = g'.map
Tactic: rw [δ_succ_map, hg]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
rw : g.map = g'.map
⊢ stdSimplex.δ i.succ ≫ r.map = g'.map
have rw₁ : g'.map = g'.map
Tactic: rw [δ_succ_map, hg]