Theorem: FilterGame.Filter.mem_inf_principal_iff (FilterGame/Solutions/Semilattice.lean)

State before:
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t → {x | x ∈ t → x ∈ s} ∈ f

case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t

State before:
case mp
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t → {x | x ∈ t → x ∈ s} ∈ f

case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
Tactic:
. intros hs
  rw [mem_inf_def] at hs
  have ⟨a, ha, b, hb, hsab⟩ := hs
  clear hs
  rw [hsab]; clear hsab
  rw [mem_principal_def] at hb
  suffices h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
  . exact superset_mem ha h
  intros x hxa hxt
  exact ⟨hxa, hb hxt⟩
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
Tactic:
. intros h
  have heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
  . apply Set.ext; intros x
    rw [Set.mem_iff, Set.mem_union, Set.mem_compl_iff, imp_iff_not_or]
  rw [heq] at h; clear heq
  have heq : s = (tᶜ ∪ s) ∩ (t ∪ s) 
  . rw [← Set.union_distrib_right, Set.compl_inter_self, Set.empty_union]
  rw [heq]; clear heq
  refine inter_mem_inf h ?_
  rw [mem_principal_def]
  exact Set.subset_union_left _ _
State after:
no goals

State before:
case mp
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t → {x | x ∈ t → x ∈ s} ∈ f
Tactic:
intros hs
State after:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : s ∈ f ⊓ 𝓟 t
⊢ {x | x ∈ t → x ∈ s} ∈ f

State before:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : s ∈ f ⊓ 𝓟 t
⊢ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
rw [mem_inf_def] at hs
State after:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : ∃ a, a ∈ f ∧ ∃ b, b ∈ 𝓟 t ∧ s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f

State before:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : ∃ a, a ∈ f ∧ ∃ b, b ∈ 𝓟 t ∧ s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
have ⟨a, ha, b, hb, hsab⟩ := hs
State after:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : ∃ a, a ∈ f ∧ ∃ b, b ∈ 𝓟 t ∧ s = a ∩ b
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f

State before:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : ∃ a, a ∈ f ∧ ∃ b, b ∈ 𝓟 t ∧ s = a ∩ b
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
clear hs
State after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f

State before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
rw [hsab]
State after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f

State before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Tactic:
clear hsab
State after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f

State before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Tactic:
rw [mem_principal_def] at hb
State after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f

State before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Tactic:
suffices h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
State after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f

case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}

State before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f

case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}
Tactic:
. exact superset_mem ha h
State after:
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}

State before:
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}
Tactic:
intros x hxa hxt
State after:
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
x : α
hxa : x ∈ a
hxt : x ∈ t
⊢ x ∈ a ∩ b

State before:
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
x : α
hxa : x ∈ a
hxt : x ∈ t
⊢ x ∈ a ∩ b
Tactic:
exact ⟨hxa, hb hxt⟩
State after:
no goals

State before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Tactic:
exact superset_mem ha h
State after:
no goals

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
Tactic:
intros h
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ s ∈ f ⊓ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
have heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
State after:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ {x | x ∈ t → x ∈ s} = tᶜ ∪ s

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t

State before:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ {x | x ∈ t → x ∈ s} = tᶜ ∪ s

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
. apply Set.ext; intros x
  rw [Set.mem_iff, Set.mem_union, Set.mem_compl_iff, imp_iff_not_or]
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
rw [heq] at h
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
clear heq
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s ∈ f ⊓ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
have heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
State after:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s = (tᶜ ∪ s) ∩ (t ∪ s)

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t

State before:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s = (tᶜ ∪ s) ∩ (t ∪ s)

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
. rw [← Set.union_distrib_right, Set.compl_inter_self, Set.empty_union]
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
rw [heq]
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ (tᶜ ∪ s) ∩ (t ∪ s) ∈ f ⊓ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ (tᶜ ∪ s) ∩ (t ∪ s) ∈ f ⊓ 𝓟 t
Tactic:
clear heq
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ (tᶜ ∪ s) ∩ (t ∪ s) ∈ f ⊓ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ (tᶜ ∪ s) ∩ (t ∪ s) ∈ f ⊓ 𝓟 t
Tactic:
refine inter_mem_inf h ?_
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ t ∪ s ∈ 𝓟 t

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ t ∪ s ∈ 𝓟 t
Tactic:
rw [mem_principal_def]
State after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ t ⊆ t ∪ s

State before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ t ⊆ t ∪ s
Tactic:
exact Set.subset_union_left _ _
State after:
no goals

State before:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ {x | x ∈ t → x ∈ s} = tᶜ ∪ s
Tactic:
apply Set.ext
State after:
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ ∀ (x : α), x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s

State before:
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ ∀ (x : α), x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s
Tactic:
intros x
State after:
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
x : α
⊢ x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s

State before:
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
x : α
⊢ x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s
Tactic:
rw [Set.mem_iff, Set.mem_union, Set.mem_compl_iff, imp_iff_not_or]
State after:
no goals

State before:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s = (tᶜ ∪ s) ∩ (t ∪ s)
Tactic:
rw [← Set.union_distrib_right, Set.compl_inter_self, Set.empty_union]
State after:
no goals