Theorem: Finset.IsUpperSet.certificator_eq_disjSups (LeanCamCombi/VanDenBergKesten.lean)

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
⊢ s □ t = s ○ t
Tactic:
refine' certificator_subset_disjSups.antisymm fun a ha ↦ mem_certificator.2 _
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ○ t
⊢ ∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ○ t
⊢ ∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t
Tactic:
obtain ⟨x, hx, y, hy, hxy, rfl⟩ := mem_disjSups.1 ha
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ ∃ x_1 y_1, IsCompl x_1 y_1 ∧ (∀ ⦃b : α⦄, (x ⊔ y) ⊓ x_1 = b ⊓ x_1 → b ∈ s) ∧ ∀ ⦃b : α⦄, (x ⊔ y) ⊓ y_1 = b ⊓ y_1 → b ∈ t

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ ∃ x_1 y_1, IsCompl x_1 y_1 ∧ (∀ ⦃b : α⦄, (x ⊔ y) ⊓ x_1 = b ⊓ x_1 → b ∈ s) ∧ ∀ ⦃b : α⦄, (x ⊔ y) ⊓ y_1 = b ⊓ y_1 → b ∈ t
Tactic:
refine' ⟨x, xᶜ, isCompl_compl, _⟩
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ (∀ ⦃b : α⦄, (x ⊔ y) ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, (x ⊔ y) ⊓ xᶜ = b ⊓ xᶜ → b ∈ t

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ (∀ ⦃b : α⦄, (x ⊔ y) ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, (x ⊔ y) ⊓ xᶜ = b ⊓ xᶜ → b ∈ t
Tactic:
simp only [inf_of_le_right, le_sup_left, right_eq_inf, ← sdiff_eq, hxy.sup_sdiff_cancel_left]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ (∀ ⦃b : α⦄, x ≤ b → b ∈ s) ∧ ∀ ⦃b : α⦄, y = b \ x → b ∈ t

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Disjoint x y
ha : x ⊔ y ∈ s ○ t
⊢ (∀ ⦃b : α⦄, x ≤ b → b ∈ s) ∧ ∀ ⦃b : α⦄, y = b \ x → b ∈ t
Tactic:
exact ⟨fun b hab ↦ hs hab hx, fun b hab ↦ ht (hab.trans_le sdiff_le) hy⟩
State after:
no goals