awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
h : m < n
mp :
  (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) →
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x
⊢ (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) ↔
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x
have mpr : (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set (X.op _⦋n⦌))
      (Set.range (ι := X.op _⦋m⦌)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
      x) →
  ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
      (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
      ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
h : m < n
⊢ (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌)) →
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        x
have mp : ∀ (x : X _⦋n⦌),
  (∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌))
        (Set.range (ι := X _⦋m⦌) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) : (a : X _⦋m⦌) → X _⦋n⦌))
        ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) ((Equiv.symm opObjEquiv : (a : X _⦋n⦌) → X.op _⦋n⦌) x : X.op _⦋n⦌) :
          X _⦋n⦌)) →
    ∃ (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (α := X.op _⦋n⦌) (γ := Set (X.op _⦋n⦌))
        (Set.range (ι := X.op _⦋m⦌)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op)) : (a : X.op _⦋m⦌) → X.op _⦋n⦌))
        ((Equiv.symm opObjEquiv : (a : X _⦋n⦌) → X.op _⦋n⦌) x : X.op _⦋n⦌)
Tactic: obtain ⟨x, rfl⟩ := opObjEquiv.symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
⊢ Eq (α := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
have h : ∀ (x : X _⦋n + 1⦌),
  Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x ↔
    Membership.mem (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x ↔
    Membership.mem (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      x
have h : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x →
  Membership.mem (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
h :
  Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x →
    Membership.mem (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      x
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x ↔
    Membership.mem (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      x
have h₁ : Membership.mem (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    x →
  Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    x
have hx₁ : ∃ (m : ℕ) (_ : m < n + 1) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f),
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    (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 + 1⦌)))
    x
Tactic: rw [mem_degenerate_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx :
  ∃ (m : ℕ) (_ : m < n + 1) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      (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 + 1⦌)))
      x
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    x
have h : ∀ (m : ℕ) (hm : m < n + 1) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (hf : Epi f) (y : X _⦋m⦌),
  Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 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 + 1⦌))
        y :
      (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
Tactic: obtain ⟨m, hm, f, hf, y, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf_1 : Epi f
y : X _⦋m⦌
hf :
  Function.Injective (α := Fin (⦋n + 1⦌.len + 1)) (β := Fin (⦋m⦌.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋m⦌.len + 1))
⊢ False
have hf₁ : Mono f
Tactic: rw [← SimplexCategory.mono_iff_injective] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf_1 : Epi f
y : X _⦋m⦌
hf : Mono f
⊢ False
have this : n + 1 ≤ m
Tactic: have := SimplexCategory.le_of_mono f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf : Epi f
y : X _⦋m⦌
⊢ Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 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 + 1⦌))
        y :
      (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
have h : ∀ (i : Fin (n + 1)) (θ : ⦋n⦌ ⟶ ⦋m⦌) (hf : Epi (SimplexCategory.σ i ≫ θ)),
  Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i ≫ θ).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
        y :
      (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
Tactic: obtain ⟨i, θ, rfl⟩ := SimplexCategory.eq_σ_comp_of_not_injective f (fun hf ↦ by
      rw [← SimplexCategory.mono_iff_injective] at hf
      have := SimplexCategory.le_of_mono f
      lia)
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx :
  Membership.mem (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    x
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x
have hx₁ : ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
Tactic: simp only [Set.mem_iUnion, Set.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx :
  ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x
have h : ∀ (i : Fin (n + 1)) (y : X _⦋n⦌),
  Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y : X _⦋n + 1⦌)
Tactic: obtain ⟨i, y, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      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⦌)
x : X _⦋n + 1⦌
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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 + 1⦌))
        (↑y : X _⦋m⦌)
have pos : ∀ (hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x),
  ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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 + 1⦌))
        (↑y : X _⦋m⦌)
Tactic: by_cases hx : x ∈ X.nonDegenerate (n + 1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      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⦌)
x : X _⦋n + 1⦌
pos :
  ∀ (hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x),
    ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      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 + 1⦌))
          (↑y : X _⦋m⦌)
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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 + 1⦌))
        (↑y : X _⦋m⦌)
have neg : ∀ (hx : x ∉ X.nonDegenerate (n + 1)),
  ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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 + 1⦌))
        (↑y : X _⦋m⦌)
Tactic: by_cases hx : x ∈ X.nonDegenerate (n + 1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (hypothesis)
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      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⦌)
x : X _⦋n + 1⦌
hx : x ∉ X.nonDegenerate (n + 1)
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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 + 1⦌))
        (↑y : X _⦋m⦌)
have hx₁ : ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
Tactic: simp only [← mem_degenerate_iff_notMem_nonDegenerate,
          degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      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⦌)
x : X _⦋n + 1⦌
hx :
  ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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 + 1⦌))
        (↑y : X _⦋m⦌)
have neg : ∀ (i : Fin (n + 1)) (y : X _⦋n⦌),
  ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y_1 : (↑(X.nonDegenerate m) : Type u)),
    Eq (α := X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y : X _⦋n + 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 + 1⦌))
          (↑y_1 : X _⦋m⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
Tactic: obtain ⟨i, y, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      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⦌)
i : Fin (n + 1)
y : X _⦋n⦌
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y_1 : (↑(X.nonDegenerate m) : Type u)),
    Eq (α := X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y : X _⦋n + 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 + 1⦌))
          (↑y_1 : X _⦋m⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
have neg : ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (hf : Epi f) (z : (↑(X.nonDegenerate m) : Type u)),
  ∃ (m_1 : ℕ) (f_1 : ⦋n + 1⦌ ⟶ ⦋m_1⦌) (_ : Epi f_1) (y : (↑(X.nonDegenerate m_1) : Type u)),
    Eq (α := X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 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⦌))
              (↑z : X _⦋m⦌) :
            (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
        X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m_1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
          (↑y : X _⦋m_1⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
Tactic: obtain ⟨m, f, hf, z, rfl⟩ := hn y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      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⦌)
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : (↑(X.nonDegenerate m) : Type u)
⊢ Eq (α := X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 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⦌))
            (↑z : X _⦋m⦌) :
          (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
      X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i ≫ f).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
        (↑z : X _⦋m⦌) :
      (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
have simp : Eq (α := X _⦋n + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑z : X _⦋m⦌) : X _⦋n⦌) :
    X _⦋n + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑z : X _⦋m⦌) : X _⦋n⦌) :
    X _⦋n + 1⦌)
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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⦌)
have zero : ∀ (x : X _⦋0⦌),
  ∃ (m : ℕ) (f : ⦋0⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (↑y : X _⦋m⦌)
Tactic: induction n with
  | zero =>
      exact ⟨0, 𝟙 _, inferInstance, ⟨x, by simp⟩, by simp⟩
  | succ n hn =>
      by_cases hx : x ∈ X.nonDegenerate (n + 1)
      · exact ⟨n + 1, 𝟙 _, inferInstance, ⟨x, hx⟩, by simp⟩
      · simp only [← mem_degenerate_iff_notMem_nonDegenerate,
          degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx
        obtain ⟨i, y, rfl⟩ := hx
        obtain ⟨m, f, hf, z, rfl⟩ := hn y
        exact ⟨_, SimplexCategory.σ i ≫ f, inferInstance, z, by simp; rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Degenerate (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
zero :
  ∀ (x : X _⦋0⦌),
    ∃ (m : ℕ) (f : ⦋0⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
          (↑y : X _⦋m⦌)
⊢ ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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⦌)
have succ : ∀ (n : ℕ)
  (hn :
    ∀ (x : X _⦋n⦌),
      ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
        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⦌))
  (x : X _⦋n + 1⦌),
  ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    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 + 1⦌))
        (↑y : X _⦋m⦌)
Tactic: induction n with
  | zero =>
      exact ⟨0, 𝟙 _, inferInstance, ⟨x, by simp⟩, by simp⟩
  | succ n hn =>
      by_cases hx : x ∈ X.nonDegenerate (n + 1)
      · exact ⟨n + 1, 𝟙 _, inferInstance, ⟨x, hx⟩, by simp⟩
      · simp only [← mem_degenerate_iff_notMem_nonDegenerate,
          degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx
        obtain ⟨i, y, rfl⟩ := hx
        obtain ⟨m, f, hf, z, rfl⟩ := hn y
        exact ⟨_, SimplexCategory.σ i ≫ f, inferInstance, z, by simp; rfl⟩
Cleared hypotheses: x
-- 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
inst : Epi f
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⦌)
⊢ IsIso f
have obtain : ∀ (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
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x, hy