awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), HasDimensionLT.{u} (F.obj j) n
⊢ HasDimensionLT.{u} c.pt n
have rw : ∀ (i : J), HasDimensionLT.{u} (Subcomplex.range (c.ι.app i)).toSSet n
Tactic: rw [← hasDimensionLT_subcomplex_top_iff, ← iSup_range_eq_top_of_isColimit hc,
    hasDimensionLT_iSup_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
inst_1 : HasColimitsOfShape.{u_2, u_1, u, u + 1} J (Type u)
F : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J SSet
c : Cocone F
hc : IsColimit c
inst_2 : Finite J
h : ∀ (j : J), SSet.Finite.{u} (F.obj j)
⊢ SSet.Finite.{u} c.pt
have rw : ∀ (i : J), SSet.Finite.{u} (Subcomplex.range (c.ι.app i)).toSSet
Tactic: rw [← finite_subcomplex_top_iff, ← iSup_range_eq_top_of_isColimit hc, finite_iSup_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{?u.10772, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
⊢ SSet.Finite.{u} (⊥_ SSet)
have apply : ∀ (j : Discrete PEmpty.{1}), SSet.Finite.{u} (Functor.obj (Functor.empty SSet) j)
Tactic: apply finite_of_isColimit (initialIsInitial (C := SSet.{u}))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{?u.11777, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst_2 : X.Finite
inst_3 : Y.Finite
⊢ SSet.Finite.{u} (X ⨿ Y)
have apply : ∀ (j : Discrete WalkingPair), SSet.Finite.{u} (Functor.obj (pair X Y) j)
Tactic: apply finite_of_isColimit (coprodIsCoprod X Y)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
⊢ HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
have obtain : ∀ (n : ℕ) (e : ι ≃ Fin n), HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
Tactic: obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (hypothesis)
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
⊢ SSet.Finite.{u} (∐ X)
have this : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
Tactic: have : HasColimitsOfShape (Discrete ι) (Type u) := by
    obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
    exact hasColimitsOfShape_of_equivalence (Discrete.equivalence e.symm)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
J : Type u_1
inst : Category.{?u.13010, u_1} J
inst_1 : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
ι : Type v
inst_2 : Finite ι
X : ι → SSet
inst_3 : HasCoproduct X
inst_4 : ∀ (j : ι), SSet.Finite.{u} (X j)
this : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
x : Discrete ι
j : ι
⊢ SSet.Finite.{u} (Functor.obj (Discrete.functor X) { as := j : Discrete ι })
have dsimp : SSet.Finite.{u} (X j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
⊢ Subcomplex.range f = ⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f)
have rw : Eq.{u + 1} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
  (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
Tactic: rw [range_eq_iSup_of_isColimit (coproductIsCoproduct X) f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
⊢ Eq.{u + 1} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
have refine_1 : LE.le.{u} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
  (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
refine_1 :
  LE.le.{u} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
⊢ Eq.{u + 1} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
have refine_2 : LE.le.{u} (α := Y.Subcomplex) (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
  (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
⊢ LE.le.{u} (α := Y.Subcomplex) (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
    (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
have refine_1 : ∀ (a' : ι),
  Subcomplex.range (X := Functor.obj (Discrete.functor X) { as := a' : Discrete ι })
      ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app { as := a' : Discrete ι } ≫ f) ≤
    ⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f)
Tactic: simp only [iSup_le_iff, Discrete.forall]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits (goal)
Goal:
ι : Type v
inst : HasColimitsOfShape.{v, v, u, u + 1} (Discrete ι) (Type u)
X : ι → SSet
Y : SSet
inst_1 : HasCoproduct X
f : ∐ X ⟶ Y
⊢ LE.le.{u} (α := Y.Subcomplex) (⨆ (i : ι), Subcomplex.range (Sigma.ι X i ≫ f))
    (⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f))
have refine_2 : ∀ (i : ι),
  Subcomplex.range (Sigma.ι X i ≫ f) ≤ ⨆ (j : Discrete ι), Subcomplex.range ((Cofan.mk (∐ X) (Sigma.ι X)).ι.app j ≫ f)
Tactic: simp only [iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (goal)
Goal:
X₁ X₂ : SSet
⊢ Eq.{u + 1} (α := (tensorObj (𝒞 := Functor.category) X₁ X₂).Subcomplex)
    (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)) ⊤
have obj : ∀ (m : SimplexCategoryᵒᵖ) (x₁ : X₁.obj m) (x₂ : X₂.obj m),
  Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X₁ X₂).obj m))
      (Subfunctor.obj
        (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)) m)
      (x₁, x₂) ↔
    Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X₁ X₂).obj m)) (Subfunctor.obj ⊤ m) (x₁, x₂)
Tactic: ext m ⟨x₁, x₂⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (goal)
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X₁ X₂).obj m))
      (Subfunctor.obj
        (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)) m)
      (x₁, x₂) ↔
    Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X₁ X₂).obj m)) (Subfunctor.obj ⊤ m) (x₁, x₂)
have obj : ∃ (i : X₁.N) (i_1 : X₂.N),
  (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
Tactic: simp only [Subfunctor.iSup_obj, Subcomplex.prod_obj, Set.mem_iUnion, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (hypothesis)
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
have hx₁ : Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁
Tactic: have hx₁ : x₁ ∈ (⊤ : X₁.Subcomplex).obj _ := by simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (hypothesis)
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
have hx₂ : Membership.mem (γ := Set (X₂.obj m)) (Subfunctor.obj ⊤ m) x₂
Tactic: have hx₂ : x₂ ∈ (⊤ : X₂.Subcomplex).obj _ := by simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (hypothesis)
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁
hx₂ : Membership.mem (γ := Set (X₂.obj m)) (Subfunctor.obj ⊤ m) x₂
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
have hx₃ : ∃ (i : X₁.N), x₁ ∈ i.subcomplex.obj m
Tactic: simp only [← N.iSup_subcomplex_eq_top, Subfunctor.iSup_obj, Set.mem_iUnion] at hx₁ hx₂
Cleared hypotheses: hx₁, hx₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (hypothesis)
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁
hx₂ : Membership.mem (γ := Set (X₂.obj m)) (Subfunctor.obj ⊤ m) x₂
hx₃ : ∃ (i : X₁.N), x₁ ∈ i.subcomplex.obj m
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
have hx₄ : ∃ (i : X₂.N), x₂ ∈ i.subcomplex.obj m
Tactic: simp only [← N.iSup_subcomplex_eq_top, Subfunctor.iSup_obj, Set.mem_iUnion] at hx₁ hx₂
Cleared hypotheses: hx₁, hx₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (goal)
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : ∃ (i : X₁.N), x₁ ∈ i.subcomplex.obj m
hx₂ : ∃ (i : X₂.N), x₂ ∈ i.subcomplex.obj m
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
have obj : ∀ (s₁ : X₁.N) (hs₁ : x₁ ∈ s₁.subcomplex.obj m),
  ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
Tactic: obtain ⟨s₁, hs₁⟩ := hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (goal)
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₂ : ∃ (i : X₂.N), x₂ ∈ i.subcomplex.obj m
s₁ : X₁.N
hs₁ : x₁ ∈ s₁.subcomplex.obj m
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
have obj : ∀ (s₂ : X₂.N) (hs₂ : x₂ ∈ s₂.subcomplex.obj m),
  ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
Tactic: obtain ⟨s₂, hs₂⟩ := hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (goal)
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
⊢ HasDimensionLT.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂) n
have rw : HasDimensionLT.{u}
  (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
    (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)))
  n
Tactic: rw [← hasDimensionLT_subcomplex_top_iff, ← iSup_subcomplexOfSimplex_prod_eq_top]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (goal)
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
⊢ HasDimensionLT.{u}
    (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
      (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)))
    n
have simp : ∀ (i : X₁.N) (i_1 : X₂.N),
  HasDimensionLT.{u}
    (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
      (Subcomplex.range (X := tensorObj (𝒞 := Functor.category) Δ[i.dim] Δ[i_1.dim])
        ((Equiv.symm yonedaEquiv : (a : X₁ _⦋i.dim⦌) → Δ[i.dim] ⟶ X₁) i.simplex ⊗ₘ
          (Equiv.symm yonedaEquiv : (a : X₂ _⦋i_1.dim⦌) → Δ[i_1.dim] ⟶ X₂) i_1.simplex)))
    n
Tactic: simp only [Subcomplex.ofSimplexProd_eq_range, hasDimensionLT_iSup_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (hypothesis)
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
⊢ HasDimensionLT.{u}
    (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
      (Subcomplex.range (X := tensorObj (𝒞 := Functor.category) Δ[x₁.dim] Δ[x₂.dim])
        ((Equiv.symm yonedaEquiv : (a : X₁ _⦋x₁.dim⦌) → Δ[x₁.dim] ⟶ X₁) x₁.simplex ⊗ₘ
          (Equiv.symm yonedaEquiv : (a : X₂ _⦋x₂.dim⦌) → Δ[x₂.dim] ⟶ X₂) x₂.simplex)))
    n
have this : x₁.dim < d₁
Tactic: have := X₁.dim_lt_of_nonDegenerate ⟨_, x₁.nonDegenerate⟩ d₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (hypothesis)
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this : x₁.dim < d₁
⊢ HasDimensionLT.{u}
    (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
      (Subcomplex.range (X := tensorObj (𝒞 := Functor.category) Δ[x₁.dim] Δ[x₂.dim])
        ((Equiv.symm yonedaEquiv : (a : X₁ _⦋x₁.dim⦌) → Δ[x₁.dim] ⟶ X₁) x₁.simplex ⊗ₘ
          (Equiv.symm yonedaEquiv : (a : X₂ _⦋x₂.dim⦌) → Δ[x₂.dim] ⟶ X₂) x₂.simplex)))
    n
have this₁ : x₂.dim < d₂
Tactic: have := X₂.dim_lt_of_nonDegenerate ⟨_, x₂.nonDegenerate⟩ d₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (hypothesis)
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this_1 : x₁.dim < d₁
this : x₂.dim < d₂
⊢ HasDimensionLT.{u}
    (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
      (Subcomplex.range (X := tensorObj (𝒞 := Functor.category) Δ[x₁.dim] Δ[x₂.dim])
        ((Equiv.symm yonedaEquiv : (a : X₁ _⦋x₁.dim⦌) → Δ[x₁.dim] ⟶ X₁) x₁.simplex ⊗ₘ
          (Equiv.symm yonedaEquiv : (a : X₂ _⦋x₂.dim⦌) → Δ[x₂.dim] ⟶ X₂) x₂.simplex)))
    n
have this₁ : HasDimensionLT.{u} (tensorObj (𝒞 := Functor.category) Δ[x₁.dim] Δ[x₂.dim]) n
Tactic: have := (Δ[x₁.dim] ⊗ Δ[x₂.dim]).hasDimensionLT_of_le (x₁.dim + x₂.dim + 1) n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (goal)
Goal:
X₁ X₂ X₃ X₄ : SSet
inst : X₁.Finite
inst_1 : X₂.Finite
⊢ SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)
have obtain : ∀ (d₁ : ℕ), X₁.HasDimensionLT d₁ → SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)
Tactic: obtain ⟨d₁, _⟩ := X₁.hasDimensionLT_of_finite
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd (goal)
Goal:
X₁ X₂ X₃ X₄ : SSet
inst : X₁.Finite
inst_1 : X₂.Finite
d₁ : ℕ
h : X₁.HasDimensionLT d₁
⊢ SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)
have obtain : ∀ (d₂ : ℕ), X₂.HasDimensionLT d₂ → SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)
Tactic: obtain ⟨d₂, _⟩ := X₂.hasDimensionLT_of_finite
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X Y : Truncated 2
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
ex : Edge x₀ x₁
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
ey : Edge y₀ y₁
⊢ homMk (ex.tensor (Edge.id y₀)) ≫ homMk ((Edge.id x₁).tensor ey) =
    homMk ((Edge.id x₀).tensor ey) ≫ homMk (ex.tensor (Edge.id y₁))
have rw : homMk (ex.tensor (Edge.id y₀)) ≫ homMk ((Edge.id x₁).tensor ey) = homMk (ex.tensor ey)
Tactic: rw [homMk_comp_homMk ((Edge.CompStruct.idComp ex).tensor (Edge.CompStruct.compId ey)),
    homMk_comp_homMk ((Edge.CompStruct.compId ex).tensor (Edge.CompStruct.idComp ey))]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X Y : Truncated 2
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
ex : Edge x₀ x₁
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
ey : Edge y₀ y₁
rw : homMk (ex.tensor (Edge.id y₀)) ≫ homMk ((Edge.id x₁).tensor ey) = homMk (ex.tensor ey)
⊢ homMk (ex.tensor (Edge.id y₀)) ≫ homMk ((Edge.id x₁).tensor ey) =
    homMk ((Edge.id x₀).tensor ey) ≫ homMk (ex.tensor (Edge.id y₁))
have rw₁ : homMk (ex.tensor ey) = homMk (ex.tensor ey)
Tactic: rw [homMk_comp_homMk ((Edge.CompStruct.idComp ex).tensor (Edge.CompStruct.compId ey)),
    homMk_comp_homMk ((Edge.CompStruct.compId ex).tensor (Edge.CompStruct.idComp ey))]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x₀ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
ex : Edge x₀ x₁
ey : Edge y₀ y₁
⊢ Eq (α :=
    (functor X Y ⋙ inverse X Y).obj (mk (x₀, y₀)) ⟶
      Functor.obj (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (mk (x₁, y₁)))
    ((functor X Y ⋙ inverse X Y).map (homMk (ex.tensor ey)) ≫
      Iso.hom
        ((fun
              (x :
                (tensorObj (𝒞 := Functor.category) X Y).obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x)) :
              (functor X Y ⋙ inverse X Y).obj (mk x) ≅ (functor X Y ⋙ inverse X Y).obj (mk x)))
          (x₁, y₁)))
    (Iso.hom
        ((fun
              (x :
                (tensorObj (𝒞 := Functor.category) X Y).obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x)) :
              (functor X Y ⋙ inverse X Y).obj (mk x) ≅ (functor X Y ⋙ inverse X Y).obj (mk x)))
          (x₀, y₀)) ≫
      CategoryTheory.Functor.map (𝟭 (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory) (homMk (ex.tensor ey)))
have dsimp : (inverse X Y).map (homMk ex, homMk ey) ≫ 𝟙 (mk (x₁, y₁)) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x₀ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
ex : Edge x₀ x₁
ey : Edge y₀ y₁
⊢ (inverse X Y).map (homMk ex, homMk ey) ≫ 𝟙 (mk (x₁, y₁)) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
have rw : (inverse X Y).map (homMk ex, homMk ey) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
Tactic: rw [Category.comp_id, Category.id_comp, inverse_map_mkHom_homMk_homMk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x₀ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
ex : Edge x₀ x₁
ey : Edge y₀ y₁
rw : (inverse X Y).map (homMk ex, homMk ey) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
⊢ (inverse X Y).map (homMk ex, homMk ey) ≫ 𝟙 (mk (x₁, y₁)) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
have rw₁ : (inverse X Y).map (homMk ex, homMk ey) = homMk (ex.tensor ey)
Tactic: rw [Category.comp_id, Category.id_comp, inverse_map_mkHom_homMk_homMk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
x₀ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₀ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
ex : Edge x₀ x₁
ey : Edge y₀ y₁
rw : (inverse X Y).map (homMk ex, homMk ey) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
rw₁ : (inverse X Y).map (homMk ex, homMk ey) = homMk (ex.tensor ey)
⊢ (inverse X Y).map (homMk ex, homMk ey) ≫ 𝟙 (mk (x₁, y₁)) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
have rw₂ : homMk (ex.tensor ey) = homMk (ex.tensor ey)
Tactic: rw [Category.comp_id, Category.id_comp, inverse_map_mkHom_homMk_homMk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
⊢ CategoryStruct.comp (Y := Cat.of (X.HomotopyCategory × Y.HomotopyCategory)) { toFunctor := functor X Y }
      { toFunctor := inverse X Y } =
    𝟙 (Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
have h : Cat.Hom.toFunctor
    (CategoryStruct.comp (Y := Cat.of (X.HomotopyCategory × Y.HomotopyCategory)) { toFunctor := functor X Y }
      { toFunctor := inverse X Y }) =
  Cat.Hom.toFunctor (𝟙 (Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal (goal)
Goal:
X X' Y Y' Z : Truncated 2
⊢ CategoryStruct.comp (Y := Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
      { toFunctor := inverse X Y } { toFunctor := functor X Y } =
    𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory))
have h : Cat.Hom.toFunctor
    (CategoryStruct.comp (Y := Cat.of (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
      { toFunctor := inverse X Y } { toFunctor := functor X Y }) =
  Cat.Hom.toFunctor (𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory)))
Tactic: ext