awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
this :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom
          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
a b : Fin (d + 1)
mp :
  LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1)) →
    a ≤ b
⊢ LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1)) ↔
    a ≤ b
have mpr : a ≤ b →
  LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
this :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom
          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
a b : Fin (d + 1)
⊢ LE.le (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1)) →
    a ≤ b
have mp : ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1)) →
  ¬b < a
Tactic: rw [← not_lt, ← not_lt]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
this :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom
          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
a b : Fin (d + 1)
h :
  ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
h' : b < a
⊢ False
have mp : LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
  (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
Tactic: apply h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
this :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom
          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
a b : Fin (d + 1)
h :
  ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
h' : b < a
⊢ LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
have mp : ∀
  (h'' :
    LT.lt (α := Fin (n + 1))
      ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) b)
      ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) a)),
  LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
Tactic: obtain h'' | h'' := (monotone_apply x.val h'.le).lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
x : (↑(Δ[n].nonDegenerate d) : Type u)
this :
  Function.Injective (α := Fin ((unop (op ⦋d⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom
          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → unop (op ⦋d⦌) ⟶ ⦋n⦌) (↑x : Δ[n] _⦋d⦌))) :
      (a : Fin ((unop (op ⦋d⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
a b : Fin (d + 1)
h :
  ¬LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
h' : b < a
mp :
  ∀
    (h'' :
      LT.lt (α := Fin (n + 1))
        ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) b)
        ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) a)),
    LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
      (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
⊢ LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
have mp₁ : ∀
  (h'' :
    Eq (α := Fin (n + 1))
      ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) b)
      ((fun (j : Fin (d + 1)) ↦ (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) j : Fin (n + 1))) a)),
  LT.lt (α := Fin (n + 1)) (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) b : Fin (n + 1))
    (((↑x : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) a : Fin (n + 1))
Tactic: obtain h'' | h'' := (monotone_apply x.val h'.le).lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
S : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)
i : Fin (d + 1)
⊢ Membership.mem (α := Fin (n + 1)) (↑S : Finset (Fin (n + 1)))
    (((↑((Equiv.symm nonDegenerateEquiv' :
                  (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
                S) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
have obtain : ∀ (f : (↑(Δ[n].nonDegenerate d) : Type u)),
  Membership.mem (α := Fin (n + 1)) (γ := Finset (Fin (n + 1)))
    (↑(((nonDegenerateEquiv' : (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
            (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
          f) :
      Finset (Fin (n + 1)))
    (((↑((Equiv.symm nonDegenerateEquiv' :
                  (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
                (((nonDegenerateEquiv' :
                        (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                      (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                    f :
                  (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
Tactic: obtain ⟨f, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
i : Fin (d + 1)
f : (↑(Δ[n].nonDegenerate d) : Type u)
⊢ Membership.mem (α := Fin (n + 1)) (γ := Finset (Fin (n + 1)))
    (↑(((nonDegenerateEquiv' : (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
            (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
          f) :
      Finset (Fin (n + 1)))
    (((↑((Equiv.symm nonDegenerateEquiv' :
                  (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
                (((nonDegenerateEquiv' :
                        (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                      (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                    f :
                  (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
have dsimp : Membership.mem (α := Fin (n + 1)) (γ := Finset (Fin (n + 1)))
  (Finset.image (α := Fin (d + 1))
    (⇑(Hom.toOrderHom
          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑f : Δ[n] _⦋d⦌))) :
      (a : Fin (d + 1)) → Fin (n + 1))
    univ)
  (((↑(((Equiv.ofBijective
                    (fun (x : { x : Δ[n] _⦋d⦌ // Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) x }) ↦
                      Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦ #x = d + 1)
                        (Finset.image (α := Fin (d + 1))
                          (⇑(Hom.toOrderHom
                                (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌)
                                  (↑x : Δ[n] _⦋d⦌))) :
                            (a : Fin (d + 1)) → Fin (n + 1))
                          univ)
                        sorry)
                    sorry).symm :
                (a : { x : Finset (Fin (n + 1)) // #x = d + 1 }) → (↑(Δ[n].nonDegenerate d) : Type u))
              (Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦ #x = d + 1)
                (Finset.image (α := Fin (d + 1))
                  (⇑(Hom.toOrderHom
                        (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌)
                          (↑f : Δ[n] _⦋d⦌))) :
                    (a : Fin (d + 1)) → Fin (n + 1))
                  univ)
                sorry)) :
          Δ[n] _⦋d⦌) :
        (a : Fin (d + 1)) → Fin (n + 1))
      i :
    Fin (n + 1))
Tactic: dsimp [nonDegenerateEquiv']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
i : Fin (d + 1)
f : (↑(Δ[n].nonDegenerate d) : Type u)
⊢ Membership.mem (α := Fin (n + 1)) (γ := Finset (Fin (n + 1)))
    (Finset.image (α := Fin (d + 1))
      (⇑(Hom.toOrderHom
            (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑f : Δ[n] _⦋d⦌))) :
        (a : Fin (d + 1)) → Fin (n + 1))
      univ)
    (((↑(((Equiv.ofBijective
                      (fun (x : { x : Δ[n] _⦋d⦌ // Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Δ[n].nonDegenerate d) x }) ↦
                        Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦ #x = d + 1)
                          (Finset.image (α := Fin (d + 1))
                            (⇑(Hom.toOrderHom
                                  (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌)
                                    (↑x : Δ[n] _⦋d⦌))) :
                              (a : Fin (d + 1)) → Fin (n + 1))
                            univ)
                          ⋯)
                      ⋯).symm :
                  (a : { x : Finset (Fin (n + 1)) // #x = d + 1 }) → (↑(Δ[n].nonDegenerate d) : Type u))
                (Subtype.mk (p := fun (x : Finset (Fin (n + 1))) ↦ #x = d + 1)
                  (Finset.image (α := Fin (d + 1))
                    (⇑(Hom.toOrderHom
                          (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌)
                            (↑f : Δ[n] _⦋d⦌))) :
                      (a : Fin (d + 1)) → Fin (n + 1))
                    univ)
                  ⋯)) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
have simp : ∃ (a : Fin (d + 1)),
  Eq (α := Fin (n + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋d⦌ ≃ (unop (op ⦋d⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋d⦌) → ⦋d⦌ ⟶ ⦋n⦌) (↑f : Δ[n] _⦋d⦌)) :
          (a : Fin (d + 1)) → Fin (n + 1))
        a :
      Fin (n + 1))
    (((↑f : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i : Fin (n + 1))
Tactic: simp only [Equiv.ofBijective_symm_apply_apply, Finset.mem_image, Finset.mem_univ, true_and]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
S : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)
A : Δ[n].Subcomplex
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            S) :
        Δ[n] _⦋d⦌) ↔
    face (↑S : Finset (Fin (n + 1))) ≤ A
have obtain : ∀ (x : (↑(Δ[n].nonDegenerate d) : Type u)),
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            (((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x :
              (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
        Δ[n] _⦋d⦌) ↔
    face
        (↑(((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x) :
          Finset (Fin (n + 1))) ≤
      A
Tactic: obtain ⟨x, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
A : Δ[n].Subcomplex
x : (↑(Δ[n].nonDegenerate d) : Type u)
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            (((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x :
              (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
        Δ[n] _⦋d⦌) ↔
    face
        (↑(((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x) :
          Finset (Fin (n + 1))) ≤
      A
have rw : Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
    (↑((Equiv.symm nonDegenerateEquiv' :
            (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
          (((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x :
            (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
      Δ[n] _⦋d⦌) ↔
  Subcomplex.ofSimplex (↑x : Δ[n] _⦋d⦌) ≤ A
Tactic: rw [face_nonDegenerateEquiv' x, Equiv.symm_apply_apply, Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
A : Δ[n].Subcomplex
x : (↑(Δ[n].nonDegenerate d) : Type u)
rw :
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            (((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x :
              (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
        Δ[n] _⦋d⦌) ↔
    Subcomplex.ofSimplex (↑x : Δ[n] _⦋d⦌) ≤ A
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            (((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x :
              (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
        Δ[n] _⦋d⦌) ↔
    face
        (↑(((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x) :
          Finset (Fin (n + 1))) ≤
      A
have rw₁ : Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n] _⦋d⦌) ↔ Subcomplex.ofSimplex (↑x : Δ[n] _⦋d⦌) ≤ A
Tactic: rw [face_nonDegenerateEquiv' x, Equiv.symm_apply_apply, Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
A : Δ[n].Subcomplex
x : (↑(Δ[n].nonDegenerate d) : Type u)
rw :
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            (((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x :
              (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
        Δ[n] _⦋d⦌) ↔
    Subcomplex.ofSimplex (↑x : Δ[n] _⦋d⦌) ≤ A
rw₁ :
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n] _⦋d⦌) ↔ Subcomplex.ofSimplex (↑x : Δ[n] _⦋d⦌) ≤ A
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            (((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x :
              (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
        Δ[n] _⦋d⦌) ↔
    face
        (↑(((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x) :
          Finset (Fin (n + 1))) ≤
      A
have rw₂ : Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n] _⦋d⦌) ↔
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n] _⦋d⦌)
Tactic: rw [face_nonDegenerateEquiv' x, Equiv.symm_apply_apply, Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : SimplexCategory
d : SimplexCategoryᵒᵖ
⊢ Finite.{u + 1} ((stdSimplex.obj n).obj d)
have rw : Finite (unop d ⟶ n)
Tactic: rw [objEquiv.finite_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : SimplexCategory
⊢ SSet.Finite.{u} (stdSimplex.obj n)
have mk : ∀ (n : ℕ), SSet.Finite.{u} Δ[n]
Tactic: induction n using SimplexCategory.rec with | _ n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ SSet.Finite.{u} (Subcomplex.ofSimplex x).toSSet
have obtain : ∀ (f : Δ[n] ⟶ X),
  SSet.Finite.{u}
    (Subcomplex.toSSet (X := X) (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ X) → X _⦋n⦌) f)))
Tactic: obtain ⟨f, rfl⟩ := yonedaEquiv.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
X : SSet
n : ℕ
f : Δ[n] ⟶ X
⊢ SSet.Finite.{u}
    (Subcomplex.toSSet (X := X) (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ X) → X _⦋n⦌) f)))
have rw : SSet.Finite.{u} (Subcomplex.range f).toSSet
Tactic: rw [← Subcomplex.range_eq_ofSimplex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
⊢ HasDimensionLT.{u} (face S).toSSet d
have generalize : ∀ (m : ℕ) (hm : #S = m), HasDimensionLT.{u} (face S).toSSet d
Tactic: generalize hm : S.card = m
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m
⊢ HasDimensionLT.{u} (face S).toSSet d
have zero : ∀ (hm : #S = 0), HasDimensionLT.{u} (face S).toSSet d
Tactic: obtain _ | m := m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m
zero : ∀ (hm : #S = 0), HasDimensionLT.{u} (face S).toSSet d
⊢ HasDimensionLT.{u} (face S).toSSet d
have succ : ∀ (m : ℕ) (hm : #S = m + 1), HasDimensionLT.{u} (face S).toSSet d
Tactic: obtain _ | m := m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
hm : #S = 0
⊢ HasDimensionLT.{u} (face S).toSSet d
have zero : ∀ (hd : card (α := Fin (n + 1)) ∅ ≤ d) (hm : card (α := Fin (n + 1)) ∅ = 0),
  HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) (face ∅)) d
Tactic: obtain rfl : S = ∅ := by rwa [← Finset.card_eq_zero]
Cleared hypotheses: S, hd, hm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n d : ℕ
hd : card (α := Fin (n + 1)) ∅ ≤ d
hm : card (α := Fin (n + 1)) ∅ = 0
⊢ HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) (face ∅)) d
have zero : HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) ⊥) d
Tactic: rw [face_empty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ HasDimensionLT.{u} (face S).toSSet d
have succ : HasDimensionLT.{u} Δ[m] d
Tactic: rw [← hasDimensionLT_iff_of_iso
      (isoOfRepresentableBy (faceRepresentableBy S m (monoEquivOfFin S (by simpa))))]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
x_1 : SimplexCategoryᵒᵖ
x : Δ[n].obj x_1
h : Membership.mem (γ := Set (Δ[n].obj x_1)) (Subfunctor.obj ⊤ x_1) x
⊢ Membership.mem (γ := Set (Δ[n].obj x_1))
    (Subfunctor.obj
      (Subcomplex.ofSimplex (n := n) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌))) x_1)
    x
have obtain : ∀ (f : unop x_1 ⟶ ⦋n⦌),
  Membership.mem.{u, u} (α := Δ[n].obj x_1) (γ := Set (Δ[n].obj x_1)) (Subfunctor.obj ⊤ x_1)
      ((Equiv.symm objEquiv : (a : unop x_1 ⟶ ⦋n⦌) → Δ[n].obj x_1) f : Δ[n].obj x_1) →
    Membership.mem.{u, u} (α := Δ[n].obj x_1) (γ := Set (Δ[n].obj x_1))
      (Subfunctor.obj
        (Subcomplex.ofSimplex (n := n) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌))) x_1)
      ((Equiv.symm objEquiv : (a : unop x_1 ⟶ ⦋n⦌) → Δ[n].obj x_1) f : Δ[n].obj x_1)
Tactic: obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x
Cleared hypotheses: x, h