awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
m : SimplexCategory
f : ⦋n⦌ ⟶ m
inst : Epi f
y : X.obj (op m)
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)
⊢ IsIso f
have mk : ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) [Epi f] (y : X _⦋m⦌)
  (hy :
    (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 =
      (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)),
  IsIso f
Tactic: induction m using SimplexCategory.rec with | _ m
Cleared hypotheses: m, f, inst, y, hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)
⊢ IsIso f
have mk : ∀ (hx_1 : x ∉ X.degenerate n) (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) [Epi f] (y : X _⦋m⦌)
  (hy :
    (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 =
      (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)),
  IsIso f
Tactic: rw [mem_nonDegenerate_iff_notMem_degenerate] at hx
Cleared hypotheses: m, f, inst, y, hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
⊢ IsIso f
have mk : ∀ (hf : ¬IsIso f), False
Tactic: by_contra hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
hf : ¬IsIso f
⊢ False
have mk : ∀ (h : n ≤ m), IsIso f
Tactic: refine hx ⟨_, not_le.1 (fun h ↦ hf ?_), f, y, hy⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
hf : ¬IsIso f
h : n ≤ m
⊢ IsIso f
have mk : ⦋n⦌.len = ⦋m⦌.len
Tactic: rw [SimplexCategory.isIso_iff_of_epi]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage f))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op (image f)))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι f))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X.obj (op (image f))))
          y :
        (fun (X : Type u) ↦ X) (X.obj (op (image f)))) =
    (↑x : X _⦋n⦌)
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := X.obj (op (image f))) (X.map (Quiver.Hom.op (image.ι f)))
          (X.map (Quiver.Hom.op (factorThruImage f)))) :
      (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
    y =
  (↑x : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := X.obj (op (image f))) (X.map (Quiver.Hom.op (image.ι f)))
            (X.map (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage f))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op (image f)))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι f))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X.obj (op (image f))))
          y :
        (fun (X : Type u) ↦ X) (X.obj (op (image f)))) =
    (↑x : X _⦋n⦌)
have rw₁ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map
          (CategoryStruct.comp (Y := op (image f)) (Quiver.Hom.op (image.ι f)) (Quiver.Hom.op (factorThruImage f)))) :
      (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
    y =
  (↑x : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := X.obj (op (image f))) (X.map (Quiver.Hom.op (image.ι f)))
            (X.map (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (CategoryStruct.comp (Y := op (image f)) (Quiver.Hom.op (image.ι f)) (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage f))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op (image f)))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι f))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X.obj (op (image f))))
          y :
        (fun (X : Type u) ↦ X) (X.obj (op (image f)))) =
    (↑x : X _⦋n⦌)
have rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)).op) :
      (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
    y =
  (↑x : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := X.obj (op (image f))) (X.map (Quiver.Hom.op (image.ι f)))
            (X.map (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map
            (CategoryStruct.comp (Y := op (image f)) (Quiver.Hom.op (image.ι f)) (Quiver.Hom.op (factorThruImage f)))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
rw₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌)
      y =
    (↑x : X _⦋n⦌)
rw₃ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → X _⦋n⦌) y =
    (↑x : X _⦋n⦌)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (factorThruImage f))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op (image f)))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (image.ι f))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X.obj (op (image f))))
          y :
        (fun (X : Type u) ↦ X) (X.obj (op (image f)))) =
    (↑x : X _⦋n⦌)
have rw₄ : (↑x : X _⦋n⦌) = (↑x : X _⦋n⦌)
Tactic: rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
⊢ Mono f
have this : IsIso (Y := image f) (factorThruImage f)
Tactic: have := X.isIso_of_nonDegenerate x (factorThruImage f) (y := X.map (image.ι f).op y) (by
      rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy])
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
this : IsIso (Y := image f) (factorThruImage f)
⊢ Mono f
have rw : Mono (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f))
Tactic: rw [← image.fac f]
-- 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₂
⊢ (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₁⦌)
have dsimp : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (f₂.op ≫ hf₁.section_.op)) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
  (↑y₁ : X _⦋m₁⦌)
Tactic: dsimp [g]
-- 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₂
⊢ (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 f₂.op ≫ X.map hf₁.section_.op) : (a : X _⦋m₂⦌) → X _⦋m₁⦌) y₂ =
  (↑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₁⦌)
⊢ (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 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₁⦌)
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₁⦌)
⊢ (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 hf₁.section_.op) : (a : X _⦋n⦌) → X _⦋m₁⦌) x = (↑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₁⦌)
⊢ (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 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₁⦌)
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₁⦌)
⊢ (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 f₁.op ≫ X.map hf₁.section_.op) :
      (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₁⦌)
⊢ (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 (f₁.op ≫ hf₁.section_.op)) :
      (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₁⦌)
⊢ (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 (hf₁.section_ ≫ f₁).op) :
      (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]