awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ScottContinuity
Goal:
β : Type u_2
inst : SemilatticeSup β
D : Set (Set (β × β))
⊢ ScottContinuousOn (β := β) D fun (x : β × β) ↦
    match (motive := β × β → β) x with
    | (a, b) => a ⊔ b

Tactic:
ScottContinuous.sup₂.scottContinuousOn

Premises used: ScottContinuous.sup₂, ScottContinuous.scottContinuousOn
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteSemilatticeSup α
inst_1 : Preorder β
f : α → β
⊢ IsOrderRightAdjoint f fun (y : β) ↦ sSup {x : α | f x ≤ y}

Tactic:
fun _ => isLUB_sSup _

Premises used: IsOrderRightAdjoint, setOf, LE.le, isLUB_sSup
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : Preorder β
f : α → β
hne : ∀ (y : β), ∃ (x : α), f x ≤ y
hbdd : ∀ (y : β), BddAbove.{u_1} (α := α) {x : α | f x ≤ y}
⊢ IsOrderRightAdjoint f fun (y : β) ↦ sSup {x : α | f x ≤ y}

Tactic:
fun y => isLUB_csSup (hne y) (hbdd y)

Premises used: IsOrderRightAdjoint, isLUB_csSup
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
f : α → β
g₁ g₂ : β → α
h₁ : IsOrderRightAdjoint f g₁
h₂ : IsOrderRightAdjoint f g₂
⊢ g₁ = g₂

Tactic:
funext fun y => (h₁ y).unique (h₂ y)

Premises used: funext, IsLUB.unique
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
⊢ Monotone g

Tactic:
fun y₁ y₂ hy => ((h y₁).mono (h y₂)) fun _ hx => le_trans hx hy

Premises used: Monotone, IsLUB.mono, le_trans
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : β ≃o γ
y : γ
⊢ IsLUB {x : α | ((⇑e : (a : β) → γ) ∘ f) x ≤ y} ((g ∘ (⇑e.symm : (a : γ) → β)) y)

Tactic:
simpa [e.le_symm_apply] using h (e.symm y)

Premises used: OrderIso.symm, OrderIso.le_symm_apply, DFunLike.coe
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
change :
  IsLUB.{u_3} (α := γ) (preimage.{u_3, u_1} (β := α) (⇑e : (a : γ) → α) {x : α | f x ≤ y} : Set γ)
    ((e.symm : (a : α) → γ) (g y) : γ)
⊢ IsLUB.{u_3} (α := γ) {x : γ | (f ∘ (⇑e : (a : γ) → α)) x ≤ y} (((⇑e.symm : (a : α) → γ) ∘ g) y)

Tactic:
change IsLUB (e ⁻¹' { x | f x ≤ y }) (e.symm (g y))

Premises used: setOf, LE.le, OrderIso.symm, Set.preimage, IsLUB, DFunLike.coe
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
rw : IsLUB {x : α | f x ≤ y} (g y)
⊢ IsLUB.{u_3} (α := γ) (preimage.{u_3, u_1} (β := α) (⇑e : (a : γ) → α) {x : α | f x ≤ y} : Set γ)
    ((e.symm : (a : α) → γ) (g y) : γ)

Tactic:
rw [e.isLUB_preimage, e.apply_symm_apply]

Premises used: OrderIso.apply_symm_apply, OrderIso.isLUB_preimage
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x : α | f x ≤ y} (g y)

Tactic:
h y
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB {x : α | f x ≤ y} (g y)

Tactic:
exact h y
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g (⇑fa : (a : α) → α) (⇑fb : (a : β) → β)
g' : β → α
hg' : IsOrderRightAdjoint g g'
⊢ Semiconj g' (⇑fb : (a : β) → β) (⇑fa : (a : α) → α)

Tactic:
fun y => (hg' _).unique ?_

Premises used: IsLUB.unique, Function.Semiconj, DFunLike.coe
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g (⇑fa : (a : α) → α) (⇑fb : (a : β) → β)
g' : β → α
hg' : IsOrderRightAdjoint g g'
refine : ∀ (y : β), IsLUB (α := α) ({x : α | g x ≤ (fb : (a : β) → β) y} : Set α) ((fa : (a : α) → α) (g' y) : α)
⊢ Semiconj g' (⇑fb : (a : β) → β) (⇑fa : (a : α) → α)

Tactic:
refine fun y => (hg' _).unique ?_

Premises used: IsLUB.unique
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g (⇑fa : (a : α) → α) (⇑fb : (a : β) → β)
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
rw :
  IsLUB (α := α) (image (α := α) (⇑fa : (a : α) → α) {a : α | g ((fa : (a : α) → α) a) ≤ (fb : (a : β) → β) y} : Set α)
    ((fa : (a : α) → α) (g' y) : α)
⊢ IsLUB (α := α) ({x : α | g x ≤ (fb : (a : β) → β) y} : Set α) ((fa : (a : α) → α) (g' y) : α)

Tactic:
rw [← fa.surjective.image_preimage { x | g x ≤ fb y }, preimage_setOf_eq]

Premises used: setOf, LE.le, OrderIso.surjective, Set.preimage_setOf_eq, Function.Surjective.image_preimage, DFunLike.coe
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g (⇑fa : (a : α) → α) (⇑fb : (a : β) → β)
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (α := α) (image (α := α) (⇑fa : (a : α) → α) {a : α | g ((fa : (a : α) → α) a) ≤ (fb : (a : β) → β) y} : Set α)
    ((fa : (a : α) → α) (g' y) : α)

Tactic:
simp only [h.eq, fb.le_iff_le, fa.leftOrdContinuous (hg' _)]

Premises used: Function.Semiconj.eq, OrderIso.leftOrdContinuous, OrderEmbedding.le_iff_le
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
G : Type u_4
inst : PartialOrder α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
h : α → α
H :
  ∀ (x : α),
    IsLUB
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
      (h x)
g : G
⊢ Semiconj h (⇑((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)

Tactic:
fun y => (H _).unique ?_

Premises used: IsLUB.unique, Function.Semiconj, DFunLike.coe
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
G : Type u_4
inst : PartialOrder α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
h : α → α
H :
  ∀ (x : α),
    IsLUB
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
      (h x)
g : G
refine :
  ∀ (y : α),
    IsLUB (α := α)
      (range fun (g' : G) ↦
          ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
            ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α)
                ((((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) y : α) :
              α) :
        Set α)
      ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
⊢ Semiconj h (⇑((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)

Tactic:
refine fun y => (H _).unique ?_

Premises used: IsLUB.unique
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
G : Type u_4
inst : PartialOrder α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
h : α → α
H :
  ∀ (x : α),
    IsLUB
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
      (h x)
g : G
y : α
⊢ IsLUB (α := α)
    (image (α := α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)
        (range fun (g' : G) ↦
          ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
            ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) y : α)) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)

Tactic:
have := (f₁ g).leftOrdContinuous (H y)
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
G : Type u_4
inst : PartialOrder α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
h : α → α
H :
  ∀ (x : α),
    IsLUB
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
      (h x)
g : G
y : α
this :
  IsLUB (α := α)
    (image (α := α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)
        (range fun (g' : G) ↦
          ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
            ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) y : α)) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
⊢ IsLUB (α := α)
    (range (ι := G)
        (comp (β := G)
          (comp (β := α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) fun (g' : G) ↦
            ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
              ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) y : α))
          (⇑(Equiv.mulRight g) : (a : G) → G)) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)

Tactic:
rw [← range_comp, ← (Equiv.mulRight g).surjective.range_comp _] at this

Premises used: Set.range_comp, Function.Surjective.range_comp, Equiv.mulRight, Equiv.surjective
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
G : Type u_4
inst : PartialOrder α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
h : α → α
H :
  ∀ (x : α),
    IsLUB
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
      (h x)
g : G
y : α
this :
  IsLUB (α := α)
    (range (ι := G)
        (comp (β := G)
          (comp (β := α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) fun (g' : G) ↦
            ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
              ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) y : α))
          (⇑(Equiv.mulRight g) : (a : G) → G)) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
⊢ IsLUB (α := α)
    (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α)
              ((((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) y : α) :
            α) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)

Tactic:
simpa [comp_def] using this

Premises used: Function.comp_def
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
G : Type u_4
inst : CompleteLattice α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
g : G
⊢ Semiconj (β := α)
    (fun (x : α) ↦
      ⨆ (g' : G),
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
    (⇑((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)

Tactic:
semiconj_of_isLUB f₁ f₂ (fun _ => isLUB_iSup) _

Premises used: isLUB_iSup, Function.semiconj_of_isLUB
-- Module: Mathlib.Order.SemiconjSup
Goal:
α : Type u_1
G : Type u_4
inst : ConditionallyCompleteLattice α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
hbdd :
  ∀ (x : α),
    BddAbove.{u_1} (α := α)
      (range fun (g : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g)⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) x : α))
g : G
⊢ Semiconj (β := α)
    (fun (x : α) ↦
      ⨆ (g' : G),
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
    (⇑((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)

Tactic:
semiconj_of_isLUB f₁ f₂ (fun x => isLUB_csSup (range_nonempty _) (hbdd x)) _

Premises used: iSup, Inv.inv, Set.range_nonempty, Function.semiconj_of_isLUB, isLUB_csSup, DFunLike.coe
-- Module: Mathlib.Order.Set
Goal:
α : Type u_1
β : Type u_2
f : WithBot α → β
⊢ range f = insert (f ⊥) (range (f ∘ some))

Tactic:
Option.range_eq f

Premises used: WithBot.some, WithBot, Option.range_eq
-- Module: Mathlib.Order.Set
Goal:
α : Type u_1
β : Type u_2
f : WithTop α → β
⊢ range f = insert (f ⊤) (range (f ∘ WithBot.some))

Tactic:
Option.range_eq f

Premises used: WithBot.some, Option.range_eq, WithTop
-- Module: Mathlib.Order.SetIsMax
Goal:
J : Type u
inst : Preorder J
S : Set J
m : (↑S : Type u)
hm : ¬IsMax m
⊢ ¬IsMax (↑m : J)

Tactic:
fun h ↦ hm (fun _ hb ↦ h hb)

Premises used: Not
-- Module: Mathlib.Order.SetIsMax
Goal:
J : Type u
inst : Preorder J
S : Set J
m : (↑S : Type u)
hm : ¬IsMin m
⊢ ¬IsMin (↑m : J)

Tactic:
fun h ↦ hm (fun _ hb ↦ h hb)

Premises used: Not
-- Module: Mathlib.Order.SetNotation
Goal:
α_1 : Type u
ι : Sort v
α : Type u_1
inst : InfSet α
⊢ Nonempty α

Tactic:
⟨sInf ∅⟩

Premises used: Nonempty.intro, EmptyCollection.emptyCollection, InfSet.sInf
-- Module: Mathlib.Order.SetNotation
Goal:
α : Type u
x : α
S : Set (Set α)
⊢ x ∈ ⋂₀ S ↔ ∀ (t : Set α), t ∈ S → x ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.sInter
-- Module: Mathlib.Order.SetNotation
Goal:
α : Type u
x : α
S : Set (Set α)
⊢ x ∈ ⋃₀ S ↔ ∃ (t : Set α), t ∈ S ∧ x ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.sUnion
-- Module: Mathlib.Order.SetNotation
Goal:
α : Type u
ι : Sort v
x : α
s : ι → Set α
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x ↔ ∃ (i : ι), x ∈ s i

Tactic:
⟨fun ⟨_, ⟨⟨a, (t_eq : s a = _)⟩, (h : x ∈ _)⟩⟩ => ⟨a, t_eq.symm ▸ h⟩, fun ⟨a, h⟩ =>
    ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩

Premises used: Membership.mem, Exists, _private.0.Set.mem_iUnion.match_2, Eq.rec, And.intro, Iff.intro, Exists.intro, _private.0.Set.mem_iUnion.match_1, Eq.symm, Set.iUnion, rfl
-- Module: Mathlib.Order.SetNotation
Goal:
α : Type u
ι : Sort v
x : α
s : ι → Set α
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), s i) x ↔ ∀ (i : ι), x ∈ s i

Tactic:
⟨fun (h : ∀ a ∈ { a : Set α | ∃ i, s i = a }, x ∈ a) a => h (s a) ⟨a, rfl⟩,
    fun h _ ⟨a, (eq : s a = _)⟩ => eq ▸ h a⟩

Premises used: Membership.mem, Eq.rec, Iff.intro, Exists.intro, _private.0.Set.mem_iInter.match_1, rfl
-- Module: Mathlib.Order.SetNotation
Goal:
α : Type u
S : Set (Set α)
⊢ sSup S = ⋃₀ S

Tactic:
rfl

Premises used: Set.sUnion, rfl
-- Module: Mathlib.Order.SetNotation
Goal:
α : Type u
S : Set (Set α)
⊢ sInf S = ⋂₀ S

Tactic:
rfl

Premises used: Set.sInter, rfl
-- Module: Mathlib.Order.SetNotation
Goal:
α : Type u
ι : Sort v
s : ι → Set α
⊢ iSup s = iUnion s

Tactic:
rfl

Premises used: Set.iUnion, rfl
-- Module: Mathlib.Order.SetNotation
Goal:
α : Type u
ι : Sort v
s : ι → Set α
⊢ iInf s = iInter s

Tactic:
rfl

Premises used: Set.iInter, rfl
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Bot α
⊢ Eq.{u + 1} (α := Shrink.{u, u_1} α) ((equivShrink α : (a : α) → Shrink.{u, u_1} α) ⊥ : Shrink.{u, u_1} α)
    (⊥ : Shrink.{u, u_1} α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Bot α
⊢ Eq.{u + 1} (α := Shrink.{u, u_1} α)
    ((equivShrink α : (a : α) → Shrink.{u, u_1} α) ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) ⊥ : α) :
      Shrink.{u, u_1} α)
    ((equivShrink α : (a : α) → Shrink.{u, u_1} α) ⊥ : Shrink.{u, u_1} α)

Tactic:
simp
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
a b : α
obtain :
  ∀ (a : Shrink.{u, u_1} α),
    LE.le.{u} (α := Shrink.{u, u_1} α)
        ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
            ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α) :
          Shrink.{u, u_1} α)
        ((equivShrink α : (a : α) → Shrink.{u, u_1} α) b : Shrink.{u, u_1} α) ↔
      (Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a ≤ b
⊢ LE.le.{u} (α := Shrink.{u, u_1} α) ((equivShrink α : (a : α) → Shrink.{u, u_1} α) a : Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) b : Shrink.{u, u_1} α) ↔
    a ≤ b

Tactic:
obtain ⟨a, rfl⟩ := (equivShrink.{u} α).symm.surjective a

Premises used: rfl
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
b : α
a : Shrink.{u, u_1} α
obtain :
  ∀ (b : Shrink.{u, u_1} α),
    LE.le.{u} (α := Shrink.{u, u_1} α)
        ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
            ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α) :
          Shrink.{u, u_1} α)
        ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
            ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α) :
          Shrink.{u, u_1} α) ↔
      LE.le.{u_1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)
        ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α)
⊢ LE.le.{u} (α := Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α) :
        Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) b : Shrink.{u, u_1} α) ↔
    (Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a ≤ b

Tactic:
obtain ⟨b, rfl⟩ := (equivShrink.{u} α).symm.surjective b

Premises used: rfl
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
a b : Shrink.{u, u_1} α
simp :
  a ≤ b ↔
    LE.le.{u_1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)
      ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α)
⊢ LE.le.{u} (α := Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α) :
        Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α) :
        Shrink.{u, u_1} α) ↔
    LE.le.{u_1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)
      ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α)

Tactic:
simp only [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
a b : Shrink.{u, u_1} α
⊢ a ≤ b ↔
    LE.le.{u_1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)
      ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α)

Tactic:
rfl
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
a : α
⊢ Eq.{u + 1} (α := Shrink.{u, u_1} α) ((orderIsoShrink α : (a : α) → Shrink.{u, u_1} α) a : Shrink.{u, u_1} α)
    ((equivShrink α : (a : α) → Shrink.{u, u_1} α) a : Shrink.{u, u_1} α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
a : Shrink.{u, u_1} α
⊢ Eq.{u_1 + 1} (α := α) ((OrderIso.symm (orderIsoShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)
    ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
x y : α
⊢ LE.le.{u} (α := Shrink.{u, u_1} α) ((equivShrink α : (a : α) → Shrink.{u, u_1} α) x : Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) y : Shrink.{u, u_1} α) ↔
    x ≤ y

Tactic:
(orderIsoShrink α).map_rel_iff

Premises used: RelIso.map_rel_iff, orderIsoShrink
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
x y : α
⊢ LT.lt.{u} (α := Shrink.{u, u_1} α) ((equivShrink α : (a : α) → Shrink.{u, u_1} α) x : Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) y : Shrink.{u, u_1} α) ↔
    x < y

Tactic:
(orderIsoShrink α).toRelIsoLT.map_rel_iff

Premises used: OrderIso.toRelIsoLT, RelIso.map_rel_iff, orderIsoShrink
-- Module: Mathlib.Order.Shrink
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
inst_2 : OrderBot α
a : Shrink.{u, u_1} α
⊢ ⊥ ≤ a

Tactic:
simp [← (orderIsoShrink.{u} α).symm.le_iff_le]
-- Module: Mathlib.Order.Sublattice
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
L_1 M_1 : Sublattice α
f : LatticeHom α β
s t : Set α
a b : α
L M : Sublattice α
h : Eq.{u_2 + 1} (α := Set α) ((fun (L : Sublattice α) ↦ L.carrier) L) ((fun (L : Sublattice α) ↦ L.carrier) M)
mk :
  ∀ (carrier : Set α) (supClosed' : SupClosed carrier) (infClosed' : InfClosed carrier)
    (h :
      Eq.{u_2 + 1} (α := Set α)
        ((fun (L : Sublattice α) ↦ L.carrier)
          { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' })
        ((fun (L : Sublattice α) ↦ L.carrier) M)),
    { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α } = M
⊢ L = M

Tactic:
cases L
-- Module: Mathlib.Order.Sublattice
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
L M_1 : Sublattice α
f : LatticeHom α β
s t : Set α
a b : α
M : Sublattice α
carrier : Set α
supClosed' : SupClosed carrier
infClosed' : InfClosed carrier
h :
  Eq.{u_2 + 1} (α := Set α)
    ((fun (L : Sublattice α) ↦ L.carrier) { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' })
    ((fun (L : Sublattice α) ↦ L.carrier) M)
⊢ { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α } = M

Tactic:
congr
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L M : Sublattice α
⊢ (↑L : Set α) = (↑M : Set α) ↔ L = M

Tactic:
SetLike.coe_set_eq

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ SupClosed (↑L : Set α)

Tactic:
L.supClosed'

Premises used: Sublattice.supClosed'
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ InfClosed (↑L : Set α)

Tactic:
L.infClosed'

Premises used: Sublattice.infClosed'
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⊔ b ∈ L

Tactic:
L.supClosed ha hb

Premises used: Sublattice.supClosed
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⊓ b ∈ L

Tactic:
L.infClosed ha hb

Premises used: Sublattice.infClosed
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ IsSublattice (↑L : Set α)

Tactic:
⟨L.supClosed, L.infClosed⟩

Premises used: Sublattice.supClosed, Sublattice.infClosed, IsSublattice.mk
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
a : α
⊢ a ∈ L.carrier ↔ a ∈ L

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
s : Set α
a : α
h_sup : SupClosed s
h_inf : InfClosed s
⊢ a ∈ { carrier := s, supClosed' := h_sup, infClosed' := h_inf : Sublattice α } ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
s : Set α
h_sup : SupClosed s
h_inf : InfClosed s
⊢ (↑{ carrier := s, supClosed' := h_sup, infClosed' := h_inf : Sublattice α } : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
s t : Set α
hs_sup : SupClosed s
hs_inf : InfClosed s
ht_sup : SupClosed t
ht_inf : InfClosed t
⊢ { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf : Sublattice α } ≤
      { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔
    s ⊆ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Set.Subset
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
s t : Set α
hs_sup : SupClosed s
hs_inf : InfClosed s
ht_sup : SupClosed t
ht_inf : InfClosed t
⊢ { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf : Sublattice α } <
      { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔
    s ⊂ t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Sublattice
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
s : Set α
hs : s = (↑L : Set α)
⊢ (↑(L.copy s hs) : Set α) = s

Tactic:
rfl

Premises used: rfl