awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z ↔
    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))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
have rw : StrictMono.{0, u} (α := Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) (β := ULift.{u, 0} (Fin (p + 1) × Fin (q + 1)))
    (Functor.obj
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve p q).hom.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌)) →
            (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1))) _⦋n⦌))
        z)) ↔
  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))
            z :
          Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
      (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
Tactic: rw [← nonDegenerate_iff_of_mono (isoNerve p q).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_strictMono]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
⊢ (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i) : ℕ) ≤
    (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) j) : ℕ)
have this : LE.le (α := 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 :
    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))
      j :
    Fin (p + 1) × Fin (q + 1))
Tactic: have := (objEquiv x).monotone h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this :
  LE.le (α := 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 :
      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))
        j :
      Fin (p + 1) × Fin (q + 1))
⊢ (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i) : ℕ) ≤
    (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) j) : ℕ)
have h₁ : LE.le (α := Fin (p + 1)) ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i : Fin (p + 1))
  ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j : Fin (p + 1))
Tactic: have h₁ : x.1 i ≤ x.1 j := this.1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this :
  LE.le (α := 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 :
      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))
        j :
      Fin (p + 1) × Fin (q + 1))
h₁ :
  LE.le (α := Fin (p + 1)) ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i : Fin (p + 1))
    ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j : Fin (p + 1))
⊢ (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i) : ℕ) ≤
    (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) j) : ℕ)
have h₂ : LE.le (α := Fin (q + 1)) ((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i : Fin (q + 1))
  ((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) j : Fin (q + 1))
Tactic: have h₂ : x.2 i ≤ x.2 j := this.2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
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 : ℕ)
have h₁ : a.1 ≤ b.1
Tactic: obtain ⟨h₁, h₂⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
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
h₁ : a.1 ≤ b.1
⊢ a < b ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)
have h₂ : a.2 ≤ b.2
Tactic: obtain ⟨h₁, h₂⟩ := hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
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 < b ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)
have rw : 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: rw [Prod.lt_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
⊢ 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))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
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 : ℕ)
⊢ 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))
have 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))
Tactic: simp only [Fin.strictMono_iff_lt_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
⊢ Eq.{u + 1} (α := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n) ⊤
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
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
have h : Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
  ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n) x
Tactic: simp only [Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
hn : p + q + 1 ≤ n
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n) x
have h : ∀ (hx : x ∉ (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).degenerate n), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
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
⊢ False
have hx₁ : StrictMono (α := Fin (n + 1)) (β := Fin (p + q + 1)) (⇑(orderHomOfSimplex x sorry) : (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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
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))
⊢ False
have hx₁ : Fintype.card (Fin (n + 1)) ≤ Fintype.card (Fin (p + q + 1))
Tactic: replace hx := Fintype.card_le_of_injective _ hx.injective
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
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))
⊢ False
have hx₁ : n ≤ p + q
Tactic: simp only [Fintype.card_fin, add_le_add_iff_right] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) : Type u)
m : ℕ
hm : p + q = m
i : Fin (n + 1)
⊢ (↑i : ℕ) ≤ (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) i) : ℕ)
have zero : (↑0 : ℕ) ≤ (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) 0) : ℕ)
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)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
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) : ℕ)
⊢ (↑i : ℕ) ≤ (↑((orderHomOfSimplex (↑x : (Δ[p] ⊗ Δ[q]) _⦋n⦌) hm : (a : Fin (n + 1)) → Fin (m + 1)) i) : ℕ)
have 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) : ℕ)
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)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
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
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z ↔
    orderHomOfSimplex z hn = OrderHom.id
have refine_2 : orderHomOfSimplex z hn = OrderHom.id →
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id →
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z
have 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))
Tactic: rw [nonDegenerate_iff_injective_objEquiv]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (hypothesis)
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))
⊢ a = b
have 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) : ℕ), sorry⟩ :
      Fin (n + 1)) =
    x
Tactic: simp only [DFunLike.ext_iff, orderHomOfSimplex_coe, OrderHom.id_coe, id_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
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
⊢ a = b
have refine_2 : (↑(⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) a) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) a) : ℕ), sorry⟩ :
        Fin (n + 1)) :
    ℕ) =
  (↑(⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) b) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) b) : ℕ), sorry⟩ :
        Fin (n + 1)) :
    ℕ)
Tactic: rw [← h a, ← h b, Fin.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex (goal)
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
⊢ (↑(⟨(↑((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)) :
      ℕ)
have refine_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))
            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: change ((objEquiv z a).1 : ℕ) + (objEquiv z a).2 = (objEquiv z b).1 + (objEquiv z b).2
-- 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
⊢ z₁ = z₂
have a : (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
Tactic: ext
-- 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
⊢ (↑z₁ : (Δ[p] ⊗ Δ[q]) _⦋n⦌) = (↑z₂ : (Δ[p] ⊗ Δ[q]) _⦋n⦌)
have 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))
Tactic: apply objEquiv.injective