-- 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
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
⊢ ((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₉ : 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