awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
⊢ a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
⊢ ∀ (a b : Fin (p + 1) × Fin (q + 1)) (hab : a ≤ b), a < b ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)

Tactic:
have (a b : Fin (p + 1) × Fin (q + 1)) (hab : a ≤ b) :
      a < b ↔ ((a.1 : ℕ) + a.2 < (b.1 : ℕ) + b.2) := by
    obtain ⟨h₁, h₂⟩ := hab
    rw [Prod.lt_iff]
    lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
this : ∀ (a b : Fin (p + 1) × Fin (q + 1)) (hab : a ≤ b), a < b ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)
simp :
  (∀ (i : Fin n),
      LT.lt (α := Fin (m + 1)) ((orderHomOfSimplex x hm : (a : Fin (n + 1)) → Fin (m + 1)) i.castSucc : Fin (m + 1))
        ((orderHomOfSimplex x hm : (a : Fin (n + 1)) → Fin (m + 1)) i.succ : Fin (m + 1))) ↔
    ∀ (i : Fin n),
      LT.lt (α := 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))
                  x :
                Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
              (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
            i.castSucc :
          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))
                  x :
                Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
              (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
            i.succ :
          Fin (p + 1) × Fin (q + 1))
⊢ StrictMono (α := Fin (n + 1)) (β := Fin (m + 1)) (⇑(orderHomOfSimplex x hm) : (a : Fin (n + 1)) → Fin (m + 1)) ↔
    StrictMono (α := Fin (n + 1)) (β := 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))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))

Tactic:
simp only [Fin.strictMono_iff_lt_succ]

Premises used: Fin.strictMono_iff_lt_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
this : ∀ (a b : Fin (p + 1) × Fin (q + 1)) (hab : a ≤ b), a < b ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)
⊢ (∀ (i : Fin n),
      LT.lt (α := Fin (m + 1)) ((orderHomOfSimplex x hm : (a : Fin (n + 1)) → Fin (m + 1)) i.castSucc : Fin (m + 1))
        ((orderHomOfSimplex x hm : (a : Fin (n + 1)) → Fin (m + 1)) i.succ : Fin (m + 1))) ↔
    ∀ (i : Fin n),
      LT.lt (α := 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))
                  x :
                Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
              (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
            i.castSucc :
          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))
                  x :
                Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
              (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
            i.succ :
          Fin (p + 1) × Fin (q + 1))

Tactic:
forall_congr' (fun i ↦ (this _ _ ((objEquiv x).monotone i.castSucc_le_succ)).symm)

Premises used: Fin.castSucc_le_succ, OrderHom.monotone, Fin.succ, SSet.prodStdSimplex.objEquiv, forall_congr', Fin.castSucc, DFunLike.coe, Iff.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
this : ∀ (a b : Fin (p + 1) × Fin (q + 1)) (hab : a ≤ b), a < b ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)
⊢ (∀ (i : Fin n),
      LT.lt (α := Fin (m + 1)) ((orderHomOfSimplex x hm : (a : Fin (n + 1)) → Fin (m + 1)) i.castSucc : Fin (m + 1))
        ((orderHomOfSimplex x hm : (a : Fin (n + 1)) → Fin (m + 1)) i.succ : Fin (m + 1))) ↔
    ∀ (i : Fin n),
      LT.lt (α := 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))
                  x :
                Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
              (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
            i.castSucc :
          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))
                  x :
                Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
              (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
            i.succ :
          Fin (p + 1) × Fin (q + 1))

Tactic:
exact forall_congr' (fun i ↦ (this _ _ ((objEquiv x).monotone i.castSucc_le_succ)).symm)

Premises used: OrderHom.monotone, SSet.prodStdSimplex.objEquiv, forall_congr', DFunLike.coe, Iff.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
m : ℕ
hm : p + q = m
⊢ StrictMono (α := Fin (n + 1)) (β := Fin (m + 1))
    (⇑(orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm) : (a : Fin (n + 1)) → Fin (m + 1))

Tactic:
simpa only [strictMono_orderHomOfSimplex_iff, ← nonDegenerate_iff_strictMono_objEquiv] using x.2

Premises used: SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
h :
  ∀ (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌),
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
        ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n) x ↔
      Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌)) ⊤ x
⊢ Eq.{u + 1} (α := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n) ⊤

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
h :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n) x
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n) x ↔
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌)) ⊤ x

Tactic:
simp only [Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: iff_true, Set.top_eq_univ, Set.mem_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
h : ∀ (hx : x ∉ (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n), False
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n) x

Tactic:
by_contra hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hx : x ∉ (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n
⊢ StrictMono (α := Fin (n + 1)) (β := Fin (p + q + 1)) (⇑(orderHomOfSimplex x ⋯) : (a : Fin (n + 1)) → Fin (p + q + 1))

Tactic:
rw [← mem_nonDegenerate_iff_notMem_degenerate,
      nonDegenerate_iff_strictMono_objEquiv,
      ← strictMono_orderHomOfSimplex_iff _ rfl] at hx

Premises used: SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, SSet.mem_nonDegenerate_iff_notMem_degenerate, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hx :
  StrictMono (α := Fin (n + 1)) (β := Fin (p + q + 1)) (⇑(orderHomOfSimplex x ⋯) : (a : Fin (n + 1)) → Fin (p + q + 1))
⊢ Fintype.card (Fin (n + 1)) ≤ Fintype.card (Fin (p + q + 1))

Tactic:
replace hx := Fintype.card_le_of_injective _ hx.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hx : Fintype.card (Fin (n + 1)) ≤ Fintype.card (Fin (p + q + 1))
⊢ n ≤ p + q

Tactic:
simp only [Fintype.card_fin, add_le_add_iff_right] at hx

Premises used: Fintype.card_fin, add_le_add_iff_right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hx : n ≤ p + q
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q : ℕ
⊢ SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q])

Tactic:
finite_of_hasDimensionLT _ (p + q + 1) inferInstance

Premises used: SSet.finite_of_hasDimensionLT, inferInstance, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
m : ℕ
hm : p + q = m
⊢ (↑0 : ℕ) ≤ (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) 0) : ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
m : ℕ
hm : p + q = m
i : Fin n
hi :
  (↑i.castSucc : ℕ) ≤
    (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) i.castSucc) : ℕ)
⊢ (↑i.succ : ℕ) ≤ (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) i.succ) : ℕ)

Tactic:
simpa using lt_of_le_of_lt hi (strictMono_orderHomOfSimplex x hm Fin.castSucc_lt_succ)

Premises used: lt_of_le_of_lt, Fin.castSucc_lt_succ, SSet.prodStdSimplex.strictMono_orderHomOfSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
m : ℕ
hm : p + q = m
i : Fin (n + 1)
zero : (↑0 : ℕ) ≤ (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) 0) : ℕ)
succ :
  ∀ (i : Fin n)
    (hi :
      (↑i.castSucc : ℕ) ≤
        (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) i.castSucc) : ℕ)),
    (↑i.succ : ℕ) ≤ (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) i.succ) : ℕ)
⊢ (↑i : ℕ) ≤ (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) i) : ℕ)

Tactic:
induction i using Fin.induction with
  | zero => simp
  | succ i hi =>
    simpa using lt_of_le_of_lt hi (strictMono_orderHomOfSimplex x hm Fin.castSucc_lt_succ)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z ↔
    orderHomOfSimplex z hn = OrderHom.id

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
refine_1 :
  ∀
    (h :
      Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
        ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z),
    orderHomOfSimplex z hn = OrderHom.id
refine_2 :
  orderHomOfSimplex z hn = OrderHom.id →
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z ↔
    orderHomOfSimplex z hn = OrderHom.id

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
h :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z
⊢ orderHomOfSimplex z hn = OrderHom.id

Tactic:
OrderHom.eq_id_of_injective _ (strictMono_orderHomOfSimplex ⟨z, h⟩ hn).injective

Premises used: Subtype.mk, StrictMono.injective, OrderHom.eq_id_of_injective, SSet.prodStdSimplex.strictMono_orderHomOfSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
h :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z
⊢ orderHomOfSimplex z hn = OrderHom.id

Tactic:
exact OrderHom.eq_id_of_injective _ (strictMono_orderHomOfSimplex ⟨z, h⟩ hn).injective

Premises used: Subtype.mk, StrictMono.injective, OrderHom.eq_id_of_injective, SSet.prodStdSimplex.strictMono_orderHomOfSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
refine_2 :
  orderHomOfSimplex z hn = OrderHom.id →
    Function.Injective (α := Fin (n + 1)) (β := 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 :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
⊢ orderHomOfSimplex z hn = OrderHom.id →
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z

Tactic:
rw [nonDegenerate_iff_injective_objEquiv]

Premises used: SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
h : orderHomOfSimplex z hn = OrderHom.id
a b : Fin (n + 1)
hab :
  Eq (α := 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 :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        a :
      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 :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        b :
      Fin (p + 1) × Fin (q + 1))
⊢ ∀ (x : Fin (n + 1)),
    (⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) x) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) x) : ℕ), ⋯⟩ :
        Fin (n + 1)) =
      x

Tactic:
simp only [DFunLike.ext_iff, orderHomOfSimplex_coe, OrderHom.id_coe, id_eq] at h

Premises used: OrderHom.id_coe, SSet.prodStdSimplex.orderHomOfSimplex_coe, DFunLike.ext_iff, id_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab :
  Eq (α := 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 :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        a :
      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 :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        b :
      Fin (p + 1) × Fin (q + 1))
h :
  ∀ (x : Fin (n + 1)),
    (⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) x) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) x) : ℕ), ⋯⟩ :
        Fin (n + 1)) =
      x
refine_2 :
  (↑(⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) a) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) a) : ℕ), ⋯⟩ :
          Fin (n + 1)) :
      ℕ) =
    (↑(⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) b) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) b) : ℕ), ⋯⟩ :
          Fin (n + 1)) :
      ℕ)
⊢ a = b

Tactic:
rw [← h a, ← h b, Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab :
  Eq (α := 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 :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        a :
      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 :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        b :
      Fin (p + 1) × Fin (q + 1))
h :
  ∀ (x : Fin (n + 1)),
    (⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) x) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) x) : ℕ), ⋯⟩ :
        Fin (n + 1)) =
      x
⊢ (↑(((((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 :
                  Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
                (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
              a).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 :
                  Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
                (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
              a).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 :
                  Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
                (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
              b).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 :
                  Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
                (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
              b).2 :
        ℕ)

Tactic:
simp only [hab]
-- 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 : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
⊢ z₁ = z₂

Tactic:
ext
-- 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 :
  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))
⊢ (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)

Tactic:
apply objEquiv.injective

Premises used: SSet.prodStdSimplex.objEquiv, Equiv.injective