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

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ s □ t ⊆ s ○ t
Tactic:
simp_rw [subset_iff, mem_certificator, mem_disjSups]
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ ∀ ⦃x : α⦄,
    (∃ x_1 y, IsCompl x_1 y ∧ (∀ ⦃b : α⦄, x ⊓ x_1 = b ⊓ x_1 → b ∈ s) ∧ ∀ ⦃b : α⦄, x ⊓ y = b ⊓ y → b ∈ t) →
      ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x

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

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a x u v : α
huv : IsCompl u v
hu : ∀ ⦃b : α⦄, x ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, x ⊓ v = b ⊓ v → b ∈ t
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x
Tactic:
refine' ⟨x ⊓ u, hu (inf_right_idem _ _).symm, x ⊓ v, hv (inf_right_idem _ _).symm,
  huv.disjoint.mono inf_le_right inf_le_right, _⟩
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a x u v : α
huv : IsCompl u v
hu : ∀ ⦃b : α⦄, x ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, x ⊓ v = b ⊓ v → b ∈ t
⊢ x ⊓ u ⊔ x ⊓ v = x

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a x u v : α
huv : IsCompl u v
hu : ∀ ⦃b : α⦄, x ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, x ⊓ v = b ⊓ v → b ∈ t
⊢ x ⊓ u ⊔ x ⊓ v = x
Tactic:
rw [← inf_sup_left, huv.codisjoint.eq_top, inf_top_eq]
State after:
no goals