awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
⊢ sSup T ∈ S
have inl : ∀ (hT : ∅ ⊆ S) (ha : IsAtom.{u_1} (α := α) (sSup ∅)) (haS : sSup ∅ ≤ sSup S), sSup ∅ ∈ S
Tactic: obtain rfl | ⟨a, haT⟩ := T.eq_empty_or_nonempty
Cleared hypotheses: T, hT, ha, haS
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
inl : ∀ (hT : ∅ ⊆ S) (ha : IsAtom.{u_1} (α := α) (sSup ∅)) (haS : sSup ∅ ≤ sSup S), sSup ∅ ∈ S
⊢ sSup T ∈ S
have inr : ∀ (a : α) (haT : a ∈ T), sSup T ∈ S
Tactic: obtain rfl | ⟨a, haT⟩ := T.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
hT : ∅ ⊆ S
ha : IsAtom.{u_1} (α := α) (sSup ∅)
haS : sSup ∅ ≤ sSup S
⊢ sSup ∅ ∈ S
have ha₁ : IsAtom.{u_1} (α := α) ⊥
Tactic: simp only [sSup_empty] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
⊢ sSup T ∈ S
have inr : sSup T = a
Tactic: suffices sSup T = a from this ▸ hT haT
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
⊢ sSup T = a
have this : a ≤ sSup T
Tactic: have : a ≤ sSup T := le_sSup haT
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
this : a ≤ sSup T
⊢ sSup T = a
have inr : a ≠ ⊥
Tactic: rwa [ha.le_iff_eq, eq_comm] at this
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂
have a : sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
a : sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂
⊢ sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂
have a₁ : sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂
have a : sSup (T₁ ∩ T₂) ≤ sSup T₁
Tactic: apply le_inf
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
a : sSup (T₁ ∩ T₂) ≤ sSup T₁
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂
have a₁ : sSup (T₁ ∩ T₂) ≤ sSup T₂
Tactic: apply le_inf
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
⊢ sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
have a : ∀ (X : Set α) (hX : X ⊆ S) (hX' : sSup T₁ ⊓ sSup T₂ = sSup X), sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
Tactic: obtain ⟨X, hX, hX'⟩ := hS.atomistic (sSup T₁ ⊓ sSup T₂) (inf_le_left.trans (sSup_le_sSup hT₁))
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
⊢ sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
have a : sSup X ≤ sSup (T₁ ∩ T₂)
Tactic: rw [hX']
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
⊢ sSup X ≤ sSup (T₁ ∩ T₂)
have a : ∀ b ∈ X, b ≤ sSup (T₁ ∩ T₂)
Tactic: apply _root_.sSup_le
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ≤ sSup (T₁ ∩ T₂)
have a : I ∈ T₁ ∩ T₂
Tactic: apply _root_.le_sSup
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ∈ T₁ ∩ T₂
have a : I ∈ T₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
a : I ∈ T₁
⊢ I ∈ T₁ ∩ T₂
have a₁ : I ∈ T₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ∈ T₁
have apply : IsAtom I
Tactic: apply (hS.mono hT₁).mem_of_isAtom_of_le_sSup_atoms _ _ _
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
apply : IsAtom I
⊢ I ∈ T₁
have apply₁ : I ≤ sSup T₁
Tactic: apply (hS.mono hT₁).mem_of_isAtom_of_le_sSup_atoms _ _ _
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ∈ T₂
have apply : IsAtom I
Tactic: apply (hS.mono hT₂).mem_of_isAtom_of_le_sSup_atoms _ _ _
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
apply : IsAtom I
⊢ I ∈ T₂
have apply₁ : I ≤ sSup T₂
Tactic: apply (hS.mono hT₂).mem_of_isAtom_of_le_sSup_atoms _ _ _
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have obtain : ∀ (Ta : Set α) (hTa : Ta ⊆ S), (sSup Ta ⊔ b) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ b ⊓ c
Tactic: obtain ⟨Ta, hTa, rfl⟩ := hS.atomistic a (h ▸ le_top)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
b c : α
Ta : Set α
hTa : Ta ⊆ S
⊢ (sSup Ta ⊔ b) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ b ⊓ c
have obtain : ∀ (Tb : Set α) (hTb : Tb ⊆ S), (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ sSup Tb ⊓ c
Tactic: obtain ⟨Tb, hTb, rfl⟩ := hS.atomistic b (h ▸ le_top)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
c : α
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
⊢ (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ sSup Tb ⊓ c
have obtain : ∀ (Tc : Set α) (hTc : Tc ⊆ S), (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) ≤ sSup Ta ⊔ sSup Tb ⊓ sSup Tc
Tactic: obtain ⟨Tc, hTc, rfl⟩ := hS.atomistic c (h ▸ le_top)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) ≤ sSup Ta ⊔ sSup Tb ⊓ sSup Tc
have hab : (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) = sSup Ta ⊔ sSup Tb ⊓ sSup Tc
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) = sSup Ta ⊔ sSup Tb ⊓ sSup Tc
have hab : sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)
Tactic: rw [← sSup_union, ← sSup_union, ← hS.sSup_inter hTb hTc, ← hS.sSup_inter, ← sSup_union]
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)
⊢ (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) = sSup Ta ⊔ sSup Tb ⊓ sSup Tc
have hab₁ : Ta ∪ Tb ⊆ S
Tactic: rw [← sSup_union, ← sSup_union, ← hS.sSup_inter hTb hTc, ← hS.sSup_inter, ← sSup_union]
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)
hab₁ : Ta ∪ Tb ⊆ S
⊢ (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) = sSup Ta ⊔ sSup Tb ⊓ sSup Tc
have hab₂ : Ta ∪ Tc ⊆ S
Tactic: rw [← sSup_union, ← sSup_union, ← hS.sSup_inter hTb hTc, ← hS.sSup_inter, ← sSup_union]
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)
have hab : (Ta ∪ Tb) ∩ (Ta ∪ Tc) = Ta ∪ Tb ∩ Tc
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ (Ta ∪ Tb) ∩ (Ta ∪ Tc) = Ta ∪ Tb ∩ Tc
have hab : ∀ (x : α), x ∈ (Ta ∪ Tb) ∩ (Ta ∪ Tc) ↔ x ∈ Ta ∪ Tb ∩ Tc
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)
have hab : ∀ (x : α), x ∈ (Ta ∪ Tb) ∩ (Ta ∪ Tc) ↔ x ∈ Ta ∪ Tb ∩ Tc
Tactic: on_goal 1 => congr 1; ext
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₁ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₁ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₂ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tb
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₁ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₁₂ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tb
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₃ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tc
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₁ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₁₂ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tb
hab₁₃ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₄ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tb
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₁ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₁₂ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tb
hab₁₃ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tc
hab₁₄ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tb
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₅ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tc
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₁ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₁₂ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tb
hab₁₃ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tc
hab₁₄ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₅ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₆ : x ∈ Tb → x ∈ Tc → x ∉ Ta → x ∈ Tb
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₁ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₁₂ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tb
hab₁₃ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tc
hab₁₄ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₅ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₁₆ : x ∈ Tb → x ∈ Tc → x ∉ Ta → x ∈ Tb
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₇ : x ∈ Tb → x ∈ Tc → x ∉ Ta → x ∈ Tc
Tactic: tauto