awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
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
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
⊢ 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))

Tactic:
ext i : 3
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
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 (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:
DFunLike.congr_fun h i

Premises used: DFunLike.congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
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 (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:
exact DFunLike.congr_fun h i

Premises used: DFunLike.congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
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)
⊢ 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
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
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⦌)
⊢ 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
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
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⦌)
⊢ orderHomOfSimplex (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) ⋯ = OrderHom.id

Tactic:
rw [nonDegenerate_max_dim_iff] at h₁ h₂

Premises used: SSet.prodStdSimplex.nonDegenerate_max_dim_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
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
⊢ orderHomOfSimplex (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) ⋯ = OrderHom.id

Tactic:
rw [nonDegenerate_max_dim_iff] at h₁ h₂

Premises used: SSet.prodStdSimplex.nonDegenerate_max_dim_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
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₁ : orderHomOfSimplex (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) ⋯ = OrderHom.id
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

Tactic:
simpa only [orderHomOfSimplex_coe, h, Fin.ext_iff, add_right_inj]
      using DFunLike.congr_fun (h₁.trans h₂.symm) i

Premises used: Fin.ext_iff, DFunLike.congr_fun, SSet.prodStdSimplex.orderHomOfSimplex_coe, Eq.symm, add_right_inj, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z₁ z₂ : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
h : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).2 = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌).2
hn : p + q = n
⊢ z₁ = z₂

Tactic:
(nonDegenerateEquivOfIso (β_ _ _)).injective (nonDegenerate_ext₁ h)

Premises used: SSet.prodStdSimplex.nonDegenerate_ext₁, SSet.nonDegenerateEquivOfIso, CategoryTheory.BraidedCategory.braiding, Equiv.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
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)
      ⋯)
    OrderHom.id
⊢ 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⦌)

Tactic:
rw [nonDegenerate_max_dim_iff _ rfl]

Premises used: SSet.prodStdSimplex.nonDegenerate_max_dim_iff, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
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)
                ⋯ :
              (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1))
            j) :
        ℕ) =
      (↑((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) j) : ℕ)
⊢ 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

Tactic:
ext j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
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 : ℕ)
⊢ (↑((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) : ℕ)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
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 : ℕ)
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 : ℕ)
⊢ (↑((((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

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ j.castSucc < i.castSucc.succ

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
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 : ℕ)
⊢ (↑((((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:
rw [objMk₁_of_castSucc_lt _ _ (by simpa),
          Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero]

Premises used: SSet.stdSimplex.objMk₁_of_castSucc_lt, Fin.coe_ofNat_eq_mod, Nat.zero_mod, add_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ (↑(i.predAbove j) : ℕ) = (↑j : ℕ)

Tactic:
simp [Fin.predAbove_of_le_castSucc _ _ hj]

Premises used: Fin.predAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : ¬j ≤ i.castSucc
⊢ i.castSucc < j

Tactic:
simp only [not_le] at hj

Premises used: not_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ ≤ j.castSucc

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
neg :
  (↑((SimplexCategory.Hom.toOrderHom (SimplexCategory.σ i) : (a : Fin (⦋p + 1⦌.len + 1)) → Fin (⦋p⦌.len + 1)) j) : ℕ) +
      (↑1 : ℕ) =
    (↑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 : ℕ)

Tactic:
rw [objMk₁_of_le_castSucc _ _ (by simpa), objEquiv_symm_apply]

Premises used: SSet.stdSimplex.objMk₁_of_le_castSucc, SSet.stdSimplex.objEquiv_symm_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
neg : (↑j : ℕ) - 1 + 1 = (↑j : ℕ)
⊢ (↑(i.predAbove j) : ℕ) + 1 = (↑j : ℕ)

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ hj, Fin.val_pred]

Premises used: Fin.val_pred, Fin.predAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : i.castSucc < j
⊢ (↑j : ℕ) - 1 + 1 = (↑j : ℕ)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
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)
      ⋯

Tactic:
⟨fun _ _ h ↦ ?_, fun ⟨⟨s₁, s₂⟩, hs⟩ ↦ ?_⟩

Premises used: Fin.succ, Exists, SimplexCategory.σ, SSet.stdSimplex.objMk₁, Prod.mk, Subtype.mk, SSet.prodStdSimplex.nonDegenerateEquiv₁._proof_2, And.intro, Function.Bijective, Equiv.symm, Fin.castSucc, Eq, DFunLike.coe, SSet.stdSimplex.objEquiv, _private.0.SSet.prodStdSimplex.nonDegenerateEquiv₁.match_2
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
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)
            ⋯ :
          { 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)
            ⋯ :
          { 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:
simpa using stdSimplex.objMk₁_injective (congr_arg (Prod.snd ∘ Subtype.val) h)

Premises used: Function.comp, SSet.stdSimplex.objMk₁_injective, congr_arg, Subtype.val, Prod.snd
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
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₂)
⊢ orderHomOfSimplex (s₁, s₂) ⋯ = OrderHom.id

Tactic:
rw [nonDegenerate_max_dim_iff _ rfl] at hs

Premises used: SSet.prodStdSimplex.nonDegenerate_max_dim_iff, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
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
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) ⋯ = 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₁, objMk₁ i) hs
⊢ ∃ (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

Tactic:
obtain ⟨i, rfl⟩ := stdSimplex.objMk₁_surjective s₂

Premises used: SSet.stdSimplex.objMk₁_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
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
⊢ Eq (α := Fin (p + 1 + 1)) ((orderHomOfSimplex (s₁, objMk₁ 0) ⋯ : (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
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
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
this :
  Eq (α := Fin (p + 1 + 1)) ((orderHomOfSimplex (s₁, objMk₁ 0) ⋯ : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) 0)
    ((OrderHom.id : (a : Fin (p + 1 + 1)) → Fin (p + 1 + 1)) 0)
⊢ LE.le (α := Fin (p + 1 + 2)) 0 (Fin.castSucc 0)

Tactic:
simp