awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : Frame α
a : α
f : ι → α
⊢ Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)

Tactic:
simpa only [disjoint_comm] using @iSup_disjoint_iff

Premises used: disjoint_comm, iSup_disjoint_iff
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint (⨆ (i : ι), ⨆ (j : κ i), f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a

Tactic:
simp_rw [iSup_disjoint_iff]

Premises used: iSup_disjoint_iff
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint a (⨆ (i : ι), ⨆ (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)

Tactic:
simp_rw [disjoint_iSup_iff]

Premises used: disjoint_iSup_iff
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
a : α
s : Set α
⊢ Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a

Tactic:
simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]

Premises used: disjoint_iff, iSup_eq_bot, sSup_inf_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
a : α
s : Set α
⊢ Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b

Tactic:
simpa only [disjoint_comm] using @sSup_disjoint_iff

Premises used: sSup_disjoint_iff, disjoint_comm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ g i) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i)

Tactic:
(le_iSup_inf_iSup f g).antisymm ?_

Premises used: LE.le.antisymm, le_iSup_inf_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
refine : LE.le.{u} (α := α) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i) (⨆ (i : ι), f i ⊓ g i)
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ g i) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i)

Tactic:
refine (le_iSup_inf_iSup f g).antisymm ?_

Premises used: LE.le.antisymm, le_iSup_inf_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
rw : LE.le.{u} (α := α) (⨆ (i : ι × ι), f i.1 ⊓ g i.2) (⨆ (i : ι), f i ⊓ g i)
⊢ LE.le.{u} (α := α) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i) (⨆ (i : ι), f i ⊓ g i)

Tactic:
rw [iSup_inf_iSup]

Premises used: iSup_inf_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ LE.le.{u} (α := α) (⨆ (i : ι × ι), f i.1 ⊓ g i.2) (⨆ (i : ι), f i ⊓ g i)

Tactic:
iSup_mono' fun i => ?_

Premises used: iSup_mono'
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
refine : ∀ (i : ι × ι), ∃ (i' : ι), f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'
⊢ LE.le.{u} (α := α) (⨆ (i : ι × ι), f i.1 ⊓ g i.2) (⨆ (i : ι), f i ⊓ g i)

Tactic:
refine iSup_mono' fun i => ?_

Premises used: iSup_mono'
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
rcases : ∀ (j : ι) (h₁ : i.1 ≤ j) (h₂ : i.2 ≤ j), ∃ (i' : ι), f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'
⊢ ∃ (i' : ι), f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'

Tactic:
rcases directed_of (· ≤ ·) i.1 i.2 with ⟨j, h₁, h₂⟩

Premises used: LE.le, Prod.fst, directed_of, Prod.snd
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
j : ι
h₁ : i.1 ≤ j
h₂ : i.2 ≤ j
⊢ ∃ (i' : ι), f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'

Tactic:
⟨j, inf_le_inf (hf h₁) (hg h₂)⟩

Premises used: inf_le_inf, Exists.intro
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
j : ι
h₁ : i.1 ≤ j
h₂ : i.2 ≤ j
⊢ ∃ (i' : ι), f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'

Tactic:
exact ⟨j, inf_le_inf (hf h₁) (hg h₂)⟩
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsCodirectedOrder ι
f g : ι → α
hf : Antitone f
hg : Antitone g
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ g i) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i)

Tactic:
@iSup_inf_of_monotone α _ ιᵒᵈ _ _ f g hf.dual_left hg.dual_left

Premises used: Antitone.dual_left, OrderDual, iSup_inf_of_monotone
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
a b : α
⊢ a ⇨ b = sSup {w : α | w ⊓ a ≤ b}

Tactic:
(isGreatest_himp a b).isLUB.sSup_eq.symm

Premises used: setOf, isGreatest_himp, IsLUB.sSup_eq, IsGreatest.isLUB, Eq.symm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
a : α
⊢ aᶜ = sSup {w : α | Disjoint w a}

Tactic:
(isGreatest_compl a).isLUB.sSup_eq.symm

Premises used: setOf, IsLUB.sSup_eq, IsGreatest.isLUB, isGreatest_compl, Eq.symm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
a b c : α
⊢ a ⇨ b ≤ c ↔ ∀ (d : α), d ⊓ a ≤ b → d ≤ c

Tactic:
simp [himp_eq_sSup]

Premises used: himp_eq_sSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Frame α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : a ⊓ sSup {b, c} ≤ a ⊓ b ⊔ a ⊓ c
rw₁ : a ⊓ sSup {b, c} ≤ sSup {a ⊓ b, a ⊓ c}
rw₂ : LE.le (α := α) (⨆ (b_2 : α), ⨆ (_ : Membership.mem (γ := Set α) {b, c} b_2), a ⊓ b_2) (sSup {a ⊓ b, a ⊓ c})
rw₃ : sSup (min a '' {b, c}) ≤ sSup {a ⊓ b, a ⊓ c}
rw₄ rw₅ : LE.le (α := α) (sSup {a ⊓ b, a ⊓ c}) (sSup {a ⊓ b, a ⊓ c})
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c

Tactic:
rw [← sSup_pair, ← sSup_pair, inf_sSup_eq, ← sSup_image, image_pair]

Premises used: Set.image_pair, inf_sSup_eq, sSup_image, sSup_pair
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
s : Set α
b : α
⊢ sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b

Tactic:
@sSup_inf_eq αᵒᵈ _ _ _

Premises used: iInf, Set.Mem, OrderDual, sSup_inf_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : Coframe α
f : ι → α
a : α
⊢ (⨅ (i : ι), f i) ⊔ a = ⨅ (i : ι), f i ⊔ a

Tactic:
@iSup_inf_eq αᵒᵈ _ _ _ _

Premises used: iInf, iSup_inf_eq, OrderDual
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : Coframe α
a : α
f : ι → α
⊢ a ⊔ ⨅ (i : ι), f i = ⨅ (i : ι), a ⊔ f i

Tactic:
@inf_iSup_eq αᵒᵈ _ _ _ _

Premises used: iInf, inf_iSup_eq, OrderDual
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : Coframe α
f : (i : ι) → κ i → α
a : α
⊢ (⨅ (i : ι), ⨅ (j : κ i), f i j) ⊔ a = ⨅ (i : ι), ⨅ (j : κ i), f i j ⊔ a

Tactic:
@iSup₂_inf_eq αᵒᵈ _ _ _ _ _

Premises used: iInf, iSup₂_inf_eq, OrderDual
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : Coframe α
f : (i : ι) → κ i → α
a : α
⊢ a ⊔ ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a ⊔ f i j

Tactic:
@inf_iSup₂_eq αᵒᵈ _ _ _ _ _

Premises used: iInf, inf_iSup₂_eq, OrderDual
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : Coframe α
a : α
f : ι → α
x : α
⊢ (⨆ (x : ι), f x) \ a ≤ x ↔ ⨆ (x : ι), f x \ a ≤ x

Tactic:
simp
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : Coframe α
a : α
f : ι → α
x : α
⊢ a \ ⨅ (x : ι), f x ≤ x ↔ ⨆ (x : ι), a \ f x ≤ x

Tactic:
simp [iInf_sup_eq]

Premises used: iInf_sup_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
⊢ Eq.{u + 1} (α := α) ((⨅ (i : ι), f i) ⊔ ⨅ (i : ι'), g i) (⨅ (i : ι × ι'), f i.1 ⊔ g i.2)

Tactic:
@iSup_inf_iSup αᵒᵈ _ _ _ _ _

Premises used: iInf, OrderDual, iSup_inf_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ Eq.{u + 1} (α := α) ((⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j) (⨅ p ∈ s ×ˢ t, f p.1 ⊔ g p.2)

Tactic:
@biSup_inf_biSup αᵒᵈ _ _ _ _ _ _ _

Premises used: iInf, biSup_inf_biSup, OrderDual
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
s t : Set α
⊢ sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, p.1 ⊔ p.2

Tactic:
@sSup_inf_sSup αᵒᵈ _ _ _

Premises used: iInf, sSup_inf_sSup, Set.Mem, OrderDual
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsCodirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ Eq.{u + 1} (α := α) (⨅ (i : ι), f i ⊔ g i) ((⨅ (i : ι), f i) ⊔ ⨅ (i : ι), g i)

Tactic:
@iSup_inf_of_antitone αᵒᵈ _ _ _ _ _ _ hf.dual_right hg.dual_right

Premises used: iInf, Monotone.dual_right, OrderDual, iSup_inf_of_antitone
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Antitone f
hg : Antitone g
⊢ Eq.{u + 1} (α := α) (⨅ (i : ι), f i ⊔ g i) ((⨅ (i : ι), f i) ⊔ ⨅ (i : ι), g i)

Tactic:
@iSup_inf_of_monotone αᵒᵈ _ _ _ _ _ _ hf.dual_right hg.dual_right

Premises used: iInf, Antitone.dual_right, OrderDual, iSup_inf_of_monotone
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
a b : α
⊢ a \ b = sInf {w : α | a ≤ b ⊔ w}

Tactic:
(isLeast_sdiff a b).isGLB.sInf_eq.symm

Premises used: IsGLB.sInf_eq, isLeast_sdiff, setOf, IsLeast.isGLB, Eq.symm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
a : α
⊢ ￢a = sInf {w : α | Codisjoint a w}

Tactic:
(isLeast_hnot a).isGLB.sInf_eq.symm

Premises used: IsGLB.sInf_eq, setOf, IsLeast.isGLB, isLeast_hnot, Eq.symm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Coframe α
a b c : α
⊢ a ≤ b \ c ↔ ∀ (d : α), b ≤ c ⊔ d → a ≤ d

Tactic:
simp [sdiff_eq_sInf]

Premises used: sdiff_eq_sInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Coframe α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ b ⊓ c
rw₁ : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ sInf {b, c}
rw₂ : LE.le (α := α) (sInf {a ⊔ b, a ⊔ c}) (⨅ (b_2 : α), ⨅ (_ : Membership.mem (γ := Set α) {b, c} b_2), a ⊔ b_2)
rw₃ : sInf {a ⊔ b, a ⊔ c} ≤ sInf (max a '' {b, c})
rw₄ rw₅ : LE.le (α := α) (sInf {a ⊔ b, a ⊔ c}) (sInf {a ⊔ b, a ⊔ c})
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]

Premises used: sInf_pair, Set.image_pair, sInf_image, sup_sInf_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompletelyDistribLattice α
inst_1 : CompletelyDistribLattice β
ι_1 : Type (max u v)
κ_1 : ι_1 → Type (max u v)
f : (a : ι_1) → κ_1 a → α × β
fst : Eq.{u + 1} (α := α) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b).1 (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a)).1
snd : Eq.{v + 1} (α := β) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b).2 (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a)).2
⊢ Eq (α := α × β) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b) (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a))

Tactic:
ext
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompletelyDistribLattice α
inst_1 : CompletelyDistribLattice β
ι_1 : Type (max u v)
κ_1 : ι_1 → Type (max u v)
f : (a : ι_1) → κ_1 a → α × β
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b).1 (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a)).1

Tactic:
simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]

Premises used: Prod.fst_iSup, iInf_iSup_eq, Prod.fst_iInf, Prod.snd_iSup, Prod.snd_iInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompletelyDistribLattice α
inst_1 : CompletelyDistribLattice β
ι_1 : Type (max u v)
κ_1 : ι_1 → Type (max u v)
f : (a : ι_1) → κ_1 a → α × β
⊢ Eq.{v + 1} (α := β) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b).2 (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a)).2

Tactic:
simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]

Premises used: Prod.fst_iSup, iInf_iSup_eq, Prod.fst_iInf, Prod.snd_iSup, Prod.snd_iInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι_1 : Sort w
κ : ι_1 → Sort w'
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → CompletelyDistribLattice (π i)
ι_2 : Type (max u_1 u_2)
κ_1 : ι_2 → Type (max u_1 u_2)
f : (a : ι_2) → κ_1 a → (i : ι) → π i
h :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := π i) ((⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) i)
      ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) i)
⊢ Eq (α := (i : ι) → π i) (⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) (⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a))

Tactic:
ext i
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι_1 : Sort w
κ : ι_1 → Sort w'
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → CompletelyDistribLattice (π i)
ι_2 : Type (max u_1 u_2)
κ_1 : ι_2 → Type (max u_1 u_2)
f : (a : ι_2) → κ_1 a → (i : ι) → π i
i : ι
⊢ Eq.{u_2 + 1} (α := π i) ((⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) i)
    ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) i)

Tactic:
simp only [iInf_apply, iSup_apply, iInf_iSup_eq]

Premises used: iInf_apply, iInf_iSup_eq, iSup_apply
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
f : ι → α
⊢ (iInf f)ᶜ = ⨆ (i : ι), (f i)ᶜ

Tactic:
le_antisymm
    (compl_le_of_compl_le <| le_iInf fun i => compl_le_of_compl_le <|
      le_iSup (Compl.compl ∘ f) i)
    (iSup_le fun _ => compl_le_compl <| iInf_le _ _)

Premises used: compl_le_of_compl_le, Compl.compl, compl_le_compl, le_iInf, Function.comp, le_iSup, le_antisymm, iSup_le, iInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
f : ι → α
⊢ (iSup f)ᶜᶜ = (⨅ (i : ι), (f i)ᶜ)ᶜ

Tactic:
simp [compl_iInf]

Premises used: compl_iInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
⊢ (sInf s)ᶜ = ⨆ i ∈ s, iᶜ

Tactic:
simp only [sInf_eq_iInf, compl_iInf]

Premises used: compl_iInf, sInf_eq_iInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
⊢ (sSup s)ᶜ = ⨅ i ∈ s, iᶜ

Tactic:
simp only [sSup_eq_iSup, compl_iSup]

Premises used: compl_iSup, sSup_eq_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
⊢ (sInf s)ᶜ = sSup (compl '' s)

Tactic:
compl_sInf.trans sSup_image.symm

Premises used: compl_sInf, sSup_image, Eq.symm, Eq.trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
⊢ (sSup s)ᶜ = sInf (compl '' s)

Tactic:
compl_sSup.trans sInf_image.symm

Premises used: compl_sSup, sInf_image, Eq.symm, Eq.trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
f g : ι → α
simp_rw :
  LE.le.{u} (α := α) (⨆ (i : ι), f i) (⨆ (x : ι), g x ⊔ f x ∆ g x) ∧
    LE.le.{u} (α := α) (⨆ (i : ι), g i) (⨆ (x : ι), f x ⊔ f x ∆ g x)
⊢ LE.le.{u} (α := α) ((⨆ (i : ι), f i) ∆ ⨆ (i : ι), g i) (⨆ (i : ι), f i ∆ g i)

Tactic:
simp_rw [symmDiff_le_iff, ← iSup_sup_eq]

Premises used: iSup_sup_eq, symmDiff_le_iff
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
f g : ι → α
⊢ LE.le.{u} (α := α) (⨆ (i : ι), f i) (⨆ (x : ι), g x ⊔ f x ∆ g x) ∧
    LE.le.{u} (α := α) (⨆ (i : ι), g i) (⨆ (x : ι), f x ⊔ f x ∆ g x)

Tactic:
⟨iSup_mono fun i ↦ sup_comm (g i) _ ▸ le_symmDiff_sup_right ..,
    iSup_mono fun i ↦ sup_comm (f i) _ ▸ symmDiff_comm (f i) _ ▸ le_symmDiff_sup_right ..⟩

Premises used: symmDiff_comm, Eq.rec, sup_comm, And.intro, le_symmDiff_sup_right, Eq.symm, symmDiff, iSup_mono
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
f g : ι → α
⊢ LE.le.{u} (α := α) (⨆ (i : ι), f i) (⨆ (x : ι), g x ⊔ f x ∆ g x) ∧
    LE.le.{u} (α := α) (⨆ (i : ι), g i) (⨆ (x : ι), f x ⊔ f x ∆ g x)

Tactic:
exact ⟨iSup_mono fun i ↦ sup_comm (g i) _ ▸ le_symmDiff_sup_right ..,
    iSup_mono fun i ↦ sup_comm (f i) _ ▸ symmDiff_comm (f i) _ ▸ le_symmDiff_sup_right ..⟩
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
f : ι → α
inst_1 : Nonempty ι
a : α
⊢ (⨆ (i : ι), f i) ∆ a ≤ ⨆ (i : ι), f i ∆ a

Tactic:
simpa [iSup_const] using iSup_symmDiff_iSup_le (g := fun _ : ι ↦ a)

Premises used: iSup_const, iSup_symmDiff_iSup_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
f : ι → α
inst_1 : Nonempty ι
a : α
⊢ a ∆ ⨆ (i : ι), f i ≤ ⨆ (i : ι), a ∆ f i

Tactic:
simpa [symmDiff_comm] using iSup_symmDiff_le (a := a)

Premises used: symmDiff_comm, iSup_symmDiff_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
rw : (⨆ (a : (↑s : Type u)), (↑a : α)) ∆ a ≤ ⨆ (a_1 : (↑s : Type u)), (↑a_1 : α) ∆ a
⊢ sSup s ∆ a ≤ sSup ((fun (x : α) ↦ x ∆ a) '' s)

Tactic:
rw [sSup_image', sSup_eq_iSup']

Premises used: sSup_image', sSup_eq_iSup'
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ Nonempty.{u + 1} (↑s : Type u)

Tactic:
have : Nonempty s := Set.nonempty_coe_sort.mpr hs
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
this : Nonempty.{u + 1} (↑s : Type u)
⊢ (⨆ (a : (↑s : Type u)), (↑a : α)) ∆ a ≤ ⨆ (a_1 : (↑s : Type u)), (↑a_1 : α) ∆ a

Tactic:
iSup_symmDiff_le

Premises used: iSup_symmDiff_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
this : Nonempty.{u + 1} (↑s : Type u)
⊢ (⨆ (a : (↑s : Type u)), (↑a : α)) ∆ a ≤ ⨆ (a_1 : (↑s : Type u)), (↑a_1 : α) ∆ a

Tactic:
exact iSup_symmDiff_le

Premises used: iSup_symmDiff_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ a ∆ sSup s ≤ sSup ((fun (x : α) ↦ a ∆ x) '' s)

Tactic:
simpa [symmDiff_comm] using sSup_symmDiff_le (a := a) hs

Premises used: symmDiff_comm, sSup_symmDiff_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
rw : sSup s ∆ sSup t ≤ ⨆ a ∈ s, ⨆ b ∈ t, a ∆ b
⊢ sSup s ∆ sSup t ≤ sSup (image2 (fun (x1 x2 : α) ↦ x1 ∆ x2) s t)

Tactic:
rw [sSup_image2]

Premises used: sSup_image2
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, a ∆ sSup t

Tactic:
simpa [sSup_image] using sSup_symmDiff_le hs

Premises used: sSup_symmDiff_le, sSup_image
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
a : α
h : a ∈ s
⊢ a ∆ sSup t ≤ ⨆ b ∈ t, a ∆ b

Tactic:
simpa [sSup_image] using symmDiff_sSup_le ht

Premises used: sSup_image, symmDiff_sSup_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
_ : sSup s ∆ sSup t ≤ ⨆ a ∈ s, a ∆ sSup t
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, ⨆ b ∈ t, a ∆ b

Tactic:
calc
  _ ≤ ⨆ a ∈ s, a ∆ sSup t := by simpa [sSup_image] using sSup_symmDiff_le hs
  _ ≤ _ := iSup_mono fun a ↦ iSup_mono fun _ ↦ by simpa [sSup_image] using symmDiff_sSup_le ht

Premises used: SupSet.sSup, iSup_mono
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
p : ι → Prop
f g : (i : ι) → p i → α
⊢ LE.le.{u} (α := α) ((⨆ (i : ι), ⨆ (h : p i), f i h) ∆ ⨆ (i : ι), ⨆ (h : p i), g i h)
    (⨆ (i : ι), ⨆ (h : p i), f i h ∆ g i h)

Tactic:
le_trans iSup_symmDiff_iSup_le <| iSup_mono fun _ ↦ iSup_symmDiff_iSup_le

Premises used: iSup_symmDiff_iSup_le, iSup_mono, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι_1 : Sort w
κ : ι_1 → Sort w'
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι_2 : Type (max u_1 u_2)
κ_1 : ι_2 → Type (max u_1 u_2)
f : (a : ι_2) → κ_1 a → (i : ι) → π i
h :
  ∀ (x : ι),
    Eq.{u_2 + 1} (α := π x) ((⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) x)
      ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) x)
⊢ Eq (α := (i : ι) → π i) (⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) (⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a))

Tactic:
ext
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι_1 : Sort w
κ : ι_1 → Sort w'
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι_2 : Type (max u_1 u_2)
κ_1 : ι_2 → Type (max u_1 u_2)
f : (a : ι_2) → κ_1 a → (i : ι) → π i
x : ι
h h₁ :
  Eq.{u_2 + 1} (α := π x) ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) x)
    ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) x)
⊢ Eq.{u_2 + 1} (α := π x) ((⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) x)
    ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) x)

Tactic:
rw [iInf_iSup_eq]

Premises used: iInf_iSup_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
ι_1 : Type
κ_1 : ι_1 → Type
f : (a : ι_1) → κ_1 a → Prop
⊢ Eq (α := Prop) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b) (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a))

Tactic:
simp [Classical.skolem]

Premises used: Classical.skolem
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Frame.MinimalAxioms β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
rw : ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [← le, ← sSup_image, map_inf, map_sSup s, minAx.inf_iSup₂_eq]

Premises used: Order.Frame.MinimalAxioms.inf_iSup₂_eq, sSup_image
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Frame.MinimalAxioms β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
simp_rw : ⨆ i ∈ s, f (a ⊓ i) ≤ f (sSup (min a '' s))
⊢ ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))

Tactic:
simp_rw [← map_inf]
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Frame.MinimalAxioms β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
⊢ ⨆ i ∈ s, f (a ⊓ i) ≤ f (sSup (min a '' s))

Tactic:
((map_sSup _).trans iSup_image).ge

Premises used: Eq.ge, iSup_image, Eq.trans