-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
x : α
h :
  (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t →
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₁ :
  (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t) →
    (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₂ : x ∈ t → x ∈ s₁ → x ∈ s₂ → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₃ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₄ : x ∈ t → x ∈ s₁ → x ∈ s₂ → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₅ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₆ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t
h₇ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t
h₈ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t
h₉ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t
h₁₀ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₁ : x ∈ s₁ → x ∈ t → x ∈ s₂' → ¬x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₂ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂ → x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₃ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₄ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₅ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₆ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → x ∈ s₁'
h₁₇ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → x ∈ s₂'
h₁₈ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → ¬x ∈ t
h₁₉ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → x ∈ s₁'
h₂₀ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → x ∈ s₂'
h₂₁ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → ¬x ∈ t
h₂₂ h₂₃ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t
h₂₄ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬(x ∈ s₁ ∧ x ∈ t) → x ∈ s₁'
h₂₅ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬(x ∈ s₁ ∧ x ∈ t) → ¬x ∈ t
h₂₆ h₂₇ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t
h₂₈ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬(x ∈ s₂ ∧ x ∈ t) → x ∈ s₂'
h₂₉ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬(x ∈ s₂ ∧ x ∈ t) → ¬x ∈ t
h₃₀ h₃₁ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t
h₃₂ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → ¬(x ∈ s₁ ∧ x ∈ t) → x ∈ s₁'
h₃₃ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → ¬(x ∈ s₁ ∧ x ∈ t) → ¬x ∈ t
h₃₄ h₃₅ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t
h₃₆ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → ¬(x ∈ s₂ ∧ x ∈ t) → x ∈ s₂'
h₃₇ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → ¬(x ∈ s₂ ∧ x ∈ t) → ¬x ∈ t
h₃₈ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬(x ∈ s₁ ∧ x ∈ s₂) → x ∈ s₁'
h₃₉ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬x ∈ t → x ∈ s₁'
h₄₀ h₄₁ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬(x ∈ s₁ ∧ x ∈ s₂) → x ∈ s₁'
h₄₂ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬(x ∈ s₁ ∧ x ∈ s₂) → x ∈ s₂'
h₄₃ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬x ∈ t → x ∈ s₂'
h₄₄ h₄₅ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬(x ∈ s₁ ∧ x ∈ s₂) → x ∈ s₂'
h₄₆ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → x ∈ t → ¬(x ∈ s₁ ∧ x ∈ s₂) → False
h₄₇ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → x ∈ t → ¬x ∈ t → False
h₄₈ h₄₉ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → x ∈ t → ¬(x ∈ s₁ ∧ x ∈ s₂) → False
h₅₀ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬x ∈ s₁ → x ∈ s₁'
h₅₁ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬x ∈ t → x ∈ s₁'
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
have h₅₂ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ t → ¬x ∈ s₁ → False
Tactic: tauto