awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : SemilatticeInf α
inst_1 : SemilatticeInf β
gi : GaloisInsertion l u
a b : β
⊢ l (u (a ⊓ 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)) = l (u (⨅ i : ι, f i)) := congr_arg l gi.gc.u_iInf.symm
    _ = ⨅ i : ι, f i := gi.l_u_eq _

Premises used: Trans.trans, GaloisConnection.u_iInf, congr_arg, Eq.symm, 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 [iInf_subtype', gi.l_iInf_u]

Premises used: iInf_subtype', GaloisInsertion.l_iInf_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) = sInf s
rw₁ : ⨅ i ∈ s, i = sInf s
rw₂ rw₃ : Eq.{v + 1} (α := β) (⨅ i ∈ s, i) (⨅ a ∈ s, a)
⊢ l (sInf (u '' s)) = sInf s

Tactic:
rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]

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

Tactic:
simp [hf]
-- 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 → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
rw : l (⨅ (x : Subtype p), f (↑x : ι) ⋯) = ⨅ (x : Subtype p), l (f (↑x : ι) ⋯)
⊢ l (⨅ (i : ι), ⨅ (hi : p i), f i hi) = ⨅ (i : ι), ⨅ (hi : p i), l (f i hi)

Tactic:
rw [iInf_subtype', iInf_subtype']

Premises used: iInf_subtype'
-- 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 → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (x : Subtype p), f (↑x : ι) ⋯) = ⨅ (x : Subtype p), l (f (↑x : ι) ⋯)

Tactic:
gi.l_iInf_of_u_l_eq_self _ fun _ => hf _ _

Premises used: Subtype.val, GaloisInsertion.l_iInf_of_u_l_eq_self, Subtype.property
-- 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 → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (x : Subtype p), f (↑x : ι) ⋯) = ⨅ (x : Subtype p), l (f (↑x : ι) ⋯)

Tactic:
exact gi.l_iInf_of_u_l_eq_self _ fun _ => hf _ _

Premises used: GaloisInsertion.l_iInf_of_u_l_eq_self
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : Preorder β
gi : GaloisInsertion l u
s : Set β
a : α
hs : IsLUB (u '' s) a
⊢ IsLUB s (l a)

Tactic:
⟨fun x hx => (gi.le_l_u x).trans <| gi.gc.monotone_l <| hs.1 <| mem_image_of_mem _ hx, fun _ hx =>
    gi.gc.l_le <| hs.2 <| gi.gc.monotone_u.mem_upperBounds_image hx⟩

Premises used: GaloisConnection.monotone_u, GaloisConnection.l_le, IsLeast, And.right, And.left, Set.mem_image_of_mem, Monotone.mem_upperBounds_image, And.intro, IsLUB, LE.le.trans, GaloisInsertion.le_l_u, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : Preorder β
gi : GaloisInsertion l u
s : Set β
a : α
hs : IsGLB (u '' s) a
⊢ IsGLB s (l a)

Tactic:
⟨fun _ hx => gi.gc.l_le <| hs.1 <| mem_image_of_mem _ hx, fun x hx =>
    (gi.le_l_u x).trans <| gi.gc.monotone_l <| hs.2 <| gi.gc.monotone_u.mem_lowerBounds_image hx⟩

Premises used: GaloisConnection.monotone_u, Monotone.mem_lowerBounds_image, GaloisConnection.l_le, IsGreatest, And.right, And.left, Set.mem_image_of_mem, IsGLB, And.intro, LE.le.trans, GaloisInsertion.le_l_u, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
simp : ∀ (a b : β), l (u a ⊓ u b) ≤ a
⊢ ∀ (a b : β), gi.choice (u a ⊓ u b) ⋯ ≤ a

Tactic:
simp only [gi.choice_eq]

Premises used: GaloisInsertion.choice_eq
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ a

Tactic:
fun a b => gi.gc.l_le inf_le_left

Premises used: GaloisConnection.l_le, inf_le_left, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ a

Tactic:
exact fun a b => gi.gc.l_le inf_le_left

Premises used: GaloisConnection.l_le, inf_le_left, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
simp : ∀ (a b : β), l (u a ⊓ u b) ≤ b
⊢ ∀ (a b : β), gi.choice (u a ⊓ u b) ⋯ ≤ b

Tactic:
simp only [gi.choice_eq]

Premises used: GaloisInsertion.choice_eq
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ b

Tactic:
fun a b => gi.gc.l_le inf_le_right

Premises used: inf_le_right, GaloisConnection.l_le, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), l (u a ⊓ u b) ≤ b

Tactic:
exact fun a b => gi.gc.l_le inf_le_right

Premises used: inf_le_right, GaloisConnection.l_le, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
simp : ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ l (u b ⊓ u c)
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ gi.choice (u b ⊓ u c) ⋯

Tactic:
simp only [gi.choice_eq]

Premises used: GaloisInsertion.choice_eq
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ l (u b ⊓ u c)

Tactic:
fun a b c hac hbc =>
        (gi.le_l_u a).trans <|
          gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc)

Premises used: GaloisConnection.monotone_u, le_inf, LE.le.trans, GaloisInsertion.le_l_u, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ l (u b ⊓ u c)

Tactic:
exact fun a b c hac hbc =>
        (gi.le_l_u a).trans <|
          gi.gc.monotone_l <| le_inf (gi.gc.monotone_u hac) (gi.gc.monotone_u hbc)

Premises used: GaloisConnection.monotone_u, le_inf, LE.le.trans, GaloisInsertion.le_l_u, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : Preorder α
inst_2 : OrderTop α
gi : GaloisInsertion l u
simp : ∀ (a : β), a ≤ l ⊤
⊢ ∀ (a : β), a ≤ gi.choice ⊤ ⋯

Tactic:
simp only [gi.choice_eq]

Premises used: GaloisInsertion.choice_eq
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : Preorder α
inst_2 : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ l ⊤

Tactic:
fun b => (gi.le_l_u b).trans (gi.gc.monotone_l le_top)

Premises used: le_top, LE.le.trans, GaloisInsertion.le_l_u, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : Preorder α
inst_2 : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ l ⊤

Tactic:
exact fun b => (gi.le_l_u b).trans (gi.gc.monotone_l le_top)

Premises used: le_top, LE.le.trans, GaloisInsertion.le_l_u, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : CompleteLattice α
gi : GaloisInsertion l u
x : Set β
rw : IsGLB x (l (sInf (u '' x)))
⊢ IsGLB x (gi.choice (sInf (u '' x)) ⋯)

Tactic:
rw [gi.choice_eq]

Premises used: GaloisInsertion.choice_eq
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : CompleteLattice α
gi : GaloisInsertion l u
x : Set β
⊢ IsGLB x (l (sInf (u '' x)))

Tactic:
gi.isGLB_of_u_image (isGLB_sInf _)

Premises used: GaloisInsertion.isGLB_of_u_image, isGLB_sInf
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : CompleteLattice α
gi : GaloisInsertion l u
x : Set β
⊢ IsGLB x (l (sInf (u '' x)))

Tactic:
exact gi.isGLB_of_u_image (isGLB_sInf _)

Premises used: GaloisInsertion.isGLB_of_u_image, isGLB_sInf
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
inst : CompleteSemilatticeSup α
⊢ GaloisConnection.{u, u} (α := Set α) sSup Iic

Tactic:
fun _ _ ↦ sSup_le_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.Iic, sSup_le_iff, GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Basic
Goal:
α : Type u
inst : CompleteSemilatticeInf α
⊢ GaloisConnection.{u, u} (α := α) (β := (Set α)ᵒᵈ) ((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ Ici)
    (sInf ∘ (⇑ofDual : (a : (Set α)ᵒᵈ) → Set α))

Tactic:
fun _ _ ↦ le_sInf_iff.symm

Premises used: le_sInf_iff, Set.Ici, Set.Mem, setOf, Set.Subset, Iff.symm, GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
rw : Eq (α := Prop) (∀ (b : α) (a : β), u a ≤ b ↔ a ≤ l b) (∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a)
⊢ Eq (α := Prop) (∀ (a : β) (b : α), u a ≤ b ↔ a ≤ l b) (∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a)

Tactic:
rw [forall_comm]

Premises used: forall_comm
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
⊢ Eq (α := Prop) (∀ (b : α) (a : β), u a ≤ b ↔ a ≤ l b) (∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a)

Tactic:
simp only [Iff.comm]

Premises used: Iff.comm
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
hu : Monotone u
hl : Monotone l
h_u_l : ∀ (a : α), a ≤ u (l a)
h_l_u : ∀ (a : β), l (u a) ≤ a
⊢ GaloisConnection l u

Tactic:
fun _ _ =>
  ⟨fun h => (h_u_l _).trans (hu h), fun h => (hl h).trans (h_l_u _)⟩

Premises used: Iff.intro, LE.le.trans, GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ GaloisConnection (α := βᵒᵈ) (β := αᵒᵈ) ((⇑toDual : (a : α) → αᵒᵈ) ∘ u ∘ (⇑ofDual : (a : βᵒᵈ) → β))
    ((⇑toDual : (a : β) → βᵒᵈ) ∘ l ∘ (⇑ofDual : (a : αᵒᵈ) → α))

Tactic:
fun a b => (gc b a).symm

Premises used: Iff.symm, GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
a : α
b : β
⊢ l a ≤ b ↔ a ≤ u b

Tactic:
gc _ _
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
a : α
b : β
⊢ a ≤ u b → l a ≤ b

Tactic:
(gc _ _).mpr

Premises used: Iff.mpr
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
a : α
⊢ a ≤ u (l a)

Tactic:
gc.le_u <| le_rfl

Premises used: le_rfl, GaloisConnection.le_u
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ Monotone u

Tactic:
fun a _ H => gc.le_u ((gc.l_u_le a).trans H)

Premises used: Monotone, GaloisConnection.le_u, LE.le.trans, GaloisConnection.l_u_le
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ Monotone (l ∘ u)

Tactic:
gc.monotone_l.comp gc.monotone_u

Premises used: GaloisConnection.monotone_u, Monotone.comp, GaloisConnection.monotone_l
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
x y z : α
hxy : x ≤ u (l y)
hyz : y ≤ u (l z)
⊢ x ≤ u (l z)

Tactic:
hxy.trans (gc.monotone_u <| gc.l_le hyz)

Premises used: GaloisConnection.monotone_u, GaloisConnection.l_le, LE.le.trans
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
b : β
⊢ u (l (u b)) = u b

Tactic:
(gc.monotone_u (gc.l_u_le _)).antisymm (gc.le_u_l _)

Premises used: GaloisConnection.monotone_u, LE.le.antisymm, GaloisConnection.le_u_l, GaloisConnection.l_u_le
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ u ∘ l ∘ u = u

Tactic:
funext gc.u_l_u_eq_u

Premises used: funext, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
l' : α → β
u' : β → α
gc' : GaloisConnection l' u'
hl : ∀ (a : α), l a = l' a
b : β
⊢ u b = u' b

Tactic:
le_antisymm (gc'.le_u <| hl (u b) ▸ gc.l_u_le _) (gc.le_u <| (hl (u' b)).symm ▸ gc'.l_u_le _)

Premises used: Eq.rec, GaloisConnection.le_u, le_antisymm, GaloisConnection.l_u_le, Eq.symm
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
a : α
⊢ (∃ (b : β), a = u b) ↔ a = u (l a)

Tactic:
⟨fun ⟨_, hS⟩ => hS.symm ▸ (gc.u_l_u_eq_u _).symm, fun HI => ⟨_, HI⟩⟩

Premises used: Eq.rec, _private.0.GaloisConnection.exists_eq_u.match_1, Iff.intro, Exists.intro, Eq.symm, Eq, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
mp : u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y
mpr : (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y

Tactic:
constructor
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y

Tactic:
(gc x y).symm

Premises used: Iff.symm
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y

Tactic:
exact (gc x y).symm

Premises used: Iff.symm
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z

Tactic:
((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)

Premises used: Iff.mpr, le_rfl, LE.le.antisymm, Iff.mp, GaloisConnection.l_u_le
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z

Tactic:
exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)

Premises used: Iff.mpr, le_rfl, LE.le.antisymm, Iff.mp, GaloisConnection.l_u_le
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : OrderTop α
l : α → β
u : β → α
gc : GaloisConnection l u
x : β
⊢ u x = ⊤ ↔ l ⊤ ≤ x

Tactic:
top_le_iff.symm.trans gc.le_iff_le.symm

Premises used: GaloisConnection.le_iff_le, top_le_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : OrderTop α
inst_3 : OrderTop β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ u ⊤ = ⊤

Tactic:
gc.u_eq_top.2 le_top

Premises used: Iff.mpr, GaloisConnection.u_eq_top, le_top
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : OrderTop α
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ u (l ⊤) = ⊤

Tactic:
gc.u_eq_top.mpr le_rfl

Premises used: Iff.mpr, le_rfl, GaloisConnection.u_eq_top
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
l : α → β
u : β → α
gc : GaloisConnection l u
a : α
b : β
⊢ b < l a ↔ u b < a

Tactic:
lt_iff_lt_of_le_iff_le (gc a b)

Premises used: lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
pα : Preorder α
⊢ GaloisConnection.{u, u} (α := α) id id

Tactic:
fun _ _ =>
  Iff.intro (fun x => x) fun x => x

Premises used: Iff.intro, GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
l1 : α → β
u1 : β → α
l2 : β → γ
u2 : γ → β
gc1 : GaloisConnection l1 u1
gc2 : GaloisConnection l2 u2
⊢ GaloisConnection (l2 ∘ l1) (u1 ∘ u2)

Tactic:
fun _ _ ↦ (gc2 _ _).trans (gc1 _ _)

Premises used: Iff.trans, GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
ι : Type u
α : ι → Type v
β : ι → Type w
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → Preorder (β i)
l : (i : ι) → α i → β i
u : (i : ι) → β i → α i
gc : ∀ (i : ι), GaloisConnection (l i) (u i)
⊢ GaloisConnection (fun (a : (i : ι) → α i) (i : ι) ↦ l i (a i)) fun (b : (i : ι) → β i) (i : ι) ↦ u i (b i)

Tactic:
fun a b =>
  forall_congr' fun i => gc i (a i) (b i)

Premises used: forall_congr', GaloisConnection
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
X : Type u_2
inst : Preorder X
Y : Type u_3
inst_1 : Preorder Y
Z : Type u_4
inst_2 : Preorder Z
W : Type u_5
inst_3 : PartialOrder W
lYX : X → Y
uXY : Y → X
hXY : GaloisConnection lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : GaloisConnection lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : GaloisConnection lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : GaloisConnection lZX uXZ
h : ∀ (w : W), uXZ (uZW w) = uXY (uYW w)
x : X
⊢ lWZ (lZX x) = lWY (lYX x)

Tactic:
(hXZ.compose hZW).l_unique (hXY.compose hWY) h

Premises used: GaloisConnection.l_unique, GaloisConnection.compose
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
X : Type u_2
inst : PartialOrder X
Y : Type u_3
inst_1 : Preorder Y
Z : Type u_4
inst_2 : Preorder Z
W : Type u_5
inst_3 : Preorder W
lYX : X → Y
uXY : Y → X
hXY : GaloisConnection lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : GaloisConnection lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : GaloisConnection lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : GaloisConnection lZX uXZ
h : ∀ (x : X), lWZ (lZX x) = lWY (lYX x)
w : W
⊢ uXZ (uZW w) = uXY (uYW w)

Tactic:
(hXZ.compose hZW).u_unique (hXY.compose hWY) h

Premises used: GaloisConnection.u_unique, GaloisConnection.compose
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
X : Type u_2
inst : PartialOrder X
Y : Type u_3
inst_1 : Preorder Y
Z : Type u_4
inst_2 : Preorder Z
W : Type u_5
inst_3 : PartialOrder W
lYX : X → Y
uXY : Y → X
hXY : GaloisConnection lYX uXY
lWZ : Z → W
uZW : W → Z
hZW : GaloisConnection lWZ uZW
lWY : Y → W
uYW : W → Y
hWY : GaloisConnection lWY uYW
lZX : X → Z
uXZ : Z → X
hXZ : GaloisConnection lZX uXZ
⊢ (∀ (w : W), uXZ (uZW w) = uXY (uYW w)) ↔ ∀ (x : X), lWZ (lZX x) = lWY (lYX x)

Tactic:
⟨hXY.l_comm_of_u_comm hZW hWY hXZ, hXY.u_comm_of_l_comm hZW hWY hXZ⟩

Premises used: GaloisConnection.l_comm_of_u_comm, GaloisConnection.u_comm_of_l_comm, Iff.intro
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : PartialOrder β
gi : GaloisInsertion l u
b : β
⊢ l (u b) = b

Tactic:
(gi.gc.l_u_le _).antisymm (gi.le_l_u _)

Premises used: LE.le.antisymm, GaloisConnection.l_u_le, GaloisInsertion.le_l_u, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : PartialOrder β
gi : GaloisInsertion l u
⊢ LeftInverse l u

Tactic:
gi.l_u_eq

Premises used: Function.LeftInverse, GaloisInsertion.l_u_eq
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
gi : GaloisInsertion l u
⊢ l ⊤ = ⊤

Tactic:
top_unique <| (gi.le_l_u _).trans <| gi.gc.monotone_l le_top

Premises used: top_unique, le_top, LE.le.trans, GaloisInsertion.le_l_u, GaloisConnection.monotone_l, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : PartialOrder β
gi : GaloisInsertion l u
⊢ Surjective l

Tactic:
gi.leftInverse_l_u.surjective

Premises used: Function.LeftInverse.surjective, GaloisInsertion.leftInverse_l_u
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : PartialOrder β
gi : GaloisInsertion l u
⊢ Injective u

Tactic:
gi.leftInverse_l_u.injective

Premises used: Function.LeftInverse.injective, GaloisInsertion.leftInverse_l_u
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : Preorder β
gi : GaloisInsertion l u
a b : β
⊢ u a ≤ u b ↔ a ≤ b

Tactic:
⟨fun h => (gi.le_l_u _).trans (gi.gc.l_le h), fun h => gi.gc.monotone_u h⟩

Premises used: GaloisConnection.monotone_u, GaloisConnection.l_le, Iff.intro, LE.le.trans, GaloisInsertion.le_l_u, GaloisInsertion.gc
-- Module: Mathlib.Order.GaloisConnection.Defs
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : Preorder α
inst_1 : Preorder β
gi : GaloisInsertion l u
⊢ StrictMono u

Tactic:
strictMono_of_le_iff_le fun _ _ => gi.u_le_u_iff.symm

Premises used: strictMono_of_le_iff_le, GaloisInsertion.u_le_u_iff, Iff.symm