awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
z₁ z₂ : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
h : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1 = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1
hn : p + q = n
⊢ Eq (α := Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
    (((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
          (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
        (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
      Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
    (((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
          (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
        (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
      Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
have a : ∀ (i : Fin (n + 1)),
  Eq (α := Fin (p + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).1
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).1
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
z₁ z₂ : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
h : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1 = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1
hn : p + q = n
a :
  ∀ (i : Fin (n + 1)),
    Eq (α := Fin (p + 1))
      (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                  (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
                (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
              Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
            (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
          i).1
      (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                  (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
                (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
              Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
            (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
          i).1
⊢ Eq (α := Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
    (((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
          (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
        (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
      Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
    (((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
          (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
        (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
      Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
have a₁ : ∀ (i : Fin (n + 1)),
  Eq (α := Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
Goal:
p q n : ℕ
z₁ z₂ : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
h : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1 = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1
hn : p + q = n
i : Fin (n + 1)
⊢ Eq (α := Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
have h₁ : Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
  ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
Tactic: have h₁ := z₁.2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
Goal:
p q n : ℕ
z₁ z₂ : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
h : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1 = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1
hn : p + q = n
i : Fin (n + 1)
h₁ :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
⊢ Eq (α := Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
have h₂ : Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
  ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
Tactic: have h₂ := z₂.2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
Goal:
p q n : ℕ
z₁ z₂ : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
h : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1 = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1
hn : p + q = n
i : Fin (n + 1)
h₁ :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
h₂ :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
⊢ Eq (α := Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
have h₃ : orderHomOfSimplex (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) sorry = OrderHom.id
Tactic: rw [nonDegenerate_max_dim_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
Goal:
p q n : ℕ
z₁ z₂ : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
h : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1 = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).1
hn : p + q = n
i : Fin (n + 1)
h₁ :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
h₂ :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
h₃ : orderHomOfSimplex (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) ⋯ = OrderHom.id
⊢ Eq (α := Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i).2
have h₄ : orderHomOfSimplex (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) sorry = OrderHom.id
Tactic: rw [nonDegenerate_max_dim_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
i : Fin (p + 1)
⊢ Membership.mem (α := tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) (γ :=
    Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1))
    (((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
        objMk₁ i.succ.castSucc) :
      Δ[p] _⦋p + 1⦌ × Δ[1] _⦋p + 1⦌)
have rw : Eq (α := Fin (p + 1 + 1) →o Fin (p + 1 + 1))
  (orderHomOfSimplex.{u}
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
      objMk₁ i.succ.castSucc)
    sorry)
  OrderHom.id
Tactic: rw [nonDegenerate_max_dim_iff _ rfl]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
i : Fin (p + 1)
⊢ Eq (α := Fin (p + 1 + 1) →o Fin (p + 1 + 1))
    (orderHomOfSimplex.{u}
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
        objMk₁ i.succ.castSucc)
      ⋯)
    OrderHom.id
have h : ∀ (j : Fin (p + 1 + 1)),
  (↑((orderHomOfSimplex.{u}
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              sorry :
            (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1))
          j) :
      ℕ) =
    (↑((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) j) : ℕ)
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
⊢ (↑((orderHomOfSimplex.{u}
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              ⋯ :
            (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1))
          j) :
      ℕ) =
    (↑((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) j) : ℕ)
have h : (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
            (a : Fin (p + 1 + 1)) → Fin (p + 1))
          j) :
      ℕ) +
    (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
  (↑j : ℕ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
⊢ (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
              (a : Fin (p + 1 + 1)) → Fin (p + 1))
            j) :
        ℕ) +
      (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
    (↑j : ℕ)
have pos : ∀ (hj : j ≤ i.castSucc),
  (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
              (a : Fin (p + 1 + 1)) → Fin (p + 1))
            j) :
        ℕ) +
      (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
    (↑j : ℕ)
Tactic: by_cases hj : j ≤ i.castSucc
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
pos :
  ∀ (hj : j ≤ i.castSucc),
    (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
                (a : Fin (p + 1 + 1)) → Fin (p + 1))
              j) :
          ℕ) +
        (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
      (↑j : ℕ)
⊢ (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
              (a : Fin (p + 1 + 1)) → Fin (p + 1))
            j) :
        ℕ) +
      (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
    (↑j : ℕ)
have neg : ∀ (hj : ¬j ≤ i.castSucc),
  (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
              (a : Fin (p + 1 + 1)) → Fin (p + 1))
            j) :
        ℕ) +
      (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
    (↑j : ℕ)
Tactic: by_cases hj : j ≤ i.castSucc
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
              (a : Fin (p + 1 + 1)) → Fin (p + 1))
            j) :
        ℕ) +
      (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
    (↑j : ℕ)
have pos : (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
          (a : Fin (p + 1 + 1)) → Fin (p + 1))
        j) :
    ℕ) =
  (↑j : ℕ)
Tactic: rw [objMk₁_of_castSucc_lt _ _ (by simpa),
          Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (hypothesis)
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : ¬j ≤ i.castSucc
⊢ (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
              (a : Fin (p + 1 + 1)) → Fin (p + 1))
            j) :
        ℕ) +
      (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
    (↑j : ℕ)
have hj₁ : i.castSucc < j
Tactic: simp only [not_le] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
⊢ (↑((((Equiv.symm stdSimplex.objEquiv : (a : ⦋p + 1⦌ ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i) : Δ[p] _⦋p + 1⦌) :
              (a : Fin (p + 1 + 1)) → Fin (p + 1))
            j) :
        ℕ) +
      (↑((objMk₁ i.castSucc.succ : (a : Fin (p + 1 + 1)) → Fin 2) j) : ℕ) =
    (↑j : ℕ)
have neg : (↑((SimplexCategory.Hom.toOrderHom (SimplexCategory.σ i) : (a : Fin (⦋p + 1⦌.len + 1)) → Fin (⦋p⦌.len + 1)) j) : ℕ) +
    (↑1 : ℕ) =
  (↑j : ℕ)
Tactic: rw [objMk₁_of_le_castSucc _ _ (by simpa), objEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
⊢ (↑(i.predAbove j) : ℕ) + 1 = (↑j : ℕ)
have neg : (↑j : ℕ) - 1 + 1 = (↑j : ℕ)
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ hj, Fin.val_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
⊢ Function.Bijective.{1, u + 1} (β := (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u))
    fun (i : Fin (p + 1)) ↦
    Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
      Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
        ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
        objMk₁ i.succ.castSucc)
      ⋯
have refine_1 : ∀ (x x_1 : Fin (p + 1))
  (h :
    Eq.{u + 1} (α := (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u))
      ((fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              sorry :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        x)
      ((fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              sorry :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        x_1)),
  x = x_1
Tactic: refine ⟨fun _ _ h ↦ ?_, fun ⟨⟨s₁, s₂⟩, hs⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (hypothesis)
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
s₂ : Δ[1] _⦋p + 1⦌
hs :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, s₂)
⊢ ∃ (a : Fin (p + 1)),
    (fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              ⋯ :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        a =
      Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
        Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
          ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
        (s₁, s₂) hs
have hs₁ : orderHomOfSimplex (s₁, s₂) sorry = OrderHom.id
Tactic: rw [nonDegenerate_max_dim_iff _ rfl] at hs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
s₂ : Δ[1] _⦋p + 1⦌
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, s₂)
hs : orderHomOfSimplex (s₁, s₂) ⋯ = OrderHom.id
⊢ ∃ (a : Fin (p + 1)),
    (fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              ⋯ :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        a =
      Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
        Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
          ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
        (s₁, s₂) hs_1
have refine_2 : ∀ (i : Fin (p + 1 + 2))
  (hs :
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i))
  (hs_2 : orderHomOfSimplex (s₁, objMk₁ i) sorry = OrderHom.id),
  ∃ (a : Fin (p + 1)),
    (fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              sorry :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        a =
      Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
        Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
          ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
        (s₁, objMk₁ i) hs
Tactic: obtain ⟨i, rfl⟩ := stdSimplex.objMk₁_surjective s₂
Cleared hypotheses: s₂, hs_1, hs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (hypothesis)
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ 0)
hs : orderHomOfSimplex (s₁, objMk₁ 0) ⋯ = OrderHom.id
⊢ False
have this : Eq (α := Fin (p + 1 + 1)) ((orderHomOfSimplex (s₁, objMk₁ 0) sorry : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) 0)
  ((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) 0)
Tactic: have := DFunLike.congr_fun hs 0