awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op ≫ X.map hf₁.section_.op) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) : (a : X _⦋m₂⦌) → X _⦋n⦌) y₂ : X _⦋n⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌) x = (↑y₁ : X _⦋m₁⦌)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑y₁ : X _⦋m₁⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n⦌)) =
    (↑y₁ : X _⦋m₁⦌)
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op ≫ X.map hf₁.section_.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₅ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₁.op ≫ hf₁.section_.op)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₆ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (hf₁.section_ ≫ f₁).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₂.op ≫ hf₁.section_.op)) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
have rw₇ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m₁⦌))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
    (↑y₁ : X _⦋m₁⦌) =
  (↑y₁ : X _⦋m₁⦌)
Tactic: rw [Functor.map_comp, comp_apply, ← hy₂, hy₁, ← comp_apply, ← Functor.map_comp, ← op_comp,
    SplitEpi.id, op_id, CategoryTheory.Functor.map_id, id_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op ≫ X.map hf₁.section_.op) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) : (a : X _⦋m₂⦌) → X _⦋n⦌) y₂ : X _⦋n⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌) x = (↑y₁ : X _⦋m₁⦌)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑y₁ : X _⦋m₁⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n⦌)) =
    (↑y₁ : X _⦋m₁⦌)
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op ≫ X.map hf₁.section_.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₅ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₁.op ≫ hf₁.section_.op)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₆ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (hf₁.section_ ≫ f₁).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₇ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m₁⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₂.op ≫ hf₁.section_.op)) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
have rw₈ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (𝟙 (op ⦋m₁⦌))) : (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
    (↑y₁ : X _⦋m₁⦌) =
  (↑y₁ : X _⦋m₁⦌)
Tactic: rw [Functor.map_comp, comp_apply, ← hy₂, hy₁, ← comp_apply, ← Functor.map_comp, ← op_comp,
    SplitEpi.id, op_id, CategoryTheory.Functor.map_id, id_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op ≫ X.map hf₁.section_.op) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) : (a : X _⦋m₂⦌) → X _⦋n⦌) y₂ : X _⦋n⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌) x = (↑y₁ : X _⦋m₁⦌)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑y₁ : X _⦋m₁⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n⦌)) =
    (↑y₁ : X _⦋m₁⦌)
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op ≫ X.map hf₁.section_.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₅ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₁.op ≫ hf₁.section_.op)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₆ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (hf₁.section_ ≫ f₁).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₇ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m₁⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₈ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (𝟙 (op ⦋m₁⦌))) : (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₂.op ≫ hf₁.section_.op)) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
have rw₉ : (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (X _⦋m₁⦌)) : (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
    (↑y₁ : X _⦋m₁⦌) =
  (↑y₁ : X _⦋m₁⦌)
Tactic: rw [Functor.map_comp, comp_apply, ← hy₂, hy₁, ← comp_apply, ← Functor.map_comp, ← op_comp,
    SplitEpi.id, op_id, CategoryTheory.Functor.map_id, id_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op ≫ X.map hf₁.section_.op) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) : (a : X _⦋m₂⦌) → X _⦋n⦌) y₂ : X _⦋n⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌) x = (↑y₁ : X _⦋m₁⦌)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑y₁ : X _⦋m₁⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n⦌)) =
    (↑y₁ : X _⦋m₁⦌)
rw₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op ≫ X.map hf₁.section_.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₅ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₁.op ≫ hf₁.section_.op)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₆ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (hf₁.section_ ≫ f₁).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₇ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋m₁⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₈ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (𝟙 (op ⦋m₁⦌))) : (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
rw₉ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (X _⦋m₁⦌)) : (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → X _⦋m₁⦌)
      (↑y₁ : X _⦋m₁⦌) =
    (↑y₁ : X _⦋m₁⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₂.op ≫ hf₁.section_.op)) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
    (↑y₁ : X _⦋m₁⦌)
have rw₁₀ : (↑y₁ : X _⦋m₁⦌) = (↑y₁ : X _⦋m₁⦌)
Tactic: rw [Functor.map_comp, comp_apply, ← hy₂, hy₁, ← comp_apply, ← Functor.map_comp, ← op_comp,
    SplitEpi.id, op_id, CategoryTheory.Functor.map_id, id_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
⊢ IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))
have this : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (g hf₁ f₂).op) :
      (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋m₁⦌))
    y₂ =
  (↑y₁ : X _⦋m₁⦌)
Tactic: have := map_g_op_y₂ hf₁ hy₁ hy₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (g hf₁ f₂).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋m₁⦌))
      y₂ =
    (↑y₁ : X _⦋m₁⦌)
⊢ IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))
have this₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage (g hf₁ f₂)))) :
      (a : X.obj (op (image (g hf₁ f₂)))) → X _⦋m₁⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι (g hf₁ f₂)))) :
          (a : X _⦋m₂⦌) → X.obj (op (image (g hf₁ f₂))))
        y₂ :
      X.obj (op (image (g hf₁ f₂)))) =
  (↑y₁ : X _⦋m₁⦌)
Tactic: rw [← image.fac (g hf₁ f₂), op_comp, Functor.map_comp, comp_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
⊢ Mono (g hf₁ f₂)
have this : IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))
Tactic: have := isIso_factorThruImage_g hf₁ hy₁ hy₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
this : IsIso (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂))
⊢ Mono (g hf₁ f₂)
have rw : Mono (CategoryStruct.comp (Y := image (g hf₁ f₂)) (factorThruImage (g hf₁ f₂)) (image.ι (g hf₁ f₂)))
Tactic: rw [← image.fac (g hf₁ f₂)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : X _⦋m⦌
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y₂
hf₁ : SplitEpi f₁
⊢ g hf₁ f₂ = 𝟙 ⦋m⦌
have this : Mono (g hf₁ f₂)
Tactic: have := mono_g hf₁ hy₁ hy₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst_1 : Epi f₂
y₂ : (↑(X.nonDegenerate m₂) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m₂⦌)
⊢ m₁ = m₂
have obtain : ∀ (hf₁ : SplitEpi f₁), m₁ = m₂
Tactic: obtain ⟨⟨hf₁⟩⟩ := isSplitEpi_of_epi f₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m₁) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₁⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m₁⦌)
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
inst_1 : Epi f₂
y₂ : (↑(X.nonDegenerate m₂) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m₂⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m₂⦌)
hf₁ : SplitEpi f₁
⊢ m₁ = m₂
have obtain : ∀ (hf₂ : SplitEpi f₂), m₁ = m₂
Tactic: obtain ⟨⟨hf₂⟩⟩ := isSplitEpi_of_epi f₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
⊢ y₁ = y₂
have obtain : ∀ (hf₁ : SplitEpi f₁), y₁ = y₂
Tactic: obtain ⟨⟨hf₁⟩⟩ := isSplitEpi_of_epi f₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
hf₁ : SplitEpi f₁
⊢ y₁ = y₂
have a : (↑y₁ : X _⦋m⦌) = (↑y₂ : X _⦋m⦌)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
⊢ f₁ = f₂
have a : ∀ (x : Fin (⦋n⦌.len + 1)),
  Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
this :
  ∃ (hf₁ : SplitEpi f₁),
    (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
      x
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
have obtain : ∀ (hf₁ : SplitEpi f₁)
  (hf₁' :
    (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
      x),
  Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
Tactic: obtain ⟨hf₁, hf₁'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
have a : ∃ (hf₁ : SplitEpi f₁),
  (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
      ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
    x
Tactic: suffices ∃ (hf₁ : SplitEpi f₁), hf₁.section_.toOrderHom (f₁.toOrderHom x) = x by
    obtain ⟨hf₁, hf₁'⟩ := this
    dsimp at hf₁'
    simpa [g, hf₁'] using (SimplexCategory.congr_toOrderHom_apply (g_eq_id hy₁ hy₂ hf₁)
      (f₁.toOrderHom x)).symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
⊢ ∃ (hf₁ : SplitEpi f₁),
    (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
      x
have a : ∀ (hf : SplitEpi f₁),
  ∃ (hf₁ : SplitEpi f₁),
    (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
      x
Tactic: obtain ⟨⟨hf⟩⟩ := isSplitEpi_of_epi f₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
y : Fin (m + 1)
⊢ (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1))
      (if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x then x
      else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (m + 1)) → Fin (n + 1)) y) =
    y
have pos : ∀ (hy : y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x),
  (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x = y
Tactic: split_ifs with hy