awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
d : ℕ
s : X _⦋d⦌
h₁_1 : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s
h₂ :
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁_1)
h₁ : ∃ (i : ι), Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s
⊢ ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                ⋯ :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      N.mk
        (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
              Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁_1)
              h₂) :
          (⨆ (i : ι), A i).toSSet _⦋d⦌)
        ⋯
have obtain : ∀ (i : ι) (hi : Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s),
  ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE sorry).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                sorry :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      N.mk
        (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
              Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁_1)
              h₂) :
          (⨆ (i : ι), A i).toSSet _⦋d⦌)
        sorry
Tactic: obtain ⟨i, hi⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
d : ℕ
s : X _⦋d⦌
h₁ : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s
h₂_1 :
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
h₂ :
  (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦
          Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁) :
      X _⦋d⦌) ∈
    X.nonDegenerate d
i : ι
hi : Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s
⊢ Membership.mem (γ := Set ((A i).toSSet _⦋d⦌)) ((A i).toSSet.nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦ Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) x) s hi)
have rwa : (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦ Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) x) s hi) :
    X _⦋d⦌) ∈
  X.nonDegenerate d
Tactic: rwa [Subcomplex.mem_nonDegenerate_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ ((𝟙_ SSet) (𝒞 := Functor.category).map f ≫
      ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ') ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
            (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ'))))
          x) =
    (↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
            (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
          x) ≫
      K.map f
have h : TypeCat.Fun.toFun
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      ((𝟙_ SSet) (𝒞 := Functor.category).map f ≫
        ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ') ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
              (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ'))))
            x))
    PUnit.unit =
  TypeCat.Fun.toFun
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      ((↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
              (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
            x) ≫
        K.map f))
    PUnit.unit
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((𝟙_ SSet) (𝒞 := Functor.category).map f ≫
          ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ') ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ'))))
              x))
      PUnit.unit =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
              x) ≫
          K.map f))
      PUnit.unit
have h : Eq (α := K.obj Δ')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
        (a : K _⦋0⦌) → K.obj Δ')
      x :
    K.obj Δ')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map f) : (a : K.obj Δ) → K.obj Δ')
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
            (a : K _⦋0⦌) → K.obj Δ)
          x :
        K.obj Δ) :
    K.obj Δ')
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ Eq (α := K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
          (a : K _⦋0⦌) → K.obj Δ')
        x :
      K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map f) : (a : K.obj Δ) → K.obj Δ')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
              (a : K _⦋0⦌) → K.obj Δ)
            x :
          K.obj Δ) :
      K.obj Δ')
have h : Eq (α := K.obj Δ')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
        (a : K _⦋0⦌) → K.obj Δ')
      x :
    K.obj Δ')
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0) ≫ f)) :
        (a : K _⦋0⦌) → K.obj Δ')
      x :
    K.obj Δ')
Tactic: rw [← Functor.map_comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
K : SSet
φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K
⊢ (fun (x : K _⦋0⦌) ↦
        ({
            app := fun (Δ : SimplexCategoryᵒᵖ) ↦
              ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                    (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) →
                      (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
                  x,
            naturality := ⋯ } :
          NatTrans ((𝟙_ SSet) (𝒞 := Functor.category)) K))
      ((fun (φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) :
                (a : (fun (X : Type u) ↦ X) (𝟙_ SSet _⦋0⦌)) → (fun (X : Type u) ↦ X) (K _⦋0⦌))
              PUnit.unit :
            (fun (X : Type u) ↦ X) (K _⦋0⦌)))
        φ) =
    φ
have w : ∀ (Δ : SimplexCategoryᵒᵖ),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : K _⦋0⦌) ↦
              ({
                  app := fun (Δ : SimplexCategoryᵒᵖ) ↦
                    ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun)
                            (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                          (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) →
                            (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
                        x,
                  naturality := sorry } :
                NatTrans ((𝟙_ SSet) (𝒞 := Functor.category)) K))
            ((fun (φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) :
                      (a : (fun (X : Type u) ↦ X) (𝟙_ SSet _⦋0⦌)) → (fun (X : Type u) ↦ X) (K _⦋0⦌))
                    PUnit.unit :
                  (fun (X : Type u) ↦ X) (K _⦋0⦌)))
              φ))
          Δ))
      PUnit.unit =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ)).toFun PUnit.unit
Tactic: ext Δ ⟨⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
K : SSet
φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K
Δ : SimplexCategoryᵒᵖ
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : K _⦋0⦌) ↦
              ({
                  app := fun (Δ : SimplexCategoryᵒᵖ) ↦
                    ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun)
                            (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                          (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) →
                            (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
                        x,
                  naturality := ⋯ } :
                NatTrans ((𝟙_ SSet) (𝒞 := Functor.category)) K))
            ((fun (φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) :
                      (a : (fun (X : Type u) ↦ X) (𝟙_ SSet _⦋0⦌)) → (fun (X : Type u) ↦ X) (K _⦋0⦌))
                    PUnit.unit :
                  (fun (X : Type u) ↦ X) (K _⦋0⦌)))
              φ))
          Δ))
      PUnit.unit =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ)).toFun PUnit.unit
have w : Eq (α := K.obj Δ)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
        (a : K _⦋0⦌) → K.obj Δ)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) : (a : 𝟙_ SSet _⦋0⦌) → K _⦋0⦌) PUnit.unit :
        K _⦋0⦌) :
    K.obj Δ)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ) PUnit.unit : K.obj Δ)
Tactic: dsimp [-Monoidal.tensorUnit_obj]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
K : SSet
φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K
Δ : SimplexCategoryᵒᵖ
⊢ Eq (α := K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
          (a : K _⦋0⦌) → K.obj Δ)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) : (a : 𝟙_ SSet _⦋0⦌) → K _⦋0⦌) PUnit.unit :
          K _⦋0⦌) :
      K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ) PUnit.unit : K.obj Δ)
have w : Eq (α := K.obj Δ)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((𝟙_ SSet) (𝒞 := Functor.category).map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
            (a : 𝟙_ SSet _⦋0⦌) → (𝟙_ SSet).obj Δ)
          PUnit.unit :
        (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) :
    K.obj Δ)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ) PUnit.unit : K.obj Δ)
Tactic: rw [← NatTrans.naturality_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
x : SSet
x_1 : x ⟶ Δ[0]
⊢ x_1 = (fun (x : SSet.{u}) ↦ (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0])) x
have w : ∀ (n : SimplexCategory) (x_2 : x.obj (Opposite.op n)),
  TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app (Opposite.op n))) x_2 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : SSet.{u}) ↦ (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0])) x)
          (Opposite.op n)))
      x_2
Tactic: ext ⟨n⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
x : SSet
x_1 : x ⟶ Δ[0]
n : SimplexCategory
x_2 : x.obj (Opposite.op n)
⊢ Eq (α := Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
    (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
          (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
        (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app (Opposite.op n))) x_2) :
      Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
    (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
          (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((fun (x : SSet.{u}) ↦ (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0]))
                x)
              (Opposite.op n)))
          x_2) :
      Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
have a : ∀ (x_3 : Fin ((Opposite.unop (Opposite.op n)).len + 1)),
  (↑((SimplexCategory.Hom.toOrderHom
              (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
                  (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
                (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app (Opposite.op n))) x_2)) :
            (a : Fin ((Opposite.unop (Opposite.op n)).len + 1)) → Fin (⦋0⦌.len + 1))
          x_3) :
      ℕ) =
    (↑((SimplexCategory.Hom.toOrderHom
              (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
                  (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app
                      ((fun (x : SSet.{u}) ↦
                          (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0]))
                        x)
                      (Opposite.op n)))
                  x_2)) :
            (a : Fin ((Opposite.unop (Opposite.op n)).len + 1)) → Fin (⦋0⦌.len + 1))
          x_3) :
      ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ range (f₁ ⊗ₘ f₂) = (range f₁).prod (range f₂)
have obj : ∀ (m : SimplexCategoryᵒᵖ) (y₁ : Y₁.obj m) (y₂ : Y₂.obj m),
  Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
      (y₁, y₂) ↔
    (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m
Tactic: ext m ⟨y₁, y₂⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
      (y₁, y₂) ↔
    (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m
have obj : Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
    (y₁, y₂) →
  (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
obj :
  Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
      (y₁, y₂) →
    (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m
⊢ Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
      (y₁, y₂) ↔
    (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m
have obj₁ : (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m →
  Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
    (y₁, y₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (hypothesis)
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
x₁ : X₁.obj m
x₂ : X₂.obj m
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
        (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
      (x₁, x₂) =
    (y₁, y₂)
⊢ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m
have h₁ : ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
          (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
        (x₁, x₂)).1 =
    (y₁, y₂).1 ∧
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
          (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
        (x₁, x₂)).2 =
    (y₁, y₂).2
Tactic: rw [Prod.eq_iff_fst_eq_snd_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i : SimplexCategoryᵒᵖ
⊢ (range ((A.prod B).ι ≫ fst X Y)).obj i ≤ A.obj i
have _ : ∀ ⦃a : X.obj i⦄, a ∈ (range ((A.prod B).ι ≫ fst X Y)).obj i → a ∈ A.obj i
Tactic: _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i : SimplexCategoryᵒᵖ
a : X.obj i
⊢ a ∈ (range ((A.prod B).ι ≫ fst X Y)).obj i → a ∈ A.obj i
have this : ∀ (val : (tensorObj (𝒞 := Functor.category) X Y).obj i) (left : val.1 ∈ A.obj i) (right : val.2 ∈ B.obj i),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (((A.prod B).ι ≫ fst X Y).app i) :
          (a : (fun (X : Type u) ↦ X) ((A.prod B).toSSet.obj i)) → (fun (X : Type u) ↦ X) (X.obj i))
        (Subtype.mk (p := fun (x : (tensorObj (𝒞 := Functor.category) X Y).obj i) ↦ x ∈ (A.prod B).obj i) val sorry) =
      a →
    a ∈ A.obj i
Tactic: ⟨⟨_, ⟨_, _⟩⟩, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i : SimplexCategoryᵒᵖ
⊢ (range ((A.prod B).ι ≫ snd X Y)).obj i ≤ B.obj i
have _ : ∀ ⦃a : Y.obj i⦄, a ∈ (range ((A.prod B).ι ≫ snd X Y)).obj i → a ∈ B.obj i
Tactic: _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i : SimplexCategoryᵒᵖ
a : Y.obj i
⊢ a ∈ (range ((A.prod B).ι ≫ snd X Y)).obj i → a ∈ B.obj i
have this : ∀ (val : (tensorObj (𝒞 := Functor.category) X Y).obj i) (left : val.1 ∈ A.obj i) (right : val.2 ∈ B.obj i),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (((A.prod B).ι ≫ snd X Y).app i) :
          (a : (fun (X : Type u) ↦ X) ((A.prod B).toSSet.obj i)) → (fun (X : Type u) ↦ X) (Y.obj i))
        (Subtype.mk (p := fun (x : (tensorObj (𝒞 := Functor.category) X Y).obj i) ↦ x ∈ (A.prod B).obj i) val sorry) =
      a →
    a ∈ B.obj i
Tactic: ⟨⟨_, ⟨_, _⟩⟩, _⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ prod ⊤ T ⊓ S.prod ⊤ = S.prod T
have obj : ∀ (n : SimplexCategoryᵒᵖ) (x : X.obj n) (y : Y.obj n), (x, y) ∈ (prod ⊤ T ⊓ S.prod ⊤).obj n ↔ (x, y) ∈ (S.prod T).obj n
Tactic: ext n ⟨x, y⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
⊢ Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X Y).obj n)) (Subfunctor.obj (prod ⊤ T) n) (x, y) ∧
      Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X Y).obj n)) (Subfunctor.obj (S.prod ⊤) n) (x, y) ↔
    (x, y) ∈ (S.prod T).obj n
have obj : (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y ↔ S.obj n x ∧ T.obj n y
Tactic: simp [prod, Set.prod, Membership.mem, Set.Mem, setOf]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
⊢ (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y ↔ S.obj n x ∧ T.obj n y
have obj : (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y → S.obj n x ∧ T.obj n y
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
obj : (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y → S.obj n x ∧ T.obj n y
⊢ (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y ↔ S.obj n x ∧ T.obj n y
have obj₁ : S.obj n x ∧ T.obj n y → (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
obj : (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y → S.obj n x ∧ T.obj n y
obj₁ : S.obj n x ∧ T.obj n y → (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y
⊢ (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y ↔ S.obj n x ∧ T.obj n y
have obj₂ : Set.univ x → T.obj n y → S.obj n x → Set.univ y → S.obj n x ∧ T.obj n y
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
obj : (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y → S.obj n x ∧ T.obj n y
obj₁ : S.obj n x ∧ T.obj n y → (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y
obj₂ obj₃ : Set.univ x → T.obj n y → S.obj n x → Set.univ y → S.obj n x ∧ T.obj n y
⊢ (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y ↔ S.obj n x ∧ T.obj n y
have obj₄ : Set.univ x → T.obj n y → S.obj n x → Set.univ y → S.obj n x
Tactic: tauto