awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
refine : ∀ (h : lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β)), Nonempty.{u + 1} (α ↪o β)
⊢ lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β) ↔ Nonempty.{u + 1} (α ↪o β)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h⟩ ↦ type_le_type <| (ULift.orderIso.toOrderEmbedding.trans h).trans
   ULift.orderIso.symm.toOrderEmbedding⟩
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β)
⊢ Nonempty (ULift.{u_1, u} α ↪o ULift.{u_1, u} β)

Tactic:
rw [← type_ulift, ← type_ulift, type_le_type_iff] at h

Premises used: OrderType.type_le_type_iff, OrderType.type_ulift
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : Nonempty (ULift.{u_1, u} α ↪o ULift.{u_1, u} β)
⊢ Nonempty.{u + 1} (α ↪o β)

Tactic:
⟨(ULift.orderIso.symm.toOrderEmbedding.trans h.some).trans ULift.orderIso.toOrderEmbedding⟩

Premises used: OrderIso.toOrderEmbedding, ULift.orderIso, Nonempty.some, Nonempty.intro, OrderIso.symm, RelEmbedding.trans
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : Nonempty (ULift.{u_1, u} α ↪o ULift.{u_1, u} β)
⊢ Nonempty.{u + 1} (α ↪o β)

Tactic:
exact ⟨(ULift.orderIso.symm.toOrderEmbedding.trans h.some).trans ULift.orderIso.toOrderEmbedding⟩
-- Module: Mathlib.Order.Types.Defs
Goal:
x x_1 : ℕ
⊢ LE.le (α := ULift (↑{ carrier := ℕ, str := Nat.instLinearOrder } : Type))
      ((Equiv.symm Equiv.ulift : (a : ℕ) → ULift (↑{ carrier := ℕ, str := Nat.instLinearOrder } : Type)) x :
        ULift (↑{ carrier := ℕ, str := Nat.instLinearOrder } : Type))
      ((Equiv.symm Equiv.ulift : (a : ℕ) → ULift (↑{ carrier := ℕ, str := Nat.instLinearOrder } : Type)) x_1 :
        ULift (↑{ carrier := ℕ, str := Nat.instLinearOrder } : Type)) ↔
    x ≤ x_1

Tactic:
simp only [ulift_symm_apply, ULift.up_le]

Premises used: Equiv.ulift_symm_apply, ULift.up_le
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : LE α
a b : α
⊢ { down := a : ULift.{u_1, u} α } ≤ { down := b } ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : LE α
a b : ULift.{u_1, u} α
⊢ a.down ≤ b.down ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : LT α
a b : α
⊢ { down := a : ULift.{u_1, u} α } < { down := b } ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : LT α
a b : ULift.{u_1, u} α
⊢ a.down < b.down ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : BEq α
a b : α
⊢ ({ down := a : ULift.{u_1, u} α } == { down := b : ULift.{u_1, u} α }) = (a == b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : BEq α
a b : ULift.{u_1, u} α
⊢ (a.down == b.down) = (a == b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : Ord α
a b : α
⊢ compare { down := a : ULift.{u_1, u} α } { down := b : ULift.{u_1, u} α } = compare a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : Ord α
a b : ULift.{u_1, u} α
⊢ compare a.down b.down = compare a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : Max α
a b : α
⊢ { down := a ⊔ b : ULift.{u_1, u} α } = { down := a } ⊔ { down := b }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : Max α
a b : ULift.{u_1, u} α
⊢ down.{u_1, u} (a ⊔ b) = a.down ⊔ b.down

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : SDiff α
a b : α
⊢ { down := a \ b : ULift.{u_1, u} α } = { down := a } \ { down := b }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : SDiff α
a b : ULift.{u_1, u} α
⊢ down.{u_1, u} (a \ b) = a.down \ b.down

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : Compl α
a : α
⊢ { down := aᶜ : ULift.{u_1, u} α } = { down := a }ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.ULift
Goal:
α : Type u
inst : Compl α
a : ULift.{u_1, u} α
⊢ down.{u_1, u} aᶜ = a.downᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
⊢ IsUpperSet.{u_1} (α := α) ∅

Tactic:
fun _ _ _ => id

Premises used: Set.Mem, IsUpperSet, id
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
⊢ IsUpperSet.{u_1} (α := α) univ

Tactic:
fun _ _ _ => id

Premises used: Set.Mem, Set.univ, setOf, IsUpperSet, id
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s : Set α
hs : IsUpperSet s
⊢ IsLowerSet sᶜ

Tactic:
fun _a _b h hb ha => hb <| hs h ha

Premises used: Set.Mem, setOf, IsLowerSet, Not
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ IsLowerSet sᶜᶜ

Tactic:
h.compl

Premises used: IsUpperSet.compl
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s : Set α
h : IsUpperSet sᶜ
h₁ : s = sᶜᶜ
⊢ IsLowerSet s

Tactic:
convert! h.compl

Premises used: IsUpperSet.compl
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s : Set α
h : IsUpperSet sᶜ
h₁ h₂ : s = s
⊢ s = sᶜᶜ

Tactic:
rw [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
⊢ IsUpperSet (s ∪ t)

Tactic:
fun _ _ h => Or.imp (hs h) (ht h)

Premises used: Set.union, Set.Mem, setOf, IsUpperSet, Or.imp
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
⊢ IsUpperSet (s ∩ t)

Tactic:
fun _ _ h => And.imp (hs h) (ht h)

Premises used: And.imp, Set.Mem, setOf, IsUpperSet, Set.inter
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
S : Set (Set α)
hf : ∀ s ∈ S, IsUpperSet s
⊢ IsUpperSet (⋃₀ S)

Tactic:
fun _ _ h => Exists.imp fun _ hs => ⟨hs.1, hf _ hs.1 h hs.2⟩

Premises used: Set.Mem, setOf, IsUpperSet, Set.sUnion, Exists.imp, And.right, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
ι : Sort u_3
inst : LE α
f : ι → Set α
hf : ∀ (i : ι), IsUpperSet (f i)
⊢ IsUpperSet.{u_1} (α := α) (⋃ (i : ι), f i)

Tactic:
isUpperSet_sUnion <| forall_mem_range.2 hf

Premises used: Iff.mpr, Set.forall_mem_range, iSup, isUpperSet_sUnion, Set.iUnion
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
ι : Sort u_3
κ : ι → Sort u_4
inst : LE α
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsUpperSet (f i j)
⊢ IsUpperSet.{u_1} (α := α) (⋃ (i : ι), ⋃ (j : κ i), f i j)

Tactic:
isUpperSet_iUnion fun i => isUpperSet_iUnion <| hf i

Premises used: isUpperSet_iUnion
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
S : Set (Set α)
hf : ∀ s ∈ S, IsUpperSet s
⊢ IsUpperSet (⋂₀ S)

Tactic:
fun _ _ h => forall₂_imp fun s hs => hf s hs h

Premises used: Set.Mem, forall₂_imp, setOf, IsUpperSet, Set.sInter
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
ι : Sort u_3
inst : LE α
f : ι → Set α
hf : ∀ (i : ι), IsUpperSet (f i)
⊢ IsUpperSet.{u_1} (α := α) (⋂ (i : ι), f i)

Tactic:
isUpperSet_sInter <| forall_mem_range.2 hf

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, isUpperSet_sInter
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
ι : Sort u_3
κ : ι → Sort u_4
inst : LE α
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsUpperSet (f i j)
⊢ IsUpperSet.{u_1} (α := α) (⋂ (i : ι), ⋂ (j : κ i), f i j)

Tactic:
isUpperSet_iInter fun i => isUpperSet_iInter <| hf i

Premises used: isUpperSet_iInter
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s : Set α
⊢ IsUpperSet (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔ IsLowerSet s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, IsLowerSet, OrderDual
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s : Set αᵒᵈ
⊢ IsUpperSet (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ IsLowerSet s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, IsLowerSet, OrderDual
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s t : Set α
hs : IsUpperSet s
⊢ IsLowerSet (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Tactic:
aesop
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s t : Set α
hs : IsUpperSet s
ht : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ IsUpperSet (s \ t)

Tactic:
fun _b _c hbc hb ↦ ⟨hs hbc hb.1, fun hc ↦ hb.2 <| ht _ hb.1 _ hc hbc⟩

Premises used: Set.Mem, Set.diff, setOf, IsUpperSet, And.right, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s t : Set α
hs : IsUpperSet s
ht : IsLowerSet t
⊢ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t

Tactic:
aesop
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LE α
s : Set α
a : α
hs : IsUpperSet s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, ∀ (c : α), Membership.mem (γ := Set α) {a} c → b ≤ c → Membership.mem (γ := Set α) {a} b

Tactic:
simpa using has
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsUpperSet (Ici a)

Tactic:
fun _ _ => ge_trans

Premises used: Set.Ici, Set.Mem, setOf, IsUpperSet, ge_trans
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsUpperSet (Ioi a)

Tactic:
fun _ _ => flip lt_of_lt_of_le

Premises used: IsUpperSet, flip, lt_of_lt_of_le
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ici a ⊆ s

Tactic:
simp [IsUpperSet, subset_def, @forall_comm (_ ∈ s)]

Premises used: Set.subset_def, IsUpperSet, forall_comm
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : IsUpperSet s
a : α
ha : a ∈ s
⊢ Ioi a ⊆ s

Tactic:
Ioi_subset_Ici_self.trans <| h.Ici_subset ha

Premises used: Set.Ioi_subset_Ici_self, IsUpperSet.Ici_subset, HasSubset.Subset.trans
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : IsUpperSet s
⊢ s.OrdConnected

Tactic:
⟨fun _ ha _ _ => Icc_subset_Ici_self.trans <| h.Ici_subset ha⟩

Premises used: IsUpperSet.Ici_subset, HasSubset.Subset.trans, Set.OrdConnected.mk, Set.Icc_subset_Ici_self
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : IsLowerSet s
⊢ s.OrdConnected

Tactic:
⟨fun _ _ _ hb => Icc_subset_Iic_self.trans <| h.Iic_subset hb⟩

Premises used: IsLowerSet.Iic_subset, Set.Icc_subset_Iic_self, HasSubset.Subset.trans, Set.OrdConnected.mk
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : IsUpperSet s
f : β → α
hf : Monotone f
⊢ IsUpperSet (f ⁻¹' s)

Tactic:
fun _ _ h => hs <| hf h

Premises used: Set.Mem, setOf, IsUpperSet, Set.preimage
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
change : IsUpperSet.{u_2} (α := β) ((⇑(↑f : α ≃ β) : (a : α) → β) '' s)
⊢ IsUpperSet.{u_2} (α := β) ((⇑f : (a : α) → β) '' s)

Tactic:
change IsUpperSet ((f : α ≃ β) '' s)

Premises used: IsUpperSet, Set.image, DFunLike.coe, EquivLike.toEquiv
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
rw : IsUpperSet.{u_2} (α := β) ((⇑(↑f : α ≃ β).symm : (a : β) → α) ⁻¹' s)
⊢ IsUpperSet.{u_2} (α := β) ((⇑(↑f : α ≃ β) : (a : α) → β) '' s)

Tactic:
rw [Equiv.image_eq_preimage_symm]

Premises used: Equiv.image_eq_preimage_symm
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet.{u_2} (α := β) ((⇑(↑f : α ≃ β).symm : (a : β) → α) ⁻¹' s)

Tactic:
hs.preimage f.symm.monotone

Premises used: OrderIso.monotone, IsUpperSet.preimage, OrderIso.symm
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet.{u_2} (α := β) ((⇑(↑f : α ≃ β).symm : (a : β) → α) ⁻¹' s)

Tactic:
exact hs.preimage f.symm.monotone

Premises used: OrderIso.monotone, IsUpperSet.preimage, OrderIso.symm
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : IsUpperSet.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
a : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ici ((e : (a : α) → β) a) : Set β)) :
      Set β)
    (Ici ((e : (a : α) → β) a) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β) (Ici ((e : (a : α) → β) a) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ici ((e : (a : α) → β) a) : Set β)
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set β) (Ici ((e : (a : α) → β) a) : Set β) (Ici ((e : (a : α) → β) a) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ici a : Set β) (Ici ((e : (a : α) → β) a) : Set β)

Tactic:
rw [← e.preimage_Ici, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]

Premises used: Set.inter_eq_left, Set.mem_range_self, Iff.mpr, OrderEmbedding.preimage_Ici, IsUpperSet.Ici_subset, Set.image_preimage_eq_inter_range
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : IsUpperSet.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
a : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ioi ((e : (a : α) → β) a) : Set β)) :
      Set β)
    (Ioi ((e : (a : α) → β) a) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β) (Ioi ((e : (a : α) → β) a) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ioi ((e : (a : α) → β) a) : Set β)
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set β) (Ioi ((e : (a : α) → β) a) : Set β) (Ioi ((e : (a : α) → β) a) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioi a : Set β) (Ioi ((e : (a : α) → β) a) : Set β)

Tactic:
rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]

Premises used: Set.inter_eq_left, Set.mem_range_self, Iff.mpr, Set.image_preimage_eq_inter_range, IsUpperSet.Ioi_subset, OrderEmbedding.preimage_Ioi
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ (Monotone (β := Prop) fun (x : α) ↦ x ∈ s) ↔ IsUpperSet s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Monotone, IsUpperSet
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ (Antitone (β := Prop) fun (x : α) ↦ x ∈ s) ↔ IsLowerSet s

Tactic:
forall_comm

Premises used: forall_comm, Antitone, IsLowerSet
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
⊢ IsUpperSet.{u_1} (α := α) {a : α | p a} ↔ Monotone p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Monotone, setOf, IsUpperSet
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
p : α → Prop
⊢ IsLowerSet.{u_1} (α := α) {a : α | p a} ↔ Antitone p

Tactic:
forall_comm

Premises used: Set.Mem, setOf, forall_comm, Antitone, IsLowerSet
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsUpperSet s
⊢ s.Nonempty → upperBounds s ⊆ s

Tactic:
fun ⟨_a, ha⟩ _b hb ↦ hs (hb ha) ha

Premises used: Membership.mem, Set.Subset, _private.0.IsUpperSet.upperBounds_subset.match_1
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : OrderTop α
hs : IsLowerSet s
⊢ ⊤ ∈ s ↔ s = univ

Tactic:
⟨fun h => eq_univ_of_forall fun _ => hs le_top h, fun h => h.symm ▸ mem_univ _⟩

Premises used: Eq.rec, Set.eq_univ_of_forall, le_top, Iff.intro, Set.mem_univ, Top.top, Eq.symm
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : OrderTop α
hs : IsUpperSet s
⊢ ⊤ ∈ s ↔ s.Nonempty

Tactic:
⟨fun h => ⟨_, h⟩, fun ⟨_a, ha⟩ => hs le_top ha⟩

Premises used: Membership.mem, le_top, Iff.intro, Exists.intro, Top.top, _private.0.IsUpperSet.upperBounds_subset.match_1
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : OrderTop α
hs : IsUpperSet s
⊢ ⊤ ∉ s ↔ s = ∅

Tactic:
hs.top_mem.not.trans not_nonempty_iff_eq_empty

Premises used: Set.not_nonempty_iff_eq_empty, IsUpperSet.top_mem, Iff.not, Iff.trans
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
obtain : ∀ (c : α) (hc : b < c), False
⊢ False

Tactic:
obtain ⟨c, hc⟩ := exists_gt b

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
c : α
hc : b < c
⊢ False

Tactic:
hc.not_ge (hb <| hs ((hb ha).trans hc.le) ha)

Premises used: LT.lt.le, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
c : α
hc : b < c
⊢ False

Tactic:
exact hc.not_ge (hb <| hs ((hb ha).trans hc.le) ha)

Premises used: LT.lt.le, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
inst_1 : NoMaxOrder α
⊢ ¬BddAbove (Ici a)

Tactic:
(isUpperSet_Ici _).not_bddAbove nonempty_Ici

Premises used: isUpperSet_Ici, IsUpperSet.not_bddAbove, Set.nonempty_Ici
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
inst_1 : NoMaxOrder α
⊢ ¬BddAbove (Ioi a)

Tactic:
(isUpperSet_Ioi _).not_bddAbove nonempty_Ioi

Premises used: isUpperSet_Ioi, Set.nonempty_Ioi, IsUpperSet.not_bddAbove
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a : α
⊢ (∀ ⦃b : α⦄, a ≤ b → a ∈ s → b ∈ s) ↔ ∀ ⦃b : α⦄, a < b → a ∈ s → b ∈ s

Tactic:
simp [le_iff_eq_or_lt, or_imp, forall_and]

Premises used: le_iff_eq_or_lt, or_imp, forall_and
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ioi a ⊆ s

Tactic:
simp [isUpperSet_iff_forall_lt, subset_def, @forall_comm (_ ∈ s)]

Premises used: isUpperSet_iff_forall_lt, Set.subset_def, forall_comm
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
⊢ s ⊆ t ∨ t ⊆ s

Tactic:
grind [isUpperSet_iff_forall_lt]

Premises used: isUpperSet_iff_forall_lt
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsUpperSet s
⊢ s = ∅ ∨ ∃ (a : α), s = Ici a

Tactic:
or_iff_not_imp_left.2 fun ha ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsUpperSet s
refine : ∀ (ha : ¬s = ∅), ∃ (a : α), s = Ici a
⊢ s = ∅ ∨ ∃ (a : α), s = Ici a

Tactic:
refine or_iff_not_imp_left.2 fun ha ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsUpperSet s
ha : ¬s = ∅
obtain : ∀ (a : α) (ha : a ∈ s), ∃ (a : α), s = Ici a
⊢ ∃ (a : α), s = Ici a

Tactic:
obtain ⟨a, ha⟩ := Set.nonempty_iff_ne_empty.2 ha

Premises used: Iff.mpr, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsUpperSet s
ha_1 : ¬s = ∅
a : α
ha : a ∈ s
⊢ ∃ (a : α), s = Ici a

Tactic:
⟨_, ext fun b ↦ ⟨wellFounded_lt.min_le, (h · <| wellFounded_lt.min_mem _ ⟨a, ha⟩)⟩⟩

Premises used: Set.ext, WellFounded.min_mem, wellFounded_lt, Iff.intro, Exists.intro
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsUpperSet s
ha_1 : ¬s = ∅
a : α
ha : a ∈ s
⊢ ∃ (a : α), s = Ici a

Tactic:
exact ⟨_, ext fun b ↦ ⟨wellFounded_lt.min_le, (h · <| wellFounded_lt.min_mem _ ⟨a, ha⟩)⟩⟩
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsLowerSet s
simp_rw : sᶜ = univᶜ ∨ ∃ (a : α), sᶜ = (Iio a)ᶜ
⊢ s = univ ∨ ∃ (a : α), s = Iio a

Tactic:
simp_rw [← @compl_inj_iff _ s]

Premises used: compl_inj_iff
-- Module: Mathlib.Order.UpperLower.Basic
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsLowerSet s
⊢ sᶜ = univᶜ ∨ ∃ (a : α), sᶜ = (Iio a)ᶜ

Tactic:
simpa using h.compl.eq_empty_or_Ici

Premises used: IsUpperSet.eq_empty_or_Ici, IsLowerSet.compl
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
x : α
⊢ Membership.mem (γ := UpperSet α) (upperClosure s) x ↔ ∃ a ∈ s, a ≤ x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : ∀ (x : α), x ∈ (↑(upperClosure s) : Set α) ↔ Membership.mem (γ := Set α) (⋃ a ∈ s, Ici a) x
⊢ (↑(upperClosure s) : Set α) = ⋃ a ∈ s, Ici a

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
x : α
⊢ x ∈ (↑(upperClosure s) : Set α) ↔ Membership.mem (γ := Set α) (⋃ a ∈ s, Ici a) x

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ s ⊆ (↑(upperClosure s) : Set α)

Tactic:
fun x hx => ⟨x, hx, le_rfl⟩

Premises used: le_rfl, Set.Mem, setOf, Set.Subset, And.intro, Exists.intro
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : s ⊆ t
ht : IsUpperSet t
⊢ (↑(upperClosure s) : Set α) ⊆ t

Tactic:
fun _a ⟨_b, hb, hba⟩ => ht hba <| h hb

Premises used: _private.0.upperClosure_min.match_1, Membership.mem, Set.Subset
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsUpperSet s
⊢ (↑(upperClosure s) : Set α) = s

Tactic:
(upperClosure_min Subset.rfl hs).antisymm subset_upperClosure

Premises used: subset_upperClosure, upperClosure_min, Set.Subset.rfl, HasSubset.Subset.antisymm
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
⊢ upperClosure (↑s : Set α) = s

Tactic:
SetLike.coe_injective s.2.upperClosure

Premises used: UpperSet.upper', IsUpperSet.upperClosure, SetLike.coe_injective
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ≃o β
rw :
  Eq.{u_2 + 1} (α := UpperSet β) (upperClosure ((⇑f : (a : α) → β) '' s))
    (((UpperSet.map f.symm).symm : (a : UpperSet α) → UpperSet β) (upperClosure s))
⊢ Eq.{u_2 + 1} (α := UpperSet β) (upperClosure ((⇑f : (a : α) → β) '' s))
    ((UpperSet.map f : (a : UpperSet α) → UpperSet β) (upperClosure s))

Tactic:
rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]

Premises used: OrderIso.symm_symm, UpperSet.symm_map
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ≃o β
a :
  ∀ (x : β),
    x ∈ (↑(upperClosure ((⇑f : (a : α) → β) '' s)) : Set β) ↔
      x ∈ (↑(((UpperSet.map f.symm).symm : (a : UpperSet α) → UpperSet β) (upperClosure s) : UpperSet β) : Set β)
⊢ Eq.{u_2 + 1} (α := UpperSet β) (upperClosure ((⇑f : (a : α) → β) '' s))
    (((UpperSet.map f.symm).symm : (a : UpperSet α) → UpperSet β) (upperClosure s))

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ≃o β
x : β
⊢ Membership.mem (γ := UpperSet β) (upperClosure ((⇑f : (a : α) → β) '' s)) x ↔
    Membership.mem (γ := UpperSet β)
      (((UpperSet.map f.symm).symm : (a : UpperSet α) → UpperSet β) (upperClosure s) : UpperSet β) x

Tactic:
simp [f.le_symm_apply]

Premises used: OrderIso.le_symm_apply