awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : Sublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
simp [← mem_subtype]

Premises used: Sublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : Sublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Tactic:
simp [← mem_subtype]

Premises used: Sublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : Sublattice (Set X)
T : ↥L
x : X
⊢ x ∈ (↑T : Set X) ↔ x ∈ T

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
h : ∀ (x : X), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
T : ↥L
x : X
⊢ Membership.mem (γ := Set X) ((L.subtype : (a : ↥L) → Set X) T : Set X) x ↔ x ∈ T

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
simp [← mem_subtype]

Premises used: CompleteSublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
𝒮 : Set ↥L
x : X
⊢ x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T

Tactic:
simp [← mem_subtype]

Premises used: CompleteSublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
I : Sort u_2
f : I → ↥L
x : X
⊢ Membership.mem (γ := ↥L) (⨅ (i : I), f i) x ↔ ∀ (i : I), x ∈ f i

Tactic:
simp [← mem_subtype]

Premises used: CompleteSublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
x : X
⊢ Membership.mem (γ := ↥L) ⊤ x

Tactic:
simp [← mem_subtype]

Premises used: CompleteSublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Tactic:
simp [← mem_subtype]

Premises used: CompleteSublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
𝒮 : Set ↥L
x : X
⊢ x ∈ sSup 𝒮 ↔ ∃ T ∈ 𝒮, x ∈ T

Tactic:
simp [← mem_subtype]

Premises used: CompleteSublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
I : Sort u_2
f : I → ↥L
x : X
⊢ Membership.mem (γ := ↥L) (⨆ (i : I), f i) x ↔ ∃ (i : I), x ∈ f i

Tactic:
simp [← mem_subtype]

Premises used: CompleteSublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLattice.SetLike
Goal:
X : Type u_1
L : CompleteSublattice (Set X)
x : X
⊢ x ∉ ⊥

Tactic:
simp [← mem_subtype]

Premises used: CompleteSublattice.mem_subtype
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : SupSet α
inst_2 : Inhabited (↑s : Type u_2)
⊢ Eq.{u_2 + 1} (α := Set (↑s : Type u_2) → (↑s : Type u_2)) sSup fun (t : Set (↑s : Type u_2)) ↦
    if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s then
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)) ⋯
    else default

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : SupSet α
inst_2 : Inhabited (↑s : Type u_2)
t : Set (↑s : Type u_2)
h' : t.Nonempty
h'' : BddAbove t
h : sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) = (↑(sSup t) : α)

Tactic:
simp [h, h', h'']
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : SupSet α
inst_2 : Inhabited (↑s : Type u_2)
⊢ Eq.{u_2 + 1} (α := (↑s : Type u_2)) (sSup ∅) default

Tactic:
simp [sSup]

Premises used: SupSet.sSup
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : SupSet α
inst_2 : Inhabited (↑s : Type u_2)
t : Set (↑s : Type u_2)
ht : ¬BddAbove t
⊢ sSup t = default

Tactic:
simp [sSup, ht]

Premises used: SupSet.sSup
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : InfSet α
inst_2 : Inhabited (↑s : Type u_2)
⊢ Eq.{u_2 + 1} (α := Set (↑s : Type u_2) → (↑s : Type u_2)) sInf fun (t : Set (↑s : Type u_2)) ↦
    if ht : t.Nonempty ∧ BddBelow t ∧ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s then
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)) ⋯
    else default

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : InfSet α
inst_2 : Inhabited (↑s : Type u_2)
t : Set (↑s : Type u_2)
h' : t.Nonempty
h'' : BddBelow t
h : sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) = (↑(sInf t) : α)

Tactic:
simp [h, h', h'']
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : InfSet α
inst_2 : Inhabited (↑s : Type u_2)
⊢ Eq.{u_2 + 1} (α := (↑s : Type u_2)) (sInf ∅) default

Tactic:
simp [sInf]

Premises used: InfSet.sInf
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : InfSet α
inst_2 : Inhabited (↑s : Type u_2)
t : Set (↑s : Type u_2)
ht : ¬BddBelow t
⊢ sInf t = default

Tactic:
simp [sInf, ht]

Premises used: InfSet.sInf
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddAbove t
rw : IsLUB ((fun {y : (↑s : Type u_2)} ↦ (↑y : α)) '' t) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))
⊢ IsLUB ((fun {y : (↑s : Type u_2)} ↦ (↑y : α)) '' t) (↑(sSup t) : α)

Tactic:
rw [← subset_sSup_of_within s ht h_bdd (h_Sup ht h_bdd)]

Premises used: subset_sSup_of_within
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddAbove t
⊢ IsLUB ((fun {y : (↑s : Type u_2)} ↦ (↑y : α)) '' t) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))

Tactic:
isLUB_csSup (ht.image _) ((Subtype.mono_coe _).map_bddAbove h_bdd)

Premises used: Subtype.mono_coe, Monotone.map_bddAbove, Set.Nonempty.image, isLUB_csSup
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddAbove t
⊢ IsLUB ((fun {y : (↑s : Type u_2)} ↦ (↑y : α)) '' t) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))

Tactic:
exact isLUB_csSup (ht.image _) ((Subtype.mono_coe _).map_bddAbove h_bdd)

Premises used: Subtype.mono_coe, Monotone.map_bddAbove, Set.Nonempty.image, isLUB_csSup
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddBelow t
rw : IsGLB ((fun {x : (↑s : Type u_2)} ↦ (↑x : α)) '' t) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))
⊢ IsGLB ((fun {x : (↑s : Type u_2)} ↦ (↑x : α)) '' t) (↑(sInf t) : α)

Tactic:
rw [← subset_sInf_of_within s ht h_bdd (h_Inf ht h_bdd)]

Premises used: subset_sInf_of_within
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddBelow t
⊢ IsGLB ((fun {x : (↑s : Type u_2)} ↦ (↑x : α)) '' t) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))

Tactic:
isGLB_csInf (ht.image _) ((Subtype.mono_coe _).map_bddBelow h_bdd)

Premises used: Subtype.mono_coe, isGLB_csInf, Set.Nonempty.image, Monotone.map_bddBelow
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddBelow t
⊢ IsGLB ((fun {x : (↑s : Type u_2)} ↦ (↑x : α)) '' t) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))

Tactic:
exact isGLB_csInf (ht.image _) ((Subtype.mono_coe _).map_bddBelow h_bdd)

Premises used: Subtype.mono_coe, isGLB_csInf, Set.Nonempty.image, Monotone.map_bddBelow
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : ¬BddAbove t
⊢ sSup t = sSup ∅

Tactic:
simp [ht]
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : ¬BddBelow t
⊢ sInf t = sInf ∅

Tactic:
simp [ht]
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddAbove t
⊢ ∃ (c : (↑s : Type u_2)), c ∈ t

Tactic:
ht

Premises used: Set.Nonempty
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddAbove t
obtain : ∀ (c : (↑s : Type u_2)) (hct : c ∈ t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s

Tactic:
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
h_bdd : BddAbove t
c : (↑s : Type u_2)
hct : c ∈ t
⊢ ∃ (B : (↑s : Type u_2)), B ∈ upperBounds t

Tactic:
h_bdd

Premises used: BddAbove, Set.Nonempty
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
h_bdd : BddAbove t
c : (↑s : Type u_2)
hct : c ∈ t
obtain : ∀ (B : (↑s : Type u_2)) (hB : B ∈ upperBounds t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s

Tactic:
obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd

Premises used: upperBounds
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s

Tactic:
hs.out c.2 B.2 ⟨?_, ?_⟩

Premises used: Set.OrdConnected.out, And.intro, Subtype.property
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ upperBounds t
refine_1 : (↑c : α) ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
refine_2 : sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ≤ (↑B : α)
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s

Tactic:
refine hs.out c.2 B.2 ⟨?_, ?_⟩

Premises used: Set.OrdConnected.out, And.intro, Subtype.property
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ upperBounds t
⊢ (↑c : α) ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
(Subtype.mono_coe (· ∈ s)).le_csSup_image hct ⟨B, hB⟩

Premises used: Membership.mem, Monotone.le_csSup_image, Subtype.mono_coe, Exists.intro
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ upperBounds t
⊢ (↑c : α) ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
exact (Subtype.mono_coe (· ∈ s)).le_csSup_image hct ⟨B, hB⟩

Premises used: Membership.mem, Monotone.le_csSup_image, Subtype.mono_coe, Exists.intro
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ≤ (↑B : α)

Tactic:
(Subtype.mono_coe (· ∈ s)).csSup_image_le ⟨c, hct⟩ hB

Premises used: Membership.mem, Subtype.mono_coe, Exists.intro, Monotone.csSup_image_le
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ≤ (↑B : α)

Tactic:
exact (Subtype.mono_coe (· ∈ s)).csSup_image_le ⟨c, hct⟩ hB

Premises used: Membership.mem, Subtype.mono_coe, Exists.intro, Monotone.csSup_image_le
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddBelow t
⊢ ∃ (c : (↑s : Type u_2)), c ∈ t

Tactic:
ht

Premises used: Set.Nonempty
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddBelow t
obtain : ∀ (c : (↑s : Type u_2)) (hct : c ∈ t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s

Tactic:
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
h_bdd : BddBelow t
c : (↑s : Type u_2)
hct : c ∈ t
⊢ ∃ (B : (↑s : Type u_2)), B ∈ lowerBounds t

Tactic:
h_bdd

Premises used: Set.Nonempty, BddBelow
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
h_bdd : BddBelow t
c : (↑s : Type u_2)
hct : c ∈ t
obtain : ∀ (B : (↑s : Type u_2)) (hB : B ∈ lowerBounds t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s

Tactic:
obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd

Premises used: lowerBounds
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s

Tactic:
hs.out B.2 c.2 ⟨?_, ?_⟩

Premises used: Set.OrdConnected.out, And.intro, Subtype.property
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ lowerBounds t
refine_1 : (↑B : α) ≤ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
refine_2 : sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ≤ (↑c : α)
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s

Tactic:
refine hs.out B.2 c.2 ⟨?_, ?_⟩

Premises used: Set.OrdConnected.out, And.intro, Subtype.property
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ lowerBounds t
⊢ (↑B : α) ≤ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
(Subtype.mono_coe (· ∈ s)).le_csInf_image ⟨c, hct⟩ hB

Premises used: Membership.mem, Subtype.mono_coe, Exists.intro, Monotone.le_csInf_image
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ lowerBounds t
⊢ (↑B : α) ≤ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
exact (Subtype.mono_coe (· ∈ s)).le_csInf_image ⟨c, hct⟩ hB

Premises used: Membership.mem, Subtype.mono_coe, Exists.intro, Monotone.le_csInf_image
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ≤ (↑c : α)

Tactic:
(Subtype.mono_coe (· ∈ s)).csInf_image_le hct ⟨B, hB⟩

Premises used: Monotone.csInf_image_le, Membership.mem, Subtype.mono_coe, Exists.intro
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ≤ (↑c : α)

Tactic:
exact (Subtype.mono_coe (· ∈ s)).csInf_image_le hct ⟨B, hB⟩

Premises used: Monotone.csInf_image_le, Membership.mem, Subtype.mono_coe, Exists.intro
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : ¬S = ∅
⊢ S.Nonempty

Tactic:
rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS

Premises used: Classical.not_not, Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ∈ Icc a b

Tactic:
⟨?_, csSup_le (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.2)⟩

Premises used: Set.Mem, setOf, _private.0.Set.Icc.completeLattice.match_1, Eq.rec, LE.le, Set.Icc, And.right, Set.Nonempty.image, And.intro, Subtype.val, csSup_le, Subtype.property
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
refine : a ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ∈ Icc a b

Tactic:
refine ⟨?_, csSup_le (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.2)⟩
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
obtain : ∀ (c : (↑(Icc a b) : Type u_2)) (hc : c ∈ S), a ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)
⊢ a ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)

Tactic:
obtain ⟨c, hc⟩ := hS
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
c : (↑(Icc a b) : Type u_2)
hc : c ∈ S
⊢ a ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)

Tactic:
c.2.1.trans (le_csSup ⟨b, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.2⟩ ⟨c, hc, rfl⟩)

Premises used: _private.0.Set.Icc.completeLattice.match_1, Eq.rec, LE.le, And.right, And.left, And.intro, Exists.intro, LE.le.trans, le_csSup, rfl, Subtype.property
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
c : (↑(Icc a b) : Type u_2)
hc : c ∈ S
⊢ a ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)

Tactic:
exact c.2.1.trans (le_csSup ⟨b, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.2⟩ ⟨c, hc, rfl⟩)
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
pos : ∀ (hS : S = ∅), IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)
neg :
  ∀ (hS : ¬S = ∅),
    IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)
⊢ IsLUB S
    (if hS : S = ∅ then Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯
    else Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)

Tactic:
split_ifs with hS
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S = ∅
pos : IsLUB (α := (↑(Icc a b) : Type u_2)) ∅ (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)
⊢ IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)

Tactic:
subst hS
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
pos : Eq (α := (↑(Icc a b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯) ⊥
⊢ IsLUB (α := (↑(Icc a b) : Type u_2)) ∅ (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)

Tactic:
simp only [isLUB_empty_iff, isBot_iff_eq_bot]

Premises used: isBot_iff_eq_bot, isLUB_empty_iff
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
⊢ Eq (α := (↑(Icc a b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯) ⊥

Tactic:
rfl