Theorem: Finset.IsLowerSet.certificator_eq_inter (LeanCamCombi/VanDenBergKesten.lean)

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
⊢ s □ t = s ∩ t
Tactic:
refine' certificator_subset_inter.antisymm fun a ha ↦
  mem_certificator.2 ⟨aᶜ, a, isCompl_compl.symm, _⟩
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∩ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∩ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t
Tactic:
rw [mem_inter] at ha
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t
Tactic:
simp only [@eq_comm _ ⊥, ← sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff]
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, b ≤ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ≤ b → b ∈ t

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, b ≤ a → b ∈ s) ∧ ∀ ⦃b : α⦄, a ≤ b → b ∈ t
Tactic:
exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩
State after:
no goals