awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ Membership.mem (α := (tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m) (γ :=
    Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.app m) :
            (a : (fun (X : Type u) ↦ X) (X₁.obj m)) → (fun (X : Type u) ↦ X) (Y₁.obj m))
          x₁,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.app m) :
            (a : (fun (X : Type u) ↦ X) (X₂.obj m)) → (fun (X : Type u) ↦ X) (Y₂.obj m))
          x₂) :
      Y₁.obj m × Y₂.obj m)

Tactic:
exact ⟨⟨x₁, x₂⟩, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
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
⊢ (range ((A.prod B).ι ≫ fst X Y)).obj i ≤ A.obj i

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i : SimplexCategoryᵒᵖ
a : X.obj i
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 ⋯) =
        a →
      a ∈ A.obj i
⊢ a ∈ (range ((A.prod B).ι ≫ fst X Y)).obj i → a ∈ A.obj i

Tactic:
⟨⟨_, ⟨_, _⟩⟩, _⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
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
⊢ (range ((A.prod B).ι ≫ snd X Y)).obj i ≤ B.obj i

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
i : SimplexCategoryᵒᵖ
a : Y.obj i
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 ⋯) =
        a →
      a ∈ B.obj i
⊢ a ∈ (range ((A.prod B).ι ≫ snd X Y)).obj i → a ∈ B.obj i

Tactic:
⟨⟨_, ⟨_, _⟩⟩, _⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
m : SimplexCategoryᵒᵖ
y₁ : A.toSSet.obj m
y₂ : B.toSSet.obj m
⊢ Membership.mem (α := (tensorObj (𝒞 := Functor.category) X Y).obj m) ((A.prod B).obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (A.ι ⊗ₘ B.ι) m) :
          (a : (fun (X : Type u) ↦ X) ((A.toSSet ⊗ B.toSSet).obj m)) → (fun (X : Type u) ↦ X) ((X ⊗ Y).obj m))
        (y₁, y₂) :
      (fun (X : Type u) ↦ X) ((tensorObj (𝒞 := Functor.category) X Y).obj m))

Tactic:
⟨Subtype.coe_prop _, Subtype.coe_prop _⟩

Premises used: Subtype.coe_prop, Set.Mem, setOf, Set.prod, And.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
m : SimplexCategoryᵒᵖ
y₁ : A.toSSet.obj m
y₂ : B.toSSet.obj m
⊢ Membership.mem (α := (tensorObj (𝒞 := Functor.category) X Y).obj m) ((A.prod B).obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (A.ι ⊗ₘ B.ι) m) :
          (a : (fun (X : Type u) ↦ X) ((A.toSSet ⊗ B.toSSet).obj m)) → (fun (X : Type u) ↦ X) ((X ⊗ Y).obj m))
        (y₁, y₂) :
      (fun (X : Type u) ↦ X) ((tensorObj (𝒞 := Functor.category) X Y).obj m))

Tactic:
exact ⟨Subtype.coe_prop _, Subtype.coe_prop _⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
f : X ⟶ Y
⊢ ι₀ ≫ f ▷ Δ[1] = f ≫ ι₀

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.CartesianMonoidalCategory.lift, TypeCat.Fun.comp, SSet.ι₀, CategoryTheory.Monoidal.FunctorCategory.tensorObj, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
⊢ ι₀ ≫ fst X Δ[1] = 𝟙 X

Tactic:
rfl

Premises used: TypeCat.Fun.id, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
⊢ ι₀ ≫ snd X Δ[1] = const ((Equiv.symm stdSimplex.obj₀Equiv : (a : Fin (1 + 1)) → Δ[1] _⦋0⦌) 0)

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, SSet.const, TypeCat.Fun.comp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
m : SimplexCategoryᵒᵖ
x : X.obj m
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₀ m) : (a : X.obj m) → X.obj m ⊗ Δ[1].obj m) x).1 = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
m : ℕ
x : X _⦋m⦌
k : Fin (m + 1)
⊢ Eq (α := Fin 2)
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₀ (Opposite.op ⦋m⦌)) :
                (a : X _⦋m⦌) → X _⦋m⦌ ⊗ Δ[1] _⦋m⦌)
              x).2 :
          (a : Fin (m + 1)) → Fin 2)
        k :
      Fin 2)
    (0 : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
⊢ ι₁ ≫ fst X Δ[1] = 𝟙 X

Tactic:
rfl

Premises used: TypeCat.Fun.id, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
⊢ ι₁ ≫ snd X Δ[1] = const ((Equiv.symm stdSimplex.obj₀Equiv : (a : Fin (1 + 1)) → Δ[1] _⦋0⦌) 1)

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, SSet.const, TypeCat.Fun.comp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
f : X ⟶ Y
⊢ ι₁ ≫ f ▷ Δ[1] = f ≫ ι₁

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.CartesianMonoidalCategory.lift, TypeCat.Fun.comp, CategoryTheory.Monoidal.FunctorCategory.tensorObj, SSet.ι₁, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
m : SimplexCategoryᵒᵖ
x : X.obj m
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₁ m) : (a : X.obj m) → X.obj m ⊗ Δ[1].obj m) x).1 = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
m : ℕ
x : X _⦋m⦌
k : Fin (m + 1)
⊢ Eq (α := Fin 2)
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ι₁ (Opposite.op ⦋m⦌)) :
                (a : X _⦋m⦌) → X _⦋m⦌ ⊗ Δ[1] _⦋m⦌)
              x).2 :
          (a : Fin (m + 1)) → Fin 2)
        k :
      Fin 2)
    (1 : Fin (HAdd.hAdd (α := ℕ) 1 1))

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
z : (tensorObj (𝒞 := Functor.category) X Y).obj m
⊢ Eq (α := X.obj n)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f ⊗ₘ Y.map f) : (a : X.obj m ⊗ Y.obj m) → X.obj n ⊗ Y.obj n)
          z).1 :
      X.obj n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) : (a : X.obj m) → X.obj n) z.1 : X.obj n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
z : (tensorObj (𝒞 := Functor.category) X Y).obj m
⊢ Eq (α := Y.obj n)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f ⊗ₘ Y.map f) : (a : X.obj m ⊗ Y.obj m) → X.obj n ⊗ Y.obj n)
          z).2 :
      Y.obj n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) : (a : Y.obj m) → Y.obj n) z.2 : Y.obj n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
n : ℕ
i : Fin (n + 2)
z : tensorObj (𝒞 := Functor.category) X Y _⦋n + 1⦌
⊢ Eq (α := X _⦋n⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (tensorObj (𝒞 := Functor.category) X Y) i) :
            (a : X _⦋n + 1⦌ ⊗ Y _⦋n + 1⦌) → X _⦋n⦌ ⊗ Y _⦋n⦌)
          z).1 :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) : (a : X _⦋n + 1⦌) → X _⦋n⦌) z.1 : X _⦋n⦌)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
n : ℕ
i : Fin (n + 2)
z : tensorObj (𝒞 := Functor.category) X Y _⦋n + 1⦌
⊢ Eq (α := Y _⦋n⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (tensorObj (𝒞 := Functor.category) X Y) i) :
            (a : X _⦋n + 1⦌ ⊗ Y _⦋n + 1⦌) → X _⦋n⦌ ⊗ Y _⦋n⦌)
          z).2 :
      Y _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Y i) : (a : Y _⦋n + 1⦌) → Y _⦋n⦌) z.2 : Y _⦋n⦌)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
n : ℕ
i : Fin (n + 1)
z : tensorObj (𝒞 := Functor.category) X Y _⦋n⦌
⊢ Eq (α := X _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (tensorObj (𝒞 := Functor.category) X Y) i) :
            (a : X _⦋n⦌ ⊗ Y _⦋n⦌) → X _⦋n + 1⦌ ⊗ Y _⦋n + 1⦌)
          z).1 :
      X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) z.1 : X _⦋n + 1⦌)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
n : ℕ
i : Fin (n + 1)
z : tensorObj (𝒞 := Functor.category) X Y _⦋n⦌
⊢ Eq (α := Y _⦋n + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (tensorObj (𝒞 := Functor.category) X Y) i) :
            (a : X _⦋n⦌ ⊗ Y _⦋n⦌) → X _⦋n + 1⦌ ⊗ Y _⦋n + 1⦌)
          z).2 :
      Y _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ Y i) : (a : Y _⦋n⦌) → Y _⦋n + 1⦌) z.2 : Y _⦋n + 1⦌)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ prod ⊤ T ≤ S.unionProd T

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ S.prod ⊤ ≤ S.unionProd T

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ S.prod T ≤ S.unionProd T

Tactic:
(prod_le_prod_top S T).trans (prod_top_le_unionProd S T)

Premises used: SSet.Subcomplex.prod_top_le_unionProd, LE.le.trans, SSet.Subcomplex.prod_le_prod_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
m : SimplexCategoryᵒᵖ
y₁ : X.obj m
y₂ : T.toSSet.obj m
⊢ Membership.mem (α := (tensorObj (𝒞 := Functor.category) X Y).obj m) ((S.unionProd T).obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (X ◁ T.ι) m) :
          (a : (fun (X : Type u) ↦ X) ((X ⊗ T.toSSet).obj m)) → (fun (X : Type u) ↦ X) ((X ⊗ Y).obj m))
        (y₁, y₂) :
      (fun (X : Type u) ↦ X) ((tensorObj (𝒞 := Functor.category) X Y).obj m))

Tactic:
Or.inl ⟨Set.mem_univ _, Subtype.coe_prop _⟩

Premises used: Set.union, Subtype.coe_prop, Set.Mem, setOf, And.intro, Set.mem_univ, Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
m : SimplexCategoryᵒᵖ
y₁ : X.obj m
y₂ : T.toSSet.obj m
⊢ Membership.mem (α := (tensorObj (𝒞 := Functor.category) X Y).obj m) ((S.unionProd T).obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (X ◁ T.ι) m) :
          (a : (fun (X : Type u) ↦ X) ((X ⊗ T.toSSet).obj m)) → (fun (X : Type u) ↦ X) ((X ⊗ Y).obj m))
        (y₁, y₂) :
      (fun (X : Type u) ↦ X) ((tensorObj (𝒞 := Functor.category) X Y).obj m))

Tactic:
exact Or.inl ⟨Set.mem_univ _, Subtype.coe_prop _⟩

Premises used: Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
m : SimplexCategoryᵒᵖ
y₁ : S.toSSet.obj m
y₂ : Y.obj m
⊢ Membership.mem (α := (tensorObj (𝒞 := Functor.category) X Y).obj m) ((S.unionProd T).obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (S.ι ▷ Y) m) :
          (a : (fun (X : Type u) ↦ X) ((S.toSSet ⊗ Y).obj m)) → (fun (X : Type u) ↦ X) ((X ⊗ Y).obj m))
        (y₁, y₂) :
      (fun (X : Type u) ↦ X) ((tensorObj (𝒞 := Functor.category) X Y).obj m))

Tactic:
Or.inr ⟨Subtype.coe_prop _, Set.mem_univ _⟩

Premises used: Set.union, Subtype.coe_prop, Set.Mem, setOf, And.intro, Set.mem_univ, Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
m : SimplexCategoryᵒᵖ
y₁ : S.toSSet.obj m
y₂ : Y.obj m
⊢ Membership.mem (α := (tensorObj (𝒞 := Functor.category) X Y).obj m) ((S.unionProd T).obj m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (S.ι ▷ Y) m) :
          (a : (fun (X : Type u) ↦ X) ((S.toSSet ⊗ Y).obj m)) → (fun (X : Type u) ↦ X) ((X ⊗ Y).obj m))
        (y₁, y₂) :
      (fun (X : Type u) ↦ X) ((tensorObj (𝒞 := Functor.category) X Y).obj m))

Tactic:
exact Or.inr ⟨Subtype.coe_prop _, Set.mem_univ _⟩

Premises used: Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₁ S T ≫ (S.unionProd T).ι = X ◁ T.ι

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Monoidal.FunctorCategory.whiskerLeft, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ ι₂ S T ≫ (S.unionProd T).ι = S.ι ▷ Y

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Monoidal.FunctorCategory.whiskerRight, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
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
⊢ prod ⊤ T ⊓ S.prod ⊤ = S.prod T

Tactic:
ext n ⟨x, y⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
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
⊢ 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

Tactic:
simp [prod, Set.prod, Membership.mem, Set.Mem, setOf]

Premises used: Set.Mem, SSet.Subcomplex.prod, setOf, Set.prod, Membership.mem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
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
obj₄ : Set.univ x → T.obj n y → S.obj n x → Set.univ y → S.obj n x
obj₅ : Set.univ x → T.obj n y → S.obj n x → Set.univ y → T.obj n y
obj₆ obj₇ : S.obj n x → T.obj n y → (Set.univ x ∧ T.obj n y) ∧ S.obj n x ∧ Set.univ y
obj₈ : S.obj n x → T.obj n y → Set.univ x
obj₉ : S.obj n x → T.obj n y → T.obj n y
obj₁₀ : S.obj n x → T.obj n y → S.obj n x
obj₁₁ : S.obj n x → T.obj n y → Set.univ y
obj₁₂ obj₁₃ obj₁₄ : S.obj n x → T.obj n y → Set.univ x
obj₁₅ obj₁₆ obj₁₇ : S.obj n x → T.obj n y → Set.univ y
obj₁₈ obj₁₉ : S.obj n x → T.obj n y → Set.univ x
obj₂₀ obj₂₁ : S.obj n x → T.obj n y → 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

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ IsPushout (S.ι ▷ T.toSSet) (S.toSSet ◁ T.ι) (ι₁ S T) (ι₂ S T)

Tactic:
(bicartSq S T).isPushout.of_iso (S.prodIso T)
    (prodIso _ _ ≪≫ whiskerRightIso (topIso X) _)
    (prodIso _ _ ≪≫ whiskerLeftIso _ (topIso Y))
    (Iso.refl _) rfl rfl rfl rfl

Premises used: CategoryTheory.MonoidalCategory.whiskerLeftIso, CategoryTheory.MonoidalCategory.whiskerRightIso, CategoryTheory.Iso.refl, SSet.Subcomplex.topIso, SSet.Subcomplex.BicartSq.isPushout, CategoryTheory.Iso.trans, CategoryTheory.IsPushout.of_iso, SSet.Subcomplex.unionProd.bicartSq, rfl, SSet.Subcomplex.prodIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
obj :
  ∀ (n : SimplexCategoryᵒᵖ) (x : Y.obj n) (y : X.obj n),
    (x, y) ∈ ((S.unionProd T).preimage (Iso.hom (β_ Y X))).obj n ↔ (x, y) ∈ (T.unionProd S).obj n
⊢ (S.unionProd T).preimage (Iso.hom (β_ Y X)) = T.unionProd S

Tactic:
ext n ⟨x, y⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : Y.obj n
y : X.obj n
obj :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.hom (β_ Y X)) n) : (a : (Y ⊗ X).obj n) → (X ⊗ Y).obj n)
            (x, y)).2 ∈
        T.obj n ∨
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.hom (β_ Y X)) n) :
              (a : (Y ⊗ X).obj n) → (X ⊗ Y).obj n)
            (x, y)).1 ∈
        S.obj n ↔
    y ∈ S.obj n ∨ x ∈ T.obj n
⊢ (x, y) ∈ ((S.unionProd T).preimage (Iso.hom (β_ Y X))).obj n ↔ (x, y) ∈ (T.unionProd S).obj n

Tactic:
simp only [mem_unionProd_iff, preimage_obj, Set.mem_preimage]

Premises used: SSet.Subcomplex.mem_unionProd_iff, SSet.Subcomplex.preimage_obj, Set.mem_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).preimage (Iso.inv (β_ X Y)) = T.unionProd S

Tactic:
apply preimage_β_hom

Premises used: SSet.Subcomplex.unionProd.preimage_β_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
rw : ((T.unionProd S).preimage (Iso.hom (β_ X Y))).image (Iso.hom (β_ X Y)) = T.unionProd S
rw₁ rw₂ : T.unionProd S = T.unionProd S
⊢ (S.unionProd T).image (Iso.hom (β_ X Y)) = T.unionProd S

Tactic:
rw [← preimage_β_hom, preimage_image_of_isIso]

Premises used: SSet.Subcomplex.preimage_image_of_isIso, SSet.Subcomplex.unionProd.preimage_β_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).image (Iso.inv (β_ Y X)) = T.unionProd S

Tactic:
apply image_β_hom

Premises used: SSet.Subcomplex.unionProd.image_β_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ range ((S.unionProd T).ι ≫ Iso.hom (β_ X Y)) ≤ T.unionProd S

Tactic:
simp [range_comp]

Premises used: SSet.Subcomplex.range_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ range ((T.unionProd S).ι ≫ Iso.hom (β_ Y X)) ≤ S.unionProd T

Tactic:
simp [range_comp]

Premises used: SSet.Subcomplex.range_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
n : ℕ
X Y : Truncated n
d e : (SimplexCategory.Truncated n)ᵒᵖ
f : d ⟶ e
x : (tensorObj (𝒞 := Functor.category) X Y).obj d
⊢ Eq (α := X.obj e)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f ⊗ₘ Y.map f) : (a : X.obj d ⊗ Y.obj d) → X.obj e ⊗ Y.obj e)
          x).1 :
      X.obj e)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) : (a : X.obj d) → X.obj e) x.1 : X.obj e)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
n : ℕ
X Y : Truncated n
d e : (SimplexCategory.Truncated n)ᵒᵖ
f : d ⟶ e
x : (tensorObj (𝒞 := Functor.category) X Y).obj d
⊢ Eq (α := Y.obj e)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f ⊗ₘ Y.map f) : (a : X.obj d ⊗ Y.obj d) → X.obj e ⊗ Y.obj e)
          x).2 :
      Y.obj e)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) : (a : Y.obj d) → Y.obj e) x.2 : Y.obj e)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : TopologicalSpace R
inst_8 : TopologicalSpace S
a : A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_cpct : CompactSpace.{u_2} (↑(spectrum S a) : Type u_2)
rw : ∀ (h_cpct : IsCompact (spectrum S a)), IsCompact (spectrum R a)
⊢ CompactSpace.{u_1} (↑(spectrum R a) : Type u_1)

Tactic:
rw [← isCompact_iff_compactSpace] at h_cpct ⊢

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : TopologicalSpace R
inst_8 : TopologicalSpace S
a : A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_cpct : IsCompact (spectrum S a)
⊢ IsCompact (spectrum R a)

Tactic:
h.image ▸ h_cpct.image (map_continuous f)

Premises used: Eq.rec, SpectrumRestricts.image, ContinuousMapClass.map_continuous, IsCompact.image
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : Semifield S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : TopologicalSpace R
inst_8 : TopologicalSpace S
a : A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_cpct : IsCompact (spectrum S a)
⊢ IsCompact (spectrum R a)

Tactic:
exact h.image ▸ h_cpct.image (map_continuous f)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id :
  (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A) (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
simp :
  (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A)
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ }
        (ContinuousMap.comp (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R))
          {
            toFun :=
              Subtype.map (p := fun (x : S) ↦ x ∈ spectrum S a) (q := fun (x : R) ↦ x ∈ spectrum R a) (⇑f : (a : S) → R)
                ⋯,
            continuous_toFun := ⋯ })) =
    a
⊢ (starAlgHom φ h : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    a

Tactic:
simp only [SpectrumRestricts.starAlgHom_apply]

Premises used: SpectrumRestricts.starAlgHom_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
a : A
φ : C((↑(spectrum S a) : Type u_2), S) →⋆ₐ[S] A
f : C(S, R)
h : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
h_id :
  (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A) (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a
⊢ (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A) (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a

Tactic:
h_id