awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ (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 neg : ∀ (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))
      ((SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (m + 1)) → Fin (n + 1)) y) =
    y
Tactic: split_ifs with hy
-- 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)
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
have pos : Eq (α := Fin (m + 1)) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x : Fin (m + 1))
  ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x : Fin (m + 1))
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
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
⊢ ∃ (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 hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
Tactic: have hα₁ (y : Fin (m + 1)) : f₁.toOrderHom (α y) = y := by
    dsimp [α]
    split_ifs with hy
    · rw [hy]
    · apply SimplexCategory.congr_toOrderHom_apply hf.id
-- 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₁_1 : (↑(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₁_1 : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂_1 : (↑(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₂_1 : 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
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
⊢ α y₁ ≤ α y₂
have by_contra! : ∀ (h' : α y₂ < α y₁), False
Tactic: by_contra! h'
-- 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₁_1 : (↑(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₁_1 : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂_1 : (↑(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₂_1 : 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
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
⊢ False
have suffices : y₂ ≤ y₁
Tactic: suffices y₂ ≤ y₁ by simp [show y₁ = y₂ by lia] at h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
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
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
⊢ ∃ (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 hα₂ : Monotone α
Tactic: have hα₂ : Monotone α := by
    rintro y₁ y₂ h
    by_contra! h'
    suffices y₂ ≤ y₁ by simp [show y₁ = y₂ by lia] at h'
    simpa only [hα₁] using f₁.toOrderHom.monotone h'.le
-- 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
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
hα₂ : Monotone α
⊢ SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ : Fin (⦋m⦌.len + 1) →o Fin (⦋n⦌.len + 1) } ≫ f₁ = 𝟙 ⦋m⦌
have a : ∀ (x : Fin (⦋m⦌.len + 1)),
  Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ : Fin (⦋m⦌.len + 1) →o Fin (⦋n⦌.len + 1) } ≫ f₁) :
          (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        x :
      Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom (𝟙 ⦋m⦌) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
⊢ Membership.mem (γ := Set (↑(A.obj (op ⦋n⦌)) : Type u)) (A.toSSet.degenerate n) x ↔ (↑x : X _⦋n⦌) ∈ X.degenerate n
have rw : (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
          (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      x) ↔
  ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
      (↑x : X _⦋n⦌)
Tactic: rw [SSet.mem_degenerate_iff, SSet.mem_degenerate_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
⊢ (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        x) ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
        (↑x : X _⦋n⦌)
have mp : (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
          (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      x) →
  ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
      (↑x : X _⦋n⦌)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
mp :
  (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        x) →
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
        (↑x : X _⦋n⦌)
⊢ (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        x) ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
        (↑x : X _⦋n⦌)
have mpr : (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
      (↑x : X _⦋n⦌)) →
  ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
          (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
⊢ (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
        (↑x : X _⦋n⦌)) →
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        x
have mpr : ∀ (x : X _⦋n⦌) (hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x),
  (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (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⦌)))
        (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x) x hx) : X _⦋n⦌)) →
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x) x hx)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X _⦋m⦌
hx :
  Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((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 :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
⊢ ∃ (m_1 : ℕ) (_ : m_1 < n) (f_1 : ⦋n⦌ ⟶ ⦋m_1⦌) (_ : Epi f_1),
    Membership.mem (α := A.toSSet _⦋n⦌) (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m_1⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f_1.op)) :
          (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m_1⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) 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)
          hx :
        { x : X _⦋n⦌ // Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x })
have mpr : Membership.mem (γ := Set (X _⦋m⦌)) (A.obj (op ⦋m⦌)) y
Tactic: refine ⟨m, hm, f, inferInstance, ⟨y, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X _⦋m⦌
hx :
  Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((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 :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
⊢ Membership.mem (γ := Set (X _⦋m⦌)) (A.obj (op ⦋m⦌)) y
have this : IsSplitEpi f
Tactic: have := isSplitEpi_of_epi f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
⊢ Membership.mem (γ := Set (↑(A.obj (op ⦋n⦌)) : Type u)) (A.toSSet.nonDegenerate n) x ↔
    (↑x : X _⦋n⦌) ∈ X.nonDegenerate n
have rw : x ∉ A.toSSet.degenerate n ↔ (↑x : X _⦋n⦌) ∈ X.nonDegenerate n
Tactic: rw [mem_nonDegenerate_iff_notMem_degenerate,
    mem_nonDegenerate_iff_notMem_degenerate, mem_degenerate_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
rw : x ∉ A.toSSet.degenerate n ↔ (↑x : X _⦋n⦌) ∈ X.nonDegenerate n
⊢ Membership.mem (γ := Set (↑(A.obj (op ⦋n⦌)) : Type u)) (A.toSSet.nonDegenerate n) x ↔
    (↑x : X _⦋n⦌) ∈ X.nonDegenerate n
have rw₁ : x ∉ A.toSSet.degenerate n ↔ (↑x : X _⦋n⦌) ∉ X.degenerate n
Tactic: rw [mem_nonDegenerate_iff_notMem_degenerate,
    mem_nonDegenerate_iff_notMem_degenerate, mem_degenerate_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
rw : x ∉ A.toSSet.degenerate n ↔ (↑x : X _⦋n⦌) ∈ X.nonDegenerate n
rw₁ : x ∉ A.toSSet.degenerate n ↔ (↑x : X _⦋n⦌) ∉ X.degenerate n
⊢ Membership.mem (γ := Set (↑(A.obj (op ⦋n⦌)) : Type u)) (A.toSSet.nonDegenerate n) x ↔
    (↑x : X _⦋n⦌) ∈ X.nonDegenerate n
have rw₂ : (↑x : X _⦋n⦌) ∉ X.degenerate n ↔ (↑x : X _⦋n⦌) ∉ X.degenerate n
Tactic: rw [mem_nonDegenerate_iff_notMem_degenerate,
    mem_nonDegenerate_iff_notMem_degenerate, mem_degenerate_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A B : X.Subcomplex
⊢ A ≤ B ↔
    ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
have mp : A ≤ B →
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A B : X.Subcomplex
mp :
  A ≤ B →
    ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ A ≤ B ↔
    ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
have mpr : (∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)) →
  A ≤ B
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
n : ℕ
x : X _⦋n⦌
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x
have mpr : ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌),
  Epi f →
    ∀ (a : A.toSSet _⦋m⦌) (ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a)
      (ha' :
        Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x) x hx =
          (ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op) :
              (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌))
            (↑(Subtype.mk (p := fun (x : A.toSSet _⦋m⦌) ↦
                  Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) x) a ha) :
              A.toSSet _⦋m⦌)),
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x
Tactic: obtain ⟨m, f, _, ⟨a, ha⟩, ha'⟩ := exists_nonDegenerate A ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
n : ℕ
x : X _⦋n⦌
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a
ha' :
  Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x) x hx =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op) :
        (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌))
      (↑(Subtype.mk (p := fun (x : A.toSSet _⦋m⦌) ↦
            Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) x) a ha) :
        A.toSSet _⦋m⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x
have ha'₁ : x =
  (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
              Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) sorry) :
          (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
        a) :
    X _⦋n⦌)
Tactic: simp only [Subfunctor.toFunctor_obj, Subtype.ext_iff,
      Subfunctor.toFunctor_map] at ha'
Cleared hypotheses: ha'