awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
    (⨆ (g : (a : κ) → ι), ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ (a : κ), f (g a))

Tactic:
le_antisymm
    (iSup₂_le fun i hi ↦ le_iSup₂_of_le (fun _ ↦ i) hi (le_iInf fun _ ↦ le_rfl))
    (iSup₂_le fun I hI ↦ ?_)

Premises used: iSup₂_le, le_rfl, le_iInf, le_antisymm, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
refine :
  ∀ (I : (a : κ) → ι) (hI : ∀ (a : κ), I a ∈ s a),
    LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
    (⨆ (g : (a : κ) → ι), ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ (a : κ), f (g a))

Tactic:
refine le_antisymm
    (iSup₂_le fun i hi ↦ le_iSup₂_of_le (fun _ ↦ i) hi (le_iInf fun _ ↦ le_rfl))
    (iSup₂_le fun I hI ↦ ?_)

Premises used: iSup₂_le, le_antisymm, le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
pos :
  ∀ (H : ∀ (k : κ), I k = I j), LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
neg :
  ∀ (H : ∃ (k : κ), I k ≠ I j), LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
⊢ LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)

Tactic:
by_cases! H : ∀ k, I k = I j
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
H : ∀ (k : κ), I k = I j
⊢ LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)

Tactic:
le_iSup₂_of_le (I j) (fun k ↦ (H k) ▸ (hI k)) (iInf_le _ _)

Premises used: Eq.rec, le_iSup₂_of_le, iInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
H : ∀ (k : κ), I k = I j
⊢ LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)

Tactic:
exact le_iSup₂_of_le (I j) (fun k ↦ (H k) ▸ (hI k)) (iInf_le _ _)

Premises used: le_iSup₂_of_le, iInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
H : ∃ (k : κ), I k ≠ I j
neg :
  ∀ (k : κ) (hk : I k ≠ I j), LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
⊢ LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)

Tactic:
rcases H with ⟨k, hk⟩
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
k : κ
hk : I k ≠ I j
⊢ ⨅ (l : κ), f (I l) ≤ f (I k) ⊓ f (I j)

Tactic:
le_inf (iInf_le _ _) (iInf_le _ _)

Premises used: le_inf, iInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
k : κ
hk : I k ≠ I j
⊢ f (I k) ⊓ f (I j) = ⊥

Tactic:
(h hk).eq_bot

Premises used: Disjoint.eq_bot
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
k : κ
hk : I k ≠ I j
⊢ LE.le.{u} (α := α) ⊥ (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
k : κ
hk : I k ≠ I j
⊢ LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)

Tactic:
calc ⨅ l, f (I l)
    _ ≤ f (I k) ⊓ f (I j) := le_inf (iInf_le _ _) (iInf_le _ _)
    _ = ⊥ := (h hk).eq_bot
    _ ≤ _ := bot_le

Premises used: le_inf, bot_le, Disjoint.eq_bot
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
suffices : lhs ≤ rhs
⊢ Eq.{u + 1} (α := α_1) (⨅ (a : α), ⨆ (b : β a), g a b) (⨆ (g_1 : (a : α) → β a), ⨅ (a : α), g a (g_1 a))

Tactic:
suffices lhs ≤ rhs from le_antisymm this le_iInf_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ∃ (x : α_1), rhs < x ∧ x < lhs
rcases : ∀ (x : α_1) (hr : rhs < x) (hl : x < lhs), lhs ≤ rhs
⊢ lhs ≤ rhs

Tactic:
rcases h with ⟨x, hr, hl⟩
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α_1
hr : rhs < x
hl : x < lhs
suffices : rhs ≥ x
⊢ lhs ≤ rhs

Tactic:
suffices rhs ≥ x from nomatch not_lt.2 this hr
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α_1
hr : rhs < x
hl : x < lhs
⊢ ∀ (a : α), ∃ (b : β a), x < g a b

Tactic:
have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α_1
hr : rhs < x
hl : x < lhs
this : ∀ (a : α), ∃ (b : β a), x < g a b
choose : ∀ (f : (a : α) → β a) (hf : ∀ (a : α), x < g a (f a)), rhs ≥ x
⊢ rhs ≥ x

Tactic:
choose f hf using this
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α_1
hr : rhs < x
hl : x < lhs
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
⊢ rhs ≥ x

Tactic:
le_trans ?_ (le_iSup _ f)

Premises used: le_iSup, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α_1
hr : rhs < x
hl : x < lhs
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
refine : x ≤ ⨅ (a : α), g a (f a)
⊢ rhs ≥ x

Tactic:
refine le_trans ?_ (le_iSup _ f)

Premises used: le_iSup, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α_1
hr : rhs < x
hl : x < lhs
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
⊢ x ≤ ⨅ (a : α), g a (f a)

Tactic:
le_iInf fun a => le_of_lt (hf a)

Premises used: le_iInf, le_of_lt
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α_1
hr : rhs < x
hl : x < lhs
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
⊢ x ≤ ⨅ (a : α), g a (f a)

Tactic:
exact le_iInf fun a => le_of_lt (hf a)

Premises used: le_iInf, le_of_lt
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ (x : α_1), rhs < x ∧ x < lhs
⊢ lhs ≤ rhs

Tactic:
le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_

Premises used: le_of_not_gt, not_le_of_gt
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ (x : α_1), rhs < x ∧ x < lhs
⊢ rhs < lhs

Tactic:
refine le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_

Premises used: le_of_not_gt, not_le_of_gt
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ (x : α_1), rhs < x ∧ x < lhs
hrl : rhs < lhs
⊢ ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x

Tactic:
simpa only [not_exists, not_and_or, not_or, not_lt] using h

Premises used: not_exists, not_or, not_lt, not_and_or
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ¬∃ (x : α_1), rhs < x ∧ x < lhs
hrl : rhs < lhs
⊢ ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x

Tactic:
replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
⊢ ∀ (a : α), ∃ (b : β a), rhs < g a b

Tactic:
have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
this : ∀ (a : α), ∃ (b : β a), rhs < g a b
choose : ∀ (f : (a : α) → β a) (hf : ∀ (a : α), rhs < g a (f a)), lhs ≤ rhs
⊢ lhs ≤ rhs

Tactic:
choose f hf using this
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
a : α
⊢ ¬g a (f a) ≤ rhs

Tactic:
simpa using hf a
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
⊢ ∀ (a : α), lhs ≤ g a (f a)

Tactic:
have : ∀ a, lhs ≤ g a (f a) := fun a =>
        (h (g a (f a))).resolve_left (by simpa using hf a)
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ rhs

Tactic:
le_trans ?_ (le_iSup _ f)

Premises used: le_iSup, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
refine : lhs ≤ ⨅ (a : α), g a (f a)
⊢ lhs ≤ rhs

Tactic:
refine le_trans ?_ (le_iSup _ f)

Premises used: le_iSup, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ ⨅ (a : α), g a (f a)

Tactic:
le_iInf fun a => this _

Premises used: le_iInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ ⨅ (a : α), g a (f a)

Tactic:
exact le_iInf fun a => this _

Premises used: le_iInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
if : ∀ (h : ∃ (x : α_1), rhs < x ∧ x < lhs), lhs ≤ rhs
if₁ : ∀ (h : ¬∃ (x : α_1), rhs < x ∧ x < lhs), lhs ≤ rhs
if₂ : ∀ (h : ∃ (x : α_1), rhs < x ∧ x < lhs), lhs ≤ rhs
if₃ if₄ : ∀ (h : ¬∃ (x : α_1), rhs < x ∧ x < lhs), lhs ≤ rhs
⊢ lhs ≤ rhs

Tactic:
if h : ∃ x, rhs < x ∧ x < lhs then
      rcases h with ⟨x, hr, hl⟩
      suffices rhs ≥ x from nomatch not_lt.2 this hr
      have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
      choose f hf using this
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => le_of_lt (hf a)
    else
      refine le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_
      replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h
      have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
      choose f hf using this
      have : ∀ a, lhs ≤ g a (f a) := fun a =>
        (h (g a (f a))).resolve_left (by simpa using hf a)
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => this _

Premises used: le_of_not_gt, not_le_of_gt
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
s : Set α
b : α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
simpa only [inf_comm] using @inf_sSup_eq α _ s b

Premises used: inf_sSup_eq, inf_comm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : Frame α
f : ι → α
a : α
rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
rw₁ :
  Eq.{u + 1} (α := α) (⨆ (a_1 : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) a_1), a_1 ⊓ a)
    (⨆ (i : ι), f i ⊓ a)
rw₂ rw₃ : Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ a) (⨆ (i : ι), f i ⊓ a)
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a

Tactic:
rw [iSup, sSup_inf_eq, iSup_range]

Premises used: iSup, iSup_range, sSup_inf_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : Frame α
a : α
f : ι → α
⊢ a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i

Tactic:
simpa only [inf_comm] using iSup_inf_eq f a

Premises used: iSup_inf_eq, inf_comm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : Frame α
f : (i : ι) → κ i → α
a : α
⊢ (⨆ (i : ι), ⨆ (j : κ i), f i j) ⊓ a = ⨆ (i : ι), ⨆ (j : κ i), f i j ⊓ a

Tactic:
simp only [iSup_inf_eq]

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

Tactic:
simp only [inf_iSup_eq]

Premises used: inf_iSup_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
inst : Frame α
a : α
f : ι → α
b : α
⊢ b ≤ a ⇨ ⨅ (x : ι), f x ↔ b ≤ ⨅ (x : ι), a ⇨ f x

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

Tactic:
simp [inf_iSup_eq]

Premises used: inf_iSup_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
simp_rw : Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ ⨆ (j : ι'), g j) (⨆ (i : ι × ι'), f i.1 ⊓ g i.2)
simp_rw₁ : Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (i_1 : ι'), f i ⊓ g i_1) (⨆ (i : ι × ι'), f i.1 ⊓ g i.2)
⊢ Eq.{u + 1} (α := α) ((⨆ (i : ι), f i) ⊓ ⨆ (j : ι'), g j) (⨆ (i : ι × ι'), f i.1 ⊓ g i.2)

Tactic:
simp_rw [iSup_inf_eq, inf_iSup_eq, iSup_prod]

Premises used: iSup_inf_eq, inf_iSup_eq, iSup_prod
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
simp :
  Eq.{u + 1} (α := α)
    (⨆ (i : Prod.{u_1, u_2} (Subtype (Membership.mem s)) (Subtype (Membership.mem t))), f (↑i.1 : ι) ⊓ g (↑i.2 : ι'))
    (⨆ (x : Subtype (Membership.mem (s ×ˢ t))), f (↑x : ι × ι').1 ⊓ g (↑x : ι × ι').2)
⊢ Eq.{u + 1} (α := α) ((⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j) (⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2)

Tactic:
simp only [iSup_subtype', iSup_inf_iSup]

Premises used: iSup_subtype', iSup_inf_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ Eq.{u + 1} (α := α)
    (⨆ (i : Prod.{u_1, u_2} (Subtype (Membership.mem s)) (Subtype (Membership.mem t))), f (↑i.1 : ι) ⊓ g (↑i.2 : ι'))
    (⨆ (x : Subtype (Membership.mem (s ×ˢ t))), f (↑x : ι × ι').1 ⊓ g (↑x : ι × ι').2)

Tactic:
(Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl

Premises used: Function.Surjective.iSup_congr, Equiv.Set.prod, Equiv.surjective, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ Eq.{u + 1} (α := α)
    (⨆ (i : Prod.{u_1, u_2} (Subtype (Membership.mem s)) (Subtype (Membership.mem t))), f (↑i.1 : ι) ⊓ g (↑i.2 : ι'))
    (⨆ (x : Subtype (Membership.mem (s ×ˢ t))), f (↑x : ι × ι').1 ⊓ g (↑x : ι × ι').2)

Tactic:
exact (Equiv.surjective _).iSup_congr (Equiv.Set.prod s t).symm fun x => rfl

Premises used: Function.Surjective.iSup_congr, Equiv.Set.prod, Equiv.surjective, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
s t : Set α
⊢ sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, p.1 ⊓ p.2

Tactic:
simp only [sSup_eq_iSup, biSup_inf_biSup]

Premises used: biSup_inf_biSup, sSup_eq_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
rw : Eq.{u + 1} (α := α) (⨆ i ∈ s ∩ t, f i) (⨆ p ∈ s ×ˢ t, f p.1 ⊓ f p.2)
⊢ Eq.{u + 1} (α := α) (⨆ i ∈ s ∩ t, f i) ((⨆ i ∈ s, f i) ⊓ ⨆ i ∈ t, f i)

Tactic:
rw [biSup_inf_biSup]

Premises used: biSup_inf_biSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
⊢ Eq.{u + 1} (α := α) (⨆ i ∈ s ∩ t, f i) (⨆ p ∈ s ×ˢ t, f p.1 ⊓ f p.2)

Tactic:
le_antisymm
    (iSup₂_le fun i ⟨his, hit⟩ ↦ le_iSup₂_of_le ⟨i, i⟩ ⟨his, hit⟩ (le_inf le_rfl le_rfl))
    (iSup₂_le fun ⟨i, j⟩ ⟨his, hjs⟩ ↦ ?_)

Premises used: iSup₂_le, le_rfl, iSup, _private.0.biSup_inter_of_pairwise_disjoint.match_1, Prod.mk, LE.le, le_inf, Prod.fst, le_antisymm, And.intro, le_iSup₂_of_le, _private.0.biSup_inter_of_pairwise_disjoint.match_3, Prod.snd, Min.min, _private.0.biSup_inter_of_pairwise_disjoint.match_2
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
refine :
  ∀ (x : ι × ι) (i j : ι),
    (i, j) ∈ s ×ˢ t → ∀ (his : (i, j).1 ∈ s) (hjs : (i, j).2 ∈ t), f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
⊢ Eq.{u + 1} (α := α) (⨆ i ∈ s ∩ t, f i) (⨆ p ∈ s ×ˢ t, f p.1 ⊓ f p.2)

Tactic:
refine le_antisymm
    (iSup₂_le fun i ⟨his, hit⟩ ↦ le_iSup₂_of_le ⟨i, i⟩ ⟨his, hit⟩ (le_inf le_rfl le_rfl))
    (iSup₂_le fun ⟨i, j⟩ ⟨his, hjs⟩ ↦ ?_)

Premises used: iSup₂_le, le_antisymm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x : ι × ι
i j : ι
h_1 : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
pos : ∀ (hij : i = j), f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
neg : ∀ (hij : ¬i = j), f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

Tactic:
by_cases hij : i = j
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x : ι × ι
i j : ι
h_1 : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

Tactic:
le_iSup₂_of_le i ⟨his, hij ▸ hjs⟩ inf_le_left

Premises used: Eq.rec, And.intro, inf_le_left, le_iSup₂_of_le, Eq.symm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x : ι × ι
i j : ι
h_1 : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

Tactic:
exact le_iSup₂_of_le i ⟨his, hij ▸ hjs⟩ inf_le_left

Premises used: le_iSup₂_of_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x : ι × ι
i j : ι
h_1 : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : ¬i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

Tactic:
simp [h hij |>.eq_bot]

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

Tactic:
simp only [disjoint_iff, iSup_inf_eq, iSup_eq_bot]

Premises used: disjoint_iff, iSup_inf_eq, iSup_eq_bot