awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
⊢ eq.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ eq.Compares b a

Tactic:
eq_comm

Premises used: eq_comm, Ordering.Compares, OrderDual
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
⊢ gt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ gt.Compares b a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Ordering.Compares
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
⊢ lt.Compares (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ lt.Compares b a

Tactic:
exacts [Iff.rfl, eq_comm, Iff.rfl]

Premises used: Iff.rfl, eq_comm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), (cmp a b).Compares a b
inr : ∀ (h : a = b), (cmp a b).Compares a b
inr₁ : ∀ (h : b < a), (cmp a b).Compares a b
⊢ (cmp a b).Compares a b

Tactic:
obtain h | h | h := lt_trichotomy a b

Premises used: lt_trichotomy
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ (cmp a b).Compares a b

Tactic:
simp [cmp, cmpUsing, h, h.not_gt]

Premises used: cmpUsing, cmp, LT.lt.not_gt
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a = b
⊢ (cmp a b).Compares a b

Tactic:
simp [cmp, cmpUsing, h, h.not_gt]

Premises used: Eq.not_gt, cmpUsing, cmp
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b < a
⊢ (cmp a b).Compares a b

Tactic:
simp [cmp, cmpUsing, h, h.not_gt]

Premises used: cmpUsing, cmp, LT.lt.not_gt
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
o : Ordering
h : o.Compares a b
⊢ cmp a b = o

Tactic:
(cmp_compares a b).inj h

Premises used: Ordering.Compares.inj, cmp_compares
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
pos :
  ∀ (h : a < b),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
neg :
  ∀ (h : ¬a < b),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq

Tactic:
by_cases h : a < b
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : a < b
pos :
  ∀ (h₂ : b < a),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
neg :
  ∀ (h₂ : ¬b < a),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq

Tactic:
by_cases h₂ : b < a
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : ¬a < b
pos :
  ∀ (h₂ : b < a),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
neg :
  ∀ (h₂ : ¬b < a),
    (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
      if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq

Tactic:
by_cases h₂ : b < a
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : a < b
h₂ : b < a
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq

Tactic:
simp_all [lt_asymm]

Premises used: lt_asymm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : a < b
h₂ : ¬b < a
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq

Tactic:
simp_all [lt_asymm]

Premises used: lt_asymm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : ¬a < b
h₂ : b < a
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq

Tactic:
simp_all [lt_asymm]

Premises used: lt_asymm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a b : α
h : ¬a < b
h₂ : ¬b < a
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then lt else if (fun (x1 x2 : α) ↦ x1 < x2) b a then gt else eq).swap =
    if (fun (x1 x2 : α) ↦ x1 < x2) b a then lt else if (fun (x1 x2 : α) ↦ x1 < x2) a b then gt else eq

Tactic:
simp_all [lt_asymm]

Premises used: lt_asymm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
x y : α
⊢ cmpLE (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) y : αᵒᵈ) = cmpLE y x

Tactic:
rfl

Premises used: cmpLE, rfl
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LE α
inst_1 : DecidableLE α
x y : αᵒᵈ
⊢ cmpLE (α := α) ((ofDual : (a : αᵒᵈ) → α) x : α) ((ofDual : (a : αᵒᵈ) → α) y : α) = cmpLE y x

Tactic:
rfl

Premises used: cmpLE, rfl
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
inst_1 : DecidableLT α
x y : α
⊢ cmp (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) y : αᵒᵈ) = cmp y x

Tactic:
rfl

Premises used: cmpUsing, cmp, OrderDual, rfl
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LT α
inst_1 : DecidableLT α
x y : αᵒᵈ
⊢ cmp (α := α) ((ofDual : (a : αᵒᵈ) → α) x : α) ((ofDual : (a : αᵒᵈ) → α) y : α) = cmp y x

Tactic:
rfl

Premises used: cmpUsing, cmp, OrderDual, rfl
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
⊢ cmp x y = lt ↔ x < y

Tactic:
Ordering.Compares.eq_lt (cmp_compares x y)

Premises used: Ordering.Compares.eq_lt, cmp_compares
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
⊢ cmp x y = eq ↔ x = y

Tactic:
Ordering.Compares.eq_eq (cmp_compares x y)

Premises used: cmp_compares, Ordering.Compares.eq_eq
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
⊢ cmp x y = gt ↔ y < x

Tactic:
Ordering.Compares.eq_gt (cmp_compares x y)

Premises used: cmp_compares, Ordering.Compares.eq_gt
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x : α
rw rw₁ : x = x
⊢ cmp x x = eq

Tactic:
rw [cmp_eq_eq_iff]

Premises used: cmp_eq_eq_iff
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rwa : cmp y x = (cmp x' y').swap
rwa₁ : (cmp x y).swap = (cmp x' y').swap
rwa₂ rwa₃ rwa₄ rwa₅ : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'

Tactic:
rwa [← cmp_swap x', ← cmp_swap, swap_inj]

Premises used: cmp_swap, Ordering.swap_inj
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
rwa : cmp x y = (cmp y' x').swap
rwa₁ : (cmp y x).swap = (cmp y' x').swap
rwa₂ rwa₃ rwa₄ rwa₅ : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'

Tactic:
rwa [← cmp_swap y', ← cmp_swap, swap_inj]

Premises used: cmp_swap, Ordering.swap_inj
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rw : cmp x y = lt ↔ x' < y'
rw₁ : cmp x y = lt ↔ cmp x' y' = lt
rw₂ rw₃ : cmp x' y' = lt ↔ cmp x' y' = lt
⊢ x < y ↔ x' < y'

Tactic:
rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]

Premises used: cmp_eq_lt_iff
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rw : ¬y < x ↔ ¬y' < x'
⊢ x ≤ y ↔ x' ≤ y'

Tactic:
rw [← not_lt, ← not_lt]

Premises used: not_lt
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
h₁ : y < x ↔ y' < x'
⊢ ¬y < x ↔ ¬y' < x'

Tactic:
apply not_congr

Premises used: not_congr
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
h₁ : cmp y x = cmp y' x'
⊢ y < x ↔ y' < x'

Tactic:
apply lt_iff_lt_of_cmp_eq_cmp

Premises used: lt_iff_lt_of_cmp_eq_cmp
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h h₁ h₂ h₃ h₄ : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'

Tactic:
rwa [cmp_eq_cmp_symm]

Premises used: cmp_eq_cmp_symm
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
β : Type u_3
inst_1 : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
rw : x ≤ y ∧ y ≤ x ↔ x' = y'
rw₁ : x ≤ y ∧ y ≤ x ↔ x' ≤ y' ∧ y' ≤ x'
rw₂ : x' ≤ y' ∧ y ≤ x ↔ x' ≤ y' ∧ y' ≤ x'
rw₃ rw₄ : x' ≤ y' ∧ y' ≤ x' ↔ x' ≤ y' ∧ y' ≤ x'
⊢ x = y ↔ x' = y'

Tactic:
rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
      le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]

Premises used: cmp_eq_cmp_symm, le_iff_le_of_cmp_eq_cmp, le_antisymm_iff, Iff.mp
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x < y
⊢ cmp x y = Ordering.lt

Tactic:
(cmp_eq_lt_iff _ _).2 h

Premises used: Iff.mpr, cmp_eq_lt_iff
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x < y
⊢ cmp y x = gt

Tactic:
(cmp_eq_gt_iff _ _).2 h

Premises used: Iff.mpr, cmp_eq_gt_iff
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x = y
⊢ cmp x y = eq

Tactic:
(cmp_eq_eq_iff _ _).2 h

Premises used: Iff.mpr, cmp_eq_eq_iff
-- Module: Mathlib.Order.Compare
Goal:
α : Type u_1
inst : LinearOrder α
x y : α
h : x = y
⊢ cmp y x = eq

Tactic:
h.symm.cmp_eq_eq

Premises used: Eq.cmp_eq_eq, Eq.symm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u_1
inst : Order.Frame α
s : Set α
a : α
⊢ a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

Tactic:
gc_inf_himp.l_sSup

Premises used: GaloisConnection.l_sSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u_1
inst : Order.Coframe α
s : Set α
a : α
⊢ a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b

Tactic:
gc_sdiff_sup.u_sInf

Premises used: GaloisConnection.u_sInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : CompleteLattice α
f : (a : ι) → κ a → α
⊢ LE.le.{u} (α := α) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)) (⨅ (a : ι), ⨆ (b : κ a), f a b)

Tactic:
iSup_le fun _ => le_iInf fun a => le_trans (iInf_le _ a) (le_iSup _ _)

Premises used: le_iInf, le_iSup, iSup_le, iInf_le, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : CompleteLattice α
f : (a : ι) → κ a → α
⊢ LE.le.{u} (α := α) (⨆ (a : ι), ⨅ (b : κ a), f a b) (⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a))

Tactic:
le_iInf_iSup (α := αᵒᵈ)

Premises used: iInf, iSup, le_iInf_iSup, OrderDual
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
minAx : MinimalAxioms α
s : Set α
a : α
⊢ a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b

Tactic:
(minAx.inf_sSup_le_iSup_inf _ _).antisymm iSup_inf_le_inf_sSup

Premises used: LE.le.antisymm, iSup_inf_le_inf_sSup, Order.Frame.MinimalAxioms.inf_sSup_le_iSup_inf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
minAx : MinimalAxioms α
s : Set α
b : α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

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

Premises used: inf_comm, Order.Frame.MinimalAxioms.inf_sSup_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
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, Order.Frame.MinimalAxioms.sSup_inf_eq, iSup_range
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
a : α
f : ι → α
⊢ a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i

Tactic:
simpa only [inf_comm] using minAx.iSup_inf_eq f a

Premises used: Order.Frame.MinimalAxioms.iSup_inf_eq, inf_comm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
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: Order.Frame.MinimalAxioms.inf_iSup_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
x b c : α
h : x ≤ sSup {c_1 : α | c_1 ⊓ b ≤ c}
⊢ sSup {c_1 : α | c_1 ⊓ b ≤ c} ⊓ b ≤ c

Tactic:
simp [minAx.sSup_inf_eq]

Premises used: Order.Frame.MinimalAxioms.sSup_inf_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
minAx : MinimalAxioms α
s : Set α
a : α
⊢ a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b

Tactic:
sup_sInf_le_iInf_sup.antisymm (minAx.iInf_sup_le_sup_sInf _ _)

Premises used: LE.le.antisymm, sup_sInf_le_iInf_sup, Order.Coframe.MinimalAxioms.iInf_sup_le_sup_sInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
minAx : MinimalAxioms α
s : Set α
b : α
⊢ sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b

Tactic:
simpa only [sup_comm] using @sup_sInf_eq α _ s b

Premises used: sup_comm, Order.Coframe.MinimalAxioms.sup_sInf_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
rw : sInf (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 [iInf, sInf_sup_eq, iInf_range]

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

Tactic:
simpa only [sup_comm] using minAx.iInf_sup_eq f a

Premises used: Order.Coframe.MinimalAxioms.iInf_sup_eq, sup_comm
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
a : α
⊢ a ⊔ ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (i : ι), ⨅ (j : κ i), a ⊔ f i j

Tactic:
simp only [sup_iInf_eq]

Premises used: Order.Coframe.MinimalAxioms.sup_iInf_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a b x : α
h : sInf {c : α | a ≤ b ⊔ c} ≤ x
⊢ a ≤ b ⊔ sInf {c : α | a ≤ b ⊔ c}

Tactic:
simp [minAx.sup_sInf_eq]

Premises used: Order.Coframe.MinimalAxioms.sup_sInf_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ let x := minAx.toCompleteLattice;
  Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))

Tactic:
le_antisymm ?_ le_iInf_iSup

Premises used: le_antisymm, le_iInf_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
refine : LE.le.{u} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))
⊢ let x := minAx.toCompleteLattice;
  Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))

Tactic:
refine le_antisymm ?_ le_iInf_iSup

Premises used: le_antisymm, le_iInf_iSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
simp_rw :
  Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
    (⨅ (i : Set α),
      ⨅ (_ : Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) i), ⨆ (b : (↑i : Type u)), (↑b : α))
simp_rw₁ : Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨅ (i : ι), ⨆ (b : (↑(range (f i)) : Type u)), (↑b : α))
simp_rw₂ : Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨅ (i : ι), ⨆ i_1 ∈ range (f i), i_1)
⊢ Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
    (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), ⨆ (b : (↑(↑a : Set α) : Type u)), (↑b : α))

Tactic:
simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]

Premises used: iSup_subtype, iInf_range, iInf_subtype, iSup_range
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ Eq.{u + 1} (α := α)
    (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), ⨆ (b : (↑(↑a : Set α) : Type u)), (↑b : α))
    (⨆ (g : (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)) → (↑(↑a : Set α) : Type u)),
      ⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))

Tactic:
minAx.iInf_iSup_eq _

Premises used: CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)) → (↑(↑a : Set α) : Type u)
⊢ LE.le.{u} (α := α) (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))
    (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))

Tactic:
le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2

Premises used: le_iSup, Subtype.mk, Exists.intro, Classical.choose, Set.range, rfl, Subtype.property, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)) → (↑(↑a : Set α) : Type u)
refine :
  LE.le.{u} (α := α) (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))
    (⨅ (i : ι),
      f i
        ((fun (a : ι) ↦
            (Classical.choose (p := fun (x : κ a) ↦
                f a x =
                  (↑(g
                        (Subtype.mk (p := fun (x : Set α) ↦
                          Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                          ((fun (x : ι) ↦ range (f x)) a) ⋯)) :
                    α))
                ⋯ :
              κ a))
          i))
⊢ LE.le.{u} (α := α) (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))
    (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))

Tactic:
refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2

Premises used: le_iSup, Subtype.mk, Exists.intro, Classical.choose, Set.range, rfl, Subtype.property, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)) → (↑(↑a : Set α) : Type u)
⊢ LE.le.{u} (α := α) (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))
    (⨅ (i : ι),
      f i
        ((fun (a : ι) ↦
            (Classical.choose (p := fun (x : κ a) ↦
                f a x =
                  (↑(g
                        (Subtype.mk (p := fun (x : Set α) ↦
                          Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                          ((fun (x : ι) ↦ range (f x)) a) ⋯)) :
                    α))
                ⋯ :
              κ a))
          i))

Tactic:
le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_

Premises used: le_iInf, Subtype.val, iInf_le, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)) → (↑(↑a : Set α) : Type u)
refine :
  ∀ (a : ι),
    (↑(g
            (Subtype.mk (p := fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
              (range (f a)) ⋯)) :
        α) ≤
      f a
        ((fun (a : ι) ↦
            (Classical.choose (p := fun (x : κ a) ↦
                f a x =
                  (↑(g
                        (Subtype.mk (p := fun (x : Set α) ↦
                          Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                          ((fun (x : ι) ↦ range (f x)) a) ⋯)) :
                    α))
                ⋯ :
              κ a))
          a)
⊢ LE.le.{u} (α := α) (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))
    (⨅ (i : ι),
      f i
        ((fun (a : ι) ↦
            (Classical.choose (p := fun (x : κ a) ↦
                f a x =
                  (↑(g
                        (Subtype.mk (p := fun (x : Set α) ↦
                          Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                          ((fun (x : ι) ↦ range (f x)) a) ⋯)) :
                    α))
                ⋯ :
              κ a))
          i))

Tactic:
refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_

Premises used: le_iInf, iInf_le, le_trans