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

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ s □ t = t □ s
Tactic:
ext s
State after:
case a
α : Type u_1
inst✝ : BooleanAlgebra α
s✝ t u : Finset α
a s : α
⊢ s ∈ s✝ □ t ↔ s ∈ t □ s✝

State before:
case a
α : Type u_1
inst✝ : BooleanAlgebra α
s✝ t u : Finset α
a s : α
⊢ s ∈ s✝ □ t ↔ s ∈ t □ s✝
Tactic:
rw [mem_certificator, exists_comm]
State after:
case a
α : Type u_1
inst✝ : BooleanAlgebra α
s✝ t u : Finset α
a s : α
⊢ (∃ b a, IsCompl a b ∧ (∀ ⦃b : α⦄, s ⊓ a = b ⊓ a → b ∈ s✝) ∧ ∀ ⦃b_1 : α⦄, s ⊓ b = b_1 ⊓ b → b_1 ∈ t) ↔ s ∈ t □ s✝

State before:
case a
α : Type u_1
inst✝ : BooleanAlgebra α
s✝ t u : Finset α
a s : α
⊢ (∃ b a, IsCompl a b ∧ (∀ ⦃b : α⦄, s ⊓ a = b ⊓ a → b ∈ s✝) ∧ ∀ ⦃b_1 : α⦄, s ⊓ b = b_1 ⊓ b → b_1 ∈ t) ↔ s ∈ t □ s✝
Tactic:
simp [isCompl_comm, and_comm]
State after:
no goals