awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
obj₄ : Set.univ x → T.obj n y → S.obj n x → Set.univ y → S.obj n x
⊢ (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 → 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
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
⊢ (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
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
⊢ (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
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
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
⊢ (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 → 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
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
⊢ (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 → S.obj n x
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
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
⊢ (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 y
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).preimage (Iso.hom (β_ Y X)) = T.unionProd S
have 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
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 : 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
have 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
Tactic: simp only [mem_unionProd_iff, preimage_obj, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : Y.obj n
y : X.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)).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
have 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
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 : 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
⊢ ((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
have obj₁ : y ∈ S.obj n ∨ x ∈ 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)).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
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 : 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
obj₁ :
  y ∈ S.obj n ∨ x ∈ 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)).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
⊢ ((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
have 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 →
  y ∈ S.obj n ∨ x ∈ T.obj n
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 : 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
obj₁ :
  y ∈ S.obj n ∨ x ∈ 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)).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
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 →
    y ∈ S.obj n ∨ x ∈ 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)).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
have obj₃ : ((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
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 : 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
obj₁ :
  y ∈ S.obj n ∨ x ∈ 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)).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
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 →
    y ∈ S.obj n ∨ x ∈ T.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)).1 ∈
      S.obj n →
    y ∈ S.obj n ∨ x ∈ T.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 →
    y ∈ S.obj n ∨ x ∈ T.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)).1 ∈
      S.obj n →
    y ∈ S.obj n ∨ x ∈ 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)).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
have 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 →
  y ∉ S.obj n → x ∈ T.obj n
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 : 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
obj₁ :
  y ∈ S.obj n ∨ x ∈ 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)).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
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 →
    y ∈ S.obj n ∨ x ∈ T.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)).1 ∈
      S.obj n →
    y ∈ S.obj n ∨ x ∈ T.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 →
    y ∈ S.obj n ∨ x ∈ T.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)).1 ∈
      S.obj n →
    y ∈ S.obj n ∨ x ∈ T.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 →
    y ∉ S.obj n → x ∈ 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)).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
have obj₇ : ((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
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 : 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
obj₁ :
  y ∈ S.obj n ∨ x ∈ 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)).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
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 →
    y ∈ S.obj n ∨ x ∈ T.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)).1 ∈
      S.obj n →
    y ∈ S.obj n ∨ x ∈ T.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 →
    y ∈ S.obj n ∨ x ∈ T.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)).1 ∈
      S.obj n →
    y ∈ S.obj n ∨ x ∈ T.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 →
    y ∉ S.obj n → x ∈ T.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)).1 ∈
      S.obj n →
    y ∉ S.obj n → x ∈ 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)).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
have obj₈ : y ∈ S.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)).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
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
Goal:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).image (Iso.hom (β_ X Y)) = T.unionProd S
have rw : ((T.unionProd S).preimage (Iso.hom (β_ X Y))).image (Iso.hom (β_ X Y)) = T.unionProd S
Tactic: rw [← preimage_β_hom, preimage_image_of_isIso]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Monoidal (goal)
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
⊢ (S.unionProd T).image (Iso.hom (β_ X Y)) = T.unionProd S
have rw₁ : T.unionProd S = T.unionProd S
Tactic: rw [← preimage_β_hom, preimage_image_of_isIso]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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)
⊢ CompactSpace.{u_1} (↑(spectrum R a) : Type u_1)
have rw : ∀ (h_cpct : IsCompact (spectrum S a)), IsCompact (spectrum R a)
Tactic: rw [← isCompact_iff_compactSpace] at h_cpct ⊢
Cleared hypotheses: h_cpct
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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
⊢ (starAlgHom φ h : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) =
    a
have simp : (φ : (a : C((↑(spectrum S a) : Type u_2), S)) → A)
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry }
      (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)
              sorry,
          continuous_toFun := sorry })) =
  a
Tactic: simp only [SpectrumRestricts.starAlgHom_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict (goal)
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.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
have h₁ : Eq (α := C((↑(spectrum S a) : Type u_2), S))
  (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry }
    (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) sorry,
        continuous_toFun := sorry }))
  (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S))
Tactic: convert! h_id