awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
⊢ Function.comp (β := α →o α) (⇑lfp : (a : α →o α) → α) (⇑h : (a : α) → α →o α) a = a

Tactic:
have ha : (lfp ∘ h) a = a := (lfp.comp h).map_lfp
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
ha : Function.comp (β := α →o α) (⇑lfp : (a : α →o α) → α) (⇑h : (a : α) → α →o α) a = a
⊢ Eq (α := α) ((((h : (a : α) → α →o α) a : α →o α) : (a : α) → α) a : α)
    ((((h : (a : α) → α →o α) a : α →o α) : (a : α) → α)
        ((lfp : (a : α →o α) → α) ((h : (a : α) → α →o α) a : α →o α) : α) :
      α)

Tactic:
congr_arg (h a) ha.symm

Premises used: congr_arg, Eq.symm, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
ha : Function.comp (β := α →o α) (⇑lfp : (a : α →o α) → α) (⇑h : (a : α) → α →o α) a = a
⊢ Eq (α := α)
    ((((h : (a : α) → α →o α) a : α →o α) : (a : α) → α)
        ((lfp : (a : α →o α) → α) ((h : (a : α) → α →o α) a : α →o α) : α) :
      α)
    ((lfp : (a : α →o α) → α) ((h : (a : α) → α →o α) a : α →o α) : α)

Tactic:
(h a).map_lfp

Premises used: OrderHom.map_lfp, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
ha : Function.comp (β := α →o α) (⇑lfp : (a : α →o α) → α) (⇑h : (a : α) → α →o α) a = a
⊢ (lfp : (a : α →o α) → α) ((h : (a : α) → α →o α) a : α →o α) = a

Tactic:
ha
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
ha : Function.comp (β := α →o α) (⇑lfp : (a : α →o α) → α) (⇑h : (a : α) → α →o α) a = a
⊢ Eq (α := α) ((h.onDiag : (a : α) → α) ((lfp : (a : α →o α) → α) (comp lfp h) : α) : α)
    ((lfp : (a : α →o α) → α) (comp lfp h) : α)

Tactic:
calc
    h a a = h a (h a).lfp := congr_arg (h a) ha.symm
    _ = (h a).lfp := (h a).map_lfp
    _ = a := ha

Premises used: OrderHom.map_lfp, congr_arg, Eq.symm, DFunLike.coe, OrderHom.lfp
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
⊢ Eq (α := α) ((gfp : (a : α →o α) → α) (comp gfp h) : α) ((gfp : (a : α →o α) → α) h.onDiag : α)

Tactic:
@lfp_lfp αᵒᵈ _ <| (OrderHom.dualIso αᵒᵈ αᵒᵈ).symm.toOrderEmbedding.toOrderHom.comp h.dual

Premises used: OrderIso.toOrderEmbedding, setOf, OrderHom.comp, OrderHom.lfp_lfp, OrderIso.symm, OrderHom.dualIso, OrderDual, OrderEmbedding.toOrderHom, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
⊢ (gfp : (a : α →o α) → α) ((const α : (a : α) → α →o α) x ⊓ f : α →o α) ≤ x

Tactic:
(gfp_le _) fun _ hb => hb.trans inf_le_left

Premises used: OrderHom.gfp_le, inf_le_left, LE.le.trans
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : (f : (a : α) → α) x ≤ x
⊢ (↑(f.prevFixed x hx) : α) ≤ x

Tactic:
f.gfp_const_inf_le x

Premises used: OrderHom.gfp_const_inf_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
⊢ x ≤ (↑(f.nextFixed x hx) : α)

Tactic:
f.dual.prevFixed_le hx

Premises used: setOf, OrderHom.prevFixed_le, OrderDual, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h : x ≤ (↑y : α)
⊢ f.nextFixed x hx ≤ y

Tactic:
Subtype.coe_le_coe.1 <| lfp_le _ <| sup_le h y.2.le

Premises used: Subtype.coe_le_coe, Eq.le, Iff.mp, sup_le, OrderHom.lfp_le, Subtype.property
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : x ≤ (f : (a : α) → α) x
y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
⊢ f.nextFixed x hx ≤ y ↔ x ≤ (↑y : α)

Tactic:
⟨fun h => (f.le_nextFixed hx).trans h, f.nextFixed_le hx⟩

Premises used: OrderHom.nextFixed_le, OrderHom.le_nextFixed, Iff.intro, LE.le.trans
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : (f : (a : α) → α) x ≤ x
y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
⊢ y ≤ f.prevFixed x hx ↔ (↑y : α) ≤ x

Tactic:
f.dual.nextFixed_le_iff hx

Premises used: setOf, OrderHom.nextFixed_le_iff, OrderDual, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x : α
hx : (f : (a : α) → α) x ≤ x
y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
h : (↑y : α) ≤ x
⊢ y ≤ f.prevFixed x hx

Tactic:
(f.le_prevFixed_iff hx).2 h

Premises used: Iff.mpr, OrderHom.le_prevFixed_iff
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
⊢ (↑x : α) ⊔ (↑y : α) ≤ (f : (a : α) → α) ((↑x : α) ⊔ (↑y : α))

Tactic:
calc
    (x ⊔ y : α) = f x ⊔ f y := congr_arg₂ (· ⊔ ·) x.2.symm y.2.symm
    _ ≤ f (x ⊔ y) := f.mono.le_map_sup x y

Premises used: Trans.trans, Monotone.le_map_sup, OrderHom.mono, Max.max, Eq.symm, Subtype.val, Subtype.property, congr_arg₂
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
x y : (↑(fixedPoints (⇑f : (a : α) → α)) : Type u)
⊢ (f : (a : α) → α) ((↑x : α) ⊓ (↑y : α)) ≤ (↑x : α) ⊓ (↑y : α)

Tactic:
f.dual.le_map_sup_fixedPoints x y

Premises used: OrderHom.le_map_sup_fixedPoints, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
A : Set α
hA : A ⊆ fixedPoints (⇑f : (a : α) → α)
⊢ sSup A ≤ (f : (a : α) → α) (sSup A)

Tactic:
sSup_le fun _ hx => hA hx ▸ (f.mono <| le_sSup hx)

Premises used: Eq.rec, OrderHom.mono, le_sSup, sSup_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
A : Set α
hA : A ⊆ fixedPoints (⇑f : (a : α) → α)
⊢ (f : (a : α) → α) (sInf A) ≤ sInf A

Tactic:
le_sInf fun _ hx => hA hx ▸ (f.mono <| sInf_le hx)

Premises used: Eq.rec, OrderHom.mono, sInf_le, le_sInf
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
a : LE.le (α := α) ((lfp : (a : α →o α) → α) f : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)
a₁ : LE.le (α := α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α) ((lfp : (a : α →o α) → α) f : α)
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) f : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
a : Eq (α := α) ((f : (a : α) → α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥) : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)
⊢ LE.le (α := α) ((lfp : (a : α →o α) → α) f : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)

Tactic:
apply lfp_le_fixed

Premises used: OrderHom.lfp_le_fixed
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
⊢ Eq (α := α) ((f : (a : α) → α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥) : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)

Tactic:
Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
      ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom, OmegaCompletePartialOrder.ContinuousHom.mk, Bot.bot, Function.mem_fixedPoints, Iff.mp, Function.IsFixedPt, bot_le, OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
⊢ Eq (α := α) ((f : (a : α) → α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥) : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)

Tactic:
exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
      ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le)

Premises used: OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom, OmegaCompletePartialOrder.ContinuousHom.mk, Bot.bot, Function.mem_fixedPoints, Iff.mp, bot_le, OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
a : ∀ (b : α), (f : (a : α) → α) b ≤ b → ⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ ≤ b
⊢ LE.le (α := α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α) ((lfp : (a : α →o α) → α) f : α)

Tactic:
apply le_lfp

Premises used: OrderHom.le_lfp
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
a : α
h_a : (f : (a : α) → α) a ≤ a
⊢ ⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ ≤ a

Tactic:
ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le

Premises used: OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint, OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom, iSup, OmegaCompletePartialOrder.ContinuousHom.mk, setOf, Bot.bot, Set.range, bot_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
a : α
h_a : (f : (a : α) → α) a ≤ a
⊢ ⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ ≤ a

Tactic:
exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le

Premises used: OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint, OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom, OmegaCompletePartialOrder.ContinuousHom.mk, Bot.bot, bot_le
-- Module: Mathlib.Order.FixedPoints
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h :
  ωScottContinuous (α := αᵒᵈ) (β := αᵒᵈ)
    (⇑((OrderHom.dual : (a : α →o α) → αᵒᵈ →o αᵒᵈ) f : αᵒᵈ →o αᵒᵈ) : (a : αᵒᵈ) → αᵒᵈ)
⊢ Eq (α := α) ((gfp : (a : α →o α) → α) f : α) (⨅ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊤ : α)

Tactic:
lfp_eq_sSup_iterate f.dual h

Premises used: iInf, setOf, fixedPoints.lfp_eq_sSup_iterate, OrderDual, OrderHom.dual, DFunLike.coe
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
b : β
⊢ b ∈ upperBounds (l '' s) ↔ b ∈ u ⁻¹' upperBounds s

Tactic:
simp [upperBounds, gc _ _]

Premises used: upperBounds
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
h : BddAbove (l '' s)
x : β
hx : x ∈ upperBounds (l '' s)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hx : x ∈ u ⁻¹' upperBounds s), u x ∈ upperBounds s
⊢ u x ∈ upperBounds s

Tactic:
rwa [gc.upperBounds_l_image] at hx

Premises used: GaloisConnection.upperBounds_l_image
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ upperBounds (l '' s)
rwa rwa₁ rwa₂ rwa₃ : ∀ (hb : b ∈ u ⁻¹' upperBounds s), u b ∈ upperBounds s
⊢ u b ∈ upperBounds s

Tactic:
rwa [gc.upperBounds_l_image] at hb

Premises used: GaloisConnection.upperBounds_l_image
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
a : α
⊢ IsLeast {b : β | a ≤ u b} (l a)

Tactic:
⟨gc.le_u_l _, fun _ hb => gc.l_le hb⟩

Premises used: GaloisConnection.l_le, GaloisConnection.le_u_l, IsLeast, And.intro
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
a : α
⊢ IsGLB {b : β | a ≤ u b} (l a)

Tactic:
gc.isLeast_l.isGLB

Premises used: IsLeast.isGLB, GaloisConnection.isLeast_l
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
a₁ a₂ : α
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ IsLUB (l '' {a₁, a₂}) (l a₁ ⊔ l a₂)

Tactic:
simp only [image_pair, isLUB_pair]

Premises used: Set.image_pair, isLUB_pair
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
ι : Sort x
inst : CompleteLattice α
inst_1 : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
rw : IsLUB (l '' range f) (l (sSup (range f)))
⊢ IsLUB (range (l ∘ f)) (l (iSup f))

Tactic:
rw [range_comp, ← sSup_range]

Premises used: Set.range_comp, sSup_range
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
ι : Sort x
inst : CompleteLattice α
inst_1 : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))

Tactic:
gc.isLUB_l_image (isLUB_sSup _)

Premises used: GaloisConnection.isLUB_l_image, isLUB_sSup
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
ι : Sort x
inst : CompleteLattice α
inst_1 : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (l '' range f) (l (sSup (range f)))

Tactic:
exact gc.isLUB_l_image (isLUB_sSup _)

Premises used: GaloisConnection.isLUB_l_image, isLUB_sSup
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
ι : Sort x
κ : ι → Sort u_1
inst : CompleteLattice α
inst_1 : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : (i : ι) → κ i → α
⊢ l (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⨆ (i : ι), ⨆ (j : κ i), l (f i j)

Tactic:
simp_rw [gc.l_iSup]

Premises used: GaloisConnection.l_iSup
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : CompleteLattice α
inst_1 : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
⊢ l (sSup s) = ⨆ a ∈ s, l a

Tactic:
simp only [sSup_eq_iSup, gc.l_iSup]

Premises used: GaloisConnection.l_iSup, sSup_eq_iSup
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
dsimp : (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
⊢ (compl ∘ u ∘ compl) a ≤ b ↔ a ≤ (compl ∘ l ∘ compl) b

Tactic:
dsimp
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
rw : (u aᶜ)ᶜ ≤ b ↔ l bᶜ ≤ aᶜ
rw₁ : (u aᶜ)ᶜ ≤ b ↔ bᶜ ≤ u aᶜ
rw₂ rw₃ : bᶜ ≤ u aᶜ ↔ bᶜ ≤ u aᶜ
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ

Tactic:
rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]

Premises used: le_compl_iff_le_compl, compl_le_iff_compl_le
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
⊢ ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b

Tactic:
simp_rw [isLUB_iff_le_iff, mem_upperBounds] at ha₀ hb₀

Premises used: isLUB_iff_le_iff, mem_upperBounds
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
ha₁ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
⊢ ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b

Tactic:
simp_rw [isLUB_iff_le_iff, mem_upperBounds] at ha₀ hb₀

Premises used: isLUB_iff_le_iff, mem_upperBounds
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
simp_rw₁ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
simp_rw₂ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b
simp_rw₃ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, ∀ y ∈ t, y ≤ u₂ x b
simp_rw₄ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, b₀ ≤ u₂ x b
simp_rw₅ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, l x b₀ ≤ b
simp_rw₆ : ∀ (b : γ), a₀ ≤ u₁ b₀ b ↔ ∀ x ∈ s, x ≤ u₁ b₀ b
simp_rw₇ : ∀ (b : γ), True
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]

Premises used: isLUB_iff_le_iff, Set.forall_mem_image2, GaloisConnection.le_iff_le, forall_true_iff, mem_upperBounds
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (α := βᵒᵈ) (l a ∘ (⇑ofDual : (a : βᵒᵈ) → β)) ((⇑toDual : (a : β) → βᵒᵈ) ∘ u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsGLB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
isLUB_image2_of_isLUB_isLUB (β := βᵒᵈ) h₁ h₂ ha₀ hb₀

Premises used: OrderDual, isLUB_image2_of_isLUB_isLUB
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ :
  ∀ (b : β),
    GaloisConnection (α := αᵒᵈ) (swap (φ := fun (x : α) (y : β) ↦ γ) l b ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑toDual : (a : α) → αᵒᵈ) ∘ u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsGLB s a₀
hb₀ : IsLUB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
isLUB_image2_of_isLUB_isLUB (α := αᵒᵈ) h₁ h₂ ha₀ hb₀

Premises used: OrderDual, isLUB_image2_of_isLUB_isLUB
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ :
  ∀ (b : β),
    GaloisConnection (α := αᵒᵈ) (swap (φ := fun (x : α) (y : β) ↦ γ) l b ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑toDual : (a : α) → αᵒᵈ) ∘ u₁ b)
h₂ : ∀ (a : α), GaloisConnection (α := βᵒᵈ) (l a ∘ (⇑ofDual : (a : βᵒᵈ) → β)) ((⇑toDual : (a : β) → βᵒᵈ) ∘ u₂ a)
ha₀ : IsGLB s a₀
hb₀ : IsGLB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
isLUB_image2_of_isLUB_isLUB (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂ ha₀ hb₀

Premises used: OrderDual, isLUB_image2_of_isLUB_isLUB
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
⊢ sSup (image2 l s t) = l (sSup s) (sSup t)

Tactic:
(isLUB_image2_of_isLUB_isLUB h₁ h₂ (isLUB_sSup _) (isLUB_sSup _)).sSup_eq

Premises used: IsLUB.sSup_eq, isLUB_sSup, isLUB_image2_of_isLUB_isLUB
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (α := βᵒᵈ) (l a ∘ (⇑ofDual : (a : βᵒᵈ) → β)) ((⇑toDual : (a : β) → βᵒᵈ) ∘ u₂ a)
⊢ sSup (image2 l s t) = l (sSup s) (sInf t)

Tactic:
sSup_image2_eq_sSup_sSup (β := βᵒᵈ) h₁ h₂

Premises used: sSup_image2_eq_sSup_sSup, OrderDual
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ :
  ∀ (b : β),
    GaloisConnection (α := αᵒᵈ) (swap (φ := fun (x : α) (y : β) ↦ γ) l b ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑toDual : (a : α) → αᵒᵈ) ∘ u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
⊢ sSup (image2 l s t) = l (sInf s) (sSup t)

Tactic:
sSup_image2_eq_sSup_sSup (α := αᵒᵈ) h₁ h₂

Premises used: sSup_image2_eq_sSup_sSup, OrderDual
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : CompleteLattice α
inst_1 : CompleteLattice β
inst_2 : CompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ :
  ∀ (b : β),
    GaloisConnection (α := αᵒᵈ) (swap (φ := fun (x : α) (y : β) ↦ γ) l b ∘ (⇑ofDual : (a : αᵒᵈ) → α))
      ((⇑toDual : (a : α) → αᵒᵈ) ∘ u₁ b)
h₂ : ∀ (a : α), GaloisConnection (α := βᵒᵈ) (l a ∘ (⇑ofDual : (a : βᵒᵈ) → β)) ((⇑toDual : (a : β) → βᵒᵈ) ∘ u₂ a)
⊢ sSup (image2 l s t) = l (sInf s) (sInf t)

Tactic:
sSup_image2_eq_sSup_sSup (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂

Premises used: sSup_image2_eq_sSup_sSup, OrderDual
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ GaloisConnection.{u, v} (α := α) (β := β) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)

Tactic:
fun _ _ => e.le_symm_apply.symm

Premises used: OrderIso.le_symm_apply, Iff.symm, GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
s : Set α
⊢ BddAbove.{v} (α := β) ((⇑e : (a : α) → β) '' s) ↔ BddAbove s

Tactic:
e.to_galoisConnection.bddAbove_l_image

Premises used: OrderIso.to_galoisConnection, GaloisConnection.bddAbove_l_image
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
s : Set β
rw : BddAbove.{v} (α := β) (image.{u, v} (α := α) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) ⁻¹' s)) ↔ BddAbove s
rw₁ rw₂ : BddAbove s ↔ BddAbove s
⊢ BddAbove.{u} (α := α) ((⇑e : (a : α) → β) ⁻¹' s) ↔ BddAbove s

Tactic:
rw [← e.bddAbove_image, e.image_preimage]

Premises used: OrderIso.bddAbove_image, OrderIso.image_preimage
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
k : ℕ
h : 0 < k
⊢ GaloisConnection (fun (n : ℕ) ↦ n * k) fun (n : ℕ) ↦ n / k

Tactic:
fun _ _ => (le_div_iff_mul_le h).symm

Premises used: Nat.le_div_iff_mul_le, Iff.symm, GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
gi : GaloisInsertion l u
a b : β
⊢ l (u a) ⊔ l (u b) = a ⊔ b

Tactic:
simp only [gi.l_u_eq]

Premises used: GaloisInsertion.l_u_eq
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
f : ι → β
⊢ l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), f i

Tactic:
calc
    l (⨆ i : ι, u (f i)) = ⨆ i : ι, l (u (f i)) := gi.gc.l_iSup
    _ = ⨆ i : ι, f i := congr_arg _ <| funext fun i => gi.l_u_eq (f i)

Premises used: Trans.trans, congr_arg, GaloisConnection.l_iSup, funext, GaloisInsertion.l_u_eq, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨆ (i : ι), ⨆ (hi : p i), u (f i hi)) = ⨆ (i : ι), ⨆ (hi : p i), f i hi

Tactic:
simp only [iSup_subtype', gi.l_iSup_u]

Premises used: iSup_subtype', GaloisInsertion.l_iSup_u
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
rw : l (⨆ a ∈ s, u a) = sSup s
rw₁ : ⨆ i ∈ s, i = sSup s
rw₂ rw₃ : Eq.{v + 1} (α := β) (⨆ i ∈ s, i) (⨆ a ∈ s, a)
⊢ l (sSup (u '' s)) = sSup s

Tactic:
rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]

Premises used: sSup_eq_iSup, GaloisInsertion.l_biSup_u, sSup_image