awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
obj :
  (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) →
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
obj₁ :
  (∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i) →
    ∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2
⊢ (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) ↔
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
have obj₂ : ∀ (w : Fin (n + 1)),
  (∀ (x_2 : Fin ((unop x).len + 1)),
      ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_2 = w) →
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
obj :
  (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) →
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
obj₁ :
  (∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i) →
    ∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2
obj₂ obj₃ obj₄ :
  ∀ (w : Fin (n + 1)),
    (∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_2 = w) →
      ∃ (i : Fin (n + 1)),
        ∀ (x_2 : Fin ((unop x).len + 1)),
          ¬(SimplexCategory.Hom.toOrderHom
                    (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                  (a : Fin ((unop x).len + 1)) → Fin (n + 1))
                x_2 =
              i
⊢ (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) ↔
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
have obj₅ : ∀ (w : Fin (n + 1)),
  (∀ (x_2 : Fin ((unop x).len + 1)),
      ¬(SimplexCategory.Hom.toOrderHom
                (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
              (a : Fin ((unop x).len + 1)) → Fin (n + 1))
            x_2 =
          w) →
    ∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
⊢ HasDimensionLT.{u_1} ∂Δ[n].toSSet n
have rw : ∀ (i : Fin (n + 1)), HasDimensionLT.{u_1} (Subcomplex.toSSet (X := Δ[n]) (stdSimplex.face {i}ᶜ)) n
Tactic: rw [boundary_eq_iSup, hasDimensionLT_iSup_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (∂Δ[n].obj (op ⦋d⦌)) s ↔
    ∃ (j : Fin (n + 1)), j ∉ Set.range (ι := Fin (d + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
have rw : Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Subfunctor.obj (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ) (op ⦋d⦌)) s ↔
  ∃ (j : Fin (n + 1)), j ∉ Set.range (ι := Fin (d + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
Tactic: rw [boundary_eq_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ stdSimplex.face {i}ᶜ ≤ ∂Δ[n]
have rw : LE.le.{u} (α := Δ[n].Subcomplex) (stdSimplex.face {i}ᶜ) (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ)
Tactic: rw [boundary_eq_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
⊢ objMk OrderHom.id ∉ ∂Δ[n].obj (op ⦋n⦌)
have rw : ∀ (x : Fin (n + 1)), objMk OrderHom.id ∉ Subfunctor.obj (face {x}ᶜ) (op ⦋n⦌)
Tactic: rw [boundary_eq_iSup, Subfunctor.iSup_obj, Set.mem_iUnion, not_exists]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m n : ℕ
h : m < n
⊢ Eq (α := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) Set.univ
have h₁ : ∀ (x : Δ[n] _⦋m⦌),
  Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x ↔ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) Set.univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m n : ℕ
h : m < n
x : Δ[n] _⦋m⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x ↔ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) Set.univ x
have h₁ : ∀ (f : unop (op ⦋m⦌) ⟶ ⦋n⦌),
  Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) ↔
    Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) Set.univ
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
Tactic: obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m n : ℕ
h : m < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) ↔
    Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) Set.univ
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
have h₁ : Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
  ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
Tactic: simp only [Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m n : ℕ
h : m < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
have h₁ : ∀ (h : m < 0) (f : unop (op ⦋m⦌) ⟶ ⦋0⦌),
  Membership.mem.{u, u} (α := Δ[0] _⦋m⦌) (γ := Set (Δ[0] _⦋m⦌)) (Subfunctor.obj ∂Δ[0] (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋0⦌) → Δ[0] _⦋m⦌) f : Δ[0] _⦋m⦌)
Tactic: obtain _ | n := n
Cleared hypotheses: n, h, f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m n : ℕ
h : m < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ :
  ∀ (h : m < 0) (f : unop (op ⦋m⦌) ⟶ ⦋0⦌),
    Membership.mem.{u, u} (α := Δ[0] _⦋m⦌) (γ := Set (Δ[0] _⦋m⦌)) (Subfunctor.obj ∂Δ[0] (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋0⦌) → Δ[0] _⦋m⦌) f : Δ[0] _⦋m⦌)
⊢ Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
have h₂ : ∀ (n : ℕ) (h : m < n + 1) (f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌),
  Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj ∂Δ[n + 1] (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) f : Δ[n + 1] _⦋m⦌)
Tactic: obtain _ | n := n
Cleared hypotheses: n, h, f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (hypothesis)
Goal:
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf :
  Function.Surjective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n + 1⦌.len + 1))
⊢ False
have hf₁ : Epi f
Tactic: rw [← SimplexCategory.epi_iff_surjective] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (hypothesis)
Goal:
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : Epi f
⊢ False
have this : n + 1 ≤ m
Tactic: have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
⊢ Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj ∂Δ[n + 1] (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) f : Δ[n + 1] _⦋m⦌)
have h₁ : ∀ (i : Fin (n + 2)) (q : unop (op ⦋m⦌) ⟶ ⦋n⦌),
  Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj ∂Δ[n + 1] (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) (q ≫ SimplexCategory.δ i) : Δ[n + 1] _⦋m⦌)
Tactic: obtain ⟨i, q, rfl⟩ := SimplexCategory.eq_comp_δ_of_not_surjective f (fun hf ↦ by
      rw [← SimplexCategory.epi_iff_surjective] at hf
      have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f
      lia)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj ∂Δ[n + 1] (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) (q ≫ SimplexCategory.δ i) : Δ[n + 1] _⦋m⦌)
have h₁ : Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj (stdSimplex.face {i}ᶜ) (op ⦋m⦌))
  ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) (q ≫ SimplexCategory.δ i) : Δ[n + 1] _⦋m⦌)
Tactic: apply face_singleton_compl_le_boundary i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj (stdSimplex.face {i}ᶜ) (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) (q ≫ SimplexCategory.δ i) : Δ[n + 1] _⦋m⦌)
have h₁ : LE.le.{u} (α := Δ[n + 1].Subcomplex)
  (Subcomplex.ofSimplex (n := m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.map (SimplexCategory.δ i)).app (op ⦋m⦌)) :
        (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n + 1] _⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) q : Δ[n] _⦋m⦌)))
  (Subcomplex.ofSimplex (n := n)
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
Tactic: rw [stdSimplex.face_singleton_compl, stdSimplex.objEquiv_symm_comp,
      ← Subcomplex.ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
⊢ Eq.{u + 1} (α := Δ[0].Subcomplex) ∂Δ[0] ⊥
have obj : ∀ (m : SimplexCategoryᵒᵖ) (x : Δ[0].obj m),
  Membership.mem (γ := Set (Δ[0].obj m)) (Subfunctor.obj ∂Δ[0] m) x ↔
    Membership.mem (γ := Set (Δ[0].obj m)) (Subfunctor.obj ⊥ m) x
Tactic: ext m x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
m : SimplexCategoryᵒᵖ
x : Δ[0].obj m
⊢ Membership.mem (γ := Set (Δ[0].obj m)) (Subfunctor.obj ∂Δ[0] m) x ↔
    Membership.mem (γ := Set (Δ[0].obj m)) (Subfunctor.obj ⊥ m) x
have obj : Function.Surjective (α := Fin ((unop m).len + 1)) (β := Fin 1)
  (⇑(stdSimplex.asOrderHom x) : (a : Fin ((unop m).len + 1)) → Fin 1)
Tactic: simp only [boundary, Nat.reduceAdd, Set.mem_setOf_eq, Subfunctor.bot_obj, Set.bot_eq_empty,
    Set.mem_empty_iff_false, iff_false, Decidable.not_not]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
⊢ ∂Δ[n].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌)) = ∂Δ[n]
have obj : ∀ (d : ℕ) (j : Δ[n] _⦋d⦌),
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) ((∂Δ[n].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌))).obj (op ⦋d⦌)) j ↔
    Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (∂Δ[n].obj (op ⦋d⦌)) j
Tactic: ext ⟨⟨d⟩⟩ j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) ((∂Δ[n].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌))).obj (op ⦋d⦌)) j ↔
    Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (∂Δ[n].obj (op ⦋d⦌)) j
have obj : (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) ↔
  ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
Tactic: simp only [Subcomplex.preimage_obj, Set.mem_preimage, stdSimplex.opIso_inv_app_hom_apply,
    Subcomplex.mem_op_obj_iff, mem_boundary_iff_notMem_range, Set.mem_range,
    stdSimplex.opObjEquiv_opObjEquiv_symm_apply, not_exists]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
⊢ (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) ↔
    ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
have obj : (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) →
  ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
obj :
  (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) →
    ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
⊢ (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) ↔
    ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
have obj₁ : (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1) →
  ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋i⦌)) (A.toSSet.degenerate i) ⊤
have h₁ : ∀ (a : Δ[n] _⦋i⦌) (ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a),
  Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.degenerate i)
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha) ↔
    Membership.mem (γ := Set (A.toSSet _⦋i⦌)) ⊤
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha)
Tactic: ext ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a
⊢ Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.degenerate i)
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha) ↔
    Membership.mem (γ := Set (A.toSSet _⦋i⦌)) ⊤
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha)
have h₁ : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i)
    (↑(Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha) :
      Δ[n] _⦋i⦌) ↔
  Membership.mem (γ := Set (A.toSSet _⦋i⦌)) ⊤
    (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha)
Tactic: rw [A.mem_degenerate_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i)
      (↑(Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha) :
        Δ[n] _⦋i⦌) ↔
    Membership.mem (γ := Set (A.toSSet _⦋i⦌)) ⊤
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha)
have h₁ : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a
Tactic: simp only [Subfunctor.toFunctor_obj, Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a
have h₁ : ∀ (hi : n < i), Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a
Tactic: obtain hi | rfl := hi.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a
h₁ : ∀ (hi : n < i), Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a
have h₂ : ∀ (hi : n ≤ n) (a : Δ[n] _⦋n⦌) (ha : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (A.obj (op ⦋n⦌)) a),
  Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].degenerate n) a
Tactic: obtain hi | rfl := hi.lt_or_eq
Cleared hypotheses: i, hi, a, ha
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (A.obj (op ⦋n⦌)) a
⊢ Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].degenerate n) a
have h₁ : a ∉
  singleton (α := stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
        (𝟙 (unop (op ⦋n⦌))) :
      stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
Tactic: rw [mem_degenerate_iff_notMem_nonDegenerate, nonDegenerate_top_dim]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
⊢ A ≤ ∂Δ[n] ↔ A ≠ ⊤
have refine_1 : ∀ (h : A ≤ ∂Δ[n]), A ≠ ⊤
Tactic: refine ⟨fun h ↦ ?_, fun hA ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
refine_1 : ∀ (h : A ≤ ∂Δ[n]), A ≠ ⊤
⊢ A ≤ ∂Δ[n] ↔ A ≠ ⊤
have refine_2 : ∀ (hA : A ≠ ⊤), A ≤ ∂Δ[n]
Tactic: refine ⟨fun h ↦ ?_, fun hA ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (hypothesis)
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
⊢ A ≤ ∂Δ[n]
have this : HasDimensionLT.{u} A.toSSet n
Tactic: have := subcomplex_hasDimensionLT_of_neq_top A hA
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
⊢ A ≤ ∂Δ[n]
have refine_2 : ∀ (n_1 : ℕ) (x : (↑(Δ[n].nonDegenerate n_1) : Type u)),
  Membership.mem (γ := Set (Δ[n] _⦋n_1⦌)) (A.obj (op ⦋n_1⦌)) (↑x : Δ[n] _⦋n_1⦌) →
    Membership.mem (γ := Set (Δ[n] _⦋n_1⦌)) (∂Δ[n].obj (op ⦋n_1⦌)) (↑x : Δ[n] _⦋n_1⦌)
Tactic: rw [Subcomplex.le_iff_contains_nonDegenerate]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
h₂ :
  Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (A.obj (op ⦋m⦌))
    (↑(Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x) x h₁) :
      Δ[n] _⦋m⦌)
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
    (↑(Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x) x h₁) :
      Δ[n] _⦋m⦌)
have refine_2 : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
Tactic: dsimp at h₂ ⊢
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
h₂ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (A.obj (op ⦋m⦌)) x
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
have pos : ∀ (h₃ : m < n), Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
Tactic: by_cases! h₃ : m < n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
h₂ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (A.obj (op ⦋m⦌)) x
pos : ∀ (h₃ : m < n), Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
have neg : ∀ (h₃ : n ≤ m), Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
Tactic: by_cases! h₃ : m < n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
⊢ A = ∂Δ[n] ↔ ∂Δ[n] ≤ A ∧ A ≠ ⊤
have mp : A = ∂Δ[n] → ∂Δ[n] ≤ A ∧ A ≠ ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
A : Δ[n].Subcomplex
mp : A = ∂Δ[n] → ∂Δ[n] ≤ A ∧ A ≠ ⊤
⊢ A = ∂Δ[n] ↔ ∂Δ[n] ≤ A ∧ A ≠ ⊤
have mpr : ∂Δ[n] ≤ A ∧ A ≠ ⊤ → A = ∂Δ[n]
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.range (stdSimplex.map (SimplexCategory.δ i)) ≤ ∂Δ[n + 1]
have simp : LE.le.{u} (α := Δ[n + 1].Subcomplex)
  (Subcomplex.ofSimplex (n := n)
    ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
  ∂Δ[n + 1]
Tactic: simp only [Subcomplex.range_eq_ofSimplex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    ∂Δ[n + 1]
have refine : LE.le.{u} (α := Δ[n + 1].Subcomplex)
  (Subcomplex.ofSimplex (n := n)
    ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
  (stdSimplex.face {i}ᶜ)
Tactic: refine le_trans ?_ (face_singleton_compl_le_boundary i)