Theorem: Finset.mem_certificator (LeanCamCombi/VanDenBergKesten.lean)

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ a ∈ s □ t ↔ ∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t
Tactic:
rw [certificator, mem_filter, and_iff_right_of_imp]
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ (∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t) → a ∈ s ∩ t

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ (∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t) → a ∈ s ∩ t
Tactic:
rintro ⟨u, v, _, hu, hv⟩
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a u v : α
left✝ : IsCompl u v
hu : ∀ ⦃b : α⦄, a ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, a ⊓ v = b ⊓ v → b ∈ t
⊢ a ∈ s ∩ t

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a u v : α
left✝ : IsCompl u v
hu : ∀ ⦃b : α⦄, a ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, a ⊓ v = b ⊓ v → b ∈ t
⊢ a ∈ s ∩ t
Tactic:
exact mem_inter.2 ⟨hu rfl, hv rfl⟩
State after:
no goals