awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
hg : IsCauSeq (α := ℚ) abs fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)
g : CauSeq ℚ abs :=
  Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) hg
y : ℝ
h : y ∈ upperBounds s
⊢ mk g ≤ y

Tactic:
mk_le_of_forall_le
        ⟨1, fun n n1 =>
          let ⟨x, xS, hx⟩ := hf₁ _ n1
          le_trans hx (h xS)⟩

Premises used: Real.mk_le_of_forall_le, Rat.cast, LE.le, Exists.intro, OfNat.ofNat, Subtype.val, _private.0.Real.exists_isLUB.match_2, le_trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
f : (d : ℕ) → ℤ
hf :
  ∀ (d : ℕ),
    Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} (f d) ∧
      ∀ (z : ℤ), Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z → z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)
hg : IsCauSeq (α := ℚ) abs fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)
g : CauSeq ℚ abs :=
  Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) hg
y : ℝ
h : y ∈ upperBounds s
⊢ mk g ≤ y

Tactic:
exact
      mk_le_of_forall_le
        ⟨1, fun n n1 =>
          let ⟨x, xS, hx⟩ := hf₁ _ n1
          le_trans hx (h xS)⟩

Premises used: Real.mk_le_of_forall_le, Rat.cast, LE.le, Exists.intro, OfNat.ofNat, Subtype.val, _private.0.Real.exists_isLUB.match_2, le_trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
⊢ (-s).Nonempty

Tactic:
have hne' : (-s).Nonempty := Set.nonempty_neg.mpr hne
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
⊢ BddAbove (-s)

Tactic:
have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hbdd
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
h : IsGLB s (-Classical.choose (p := IsLUB (-s)) ⋯)
⊢ ∃ (x : ℝ), IsGLB s x

Tactic:
use -Classical.choose (Real.exists_isLUB hne' hbdd')

Premises used: Classical.choose, Real.exists_isLUB
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
h : IsLUB (-s) (Classical.choose (p := IsLUB (-s)) ⋯)
⊢ IsGLB s (-Classical.choose (p := IsLUB (-s)) ⋯)

Tactic:
rw [← isLUB_neg]

Premises used: isLUB_neg
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsLUB (-s) (Classical.choose (p := IsLUB (-s)) ⋯)

Tactic:
Classical.choose_spec (Real.exists_isLUB hne' hbdd')

Premises used: Classical.choose_spec, Real.exists_isLUB
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsLUB (-s) (Classical.choose (p := IsLUB (-s)) ⋯)

Tactic:
exact Classical.choose_spec (Real.exists_isLUB hne' hbdd')

Premises used: Classical.choose_spec, Real.exists_isLUB
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
⊢ sSup s = if h : s.Nonempty ∧ BddAbove s then Classical.choose (p := IsLUB s) ⋯ else 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
simp : IsLUB s (Classical.choose (p := IsLUB s) ⋯)
⊢ IsLUB s (sSup s)

Tactic:
simp only [sSup_def, dif_pos (And.intro h₁ h₂)]

Premises used: dif_pos, And.intro, Real.sSup_def
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ IsLUB s (Classical.choose (p := IsLUB s) ⋯)

Tactic:
apply Classical.choose_spec

Premises used: Classical.choose_spec
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
⊢ sInf s = -sSup (-s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
rw : IsLUB (-s) (sSup (-s))
⊢ IsGLB s (sInf s)

Tactic:
rw [sInf_def, ← isLUB_neg', neg_neg]

Premises used: isLUB_neg', neg_neg, Real.sInf_def
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsLUB (-s) (sSup (-s))

Tactic:
Real.isLUB_sSup h₁.neg h₂.neg

Premises used: BddBelow.neg, Set.Nonempty.neg, Real.isLUB_sSup
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsLUB (-s) (sSup (-s))

Tactic:
exact Real.isLUB_sSup h₁.neg h₂.neg

Premises used: BddBelow.neg, Set.Nonempty.neg, Real.isLUB_sSup
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
s_1 : Set ℝ
a : ℝ
s : Set ℝ
hs : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
simp [hs, sSup_def]

Premises used: Real.sSup_def
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
s_1 : Set ℝ
a : ℝ
s : Set ℝ
hs : ¬BddBelow s
⊢ sInf s = sInf ∅

Tactic:
simp [hs, sInf_def, sSup_def]

Premises used: Real.sSup_def, Real.sInf_def
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h : s.Nonempty
ε : ℝ
hε : 0 < ε
⊢ ∃ a ∈ s, a < sInf s + ε

Tactic:
exists_lt_of_csInf_lt h <| lt_add_of_pos_right _ hε

Premises used: lt_add_of_pos_right, exists_lt_of_csInf_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
h : s.Nonempty
ε : ℝ
hε : ε < 0
⊢ ∃ a ∈ s, sSup s + ε < a

Tactic:
exists_lt_of_lt_csSup h <| add_lt_iff_neg_left.2 hε

Premises used: Iff.mpr, add_lt_iff_neg_left, exists_lt_of_lt_csSup
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
rw : (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
⊢ sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

Tactic:
rw [le_iff_forall_pos_lt_add]

Premises used: le_iff_forall_pos_lt_add
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
mp : (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) → ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
mpr : (∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε) → ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

Tactic:
constructor
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε

Tactic:
exists_lt_of_csInf_lt h' (H ε ε_pos)

Premises used: exists_lt_of_csInf_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε

Tactic:
exact exists_lt_of_csInf_lt h' (H ε ε_pos)

Premises used: exists_lt_of_csInf_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
mpr : ∀ (x : ℝ) (x_in : x ∈ s) (hx : x < a + ε), sInf s < a + ε
⊢ sInf s < a + ε

Tactic:
rcases H ε ε_pos with ⟨x, x_in, hx⟩
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : x < a + ε
⊢ sInf s < a + ε

Tactic:
csInf_lt_of_lt h x_in hx

Premises used: csInf_lt_of_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : x < a + ε
⊢ sInf s < a + ε

Tactic:
exact csInf_lt_of_lt h x_in hx

Premises used: csInf_lt_of_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
rw : (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x
⊢ a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

Tactic:
rw [le_iff_forall_pos_lt_add]

Premises used: le_iff_forall_pos_lt_add
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

Tactic:
⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
refine_1 : ∀ (H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε) (ε : ℝ) (ε_neg : ε < 0), ∃ x ∈ s, a + ε < x
refine_2 : ∀ (H : ∀ ε < 0, ∃ x ∈ s, a + ε < x) (ε : ℝ) (ε_pos : 0 < ε), a < sSup s + ε
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

Tactic:
refine ⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x ∈ s, a + ε < x

Tactic:
exists_lt_of_lt_csSup h' (lt_sub_iff_add_lt.mp (H _ (neg_pos.mpr ε_neg)))

Premises used: Iff.mpr, neg_pos, exists_lt_of_lt_csSup, Iff.mp, lt_sub_iff_add_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε
ε : ℝ
ε_neg : ε < 0
⊢ ∃ x ∈ s, a + ε < x

Tactic:
exact exists_lt_of_lt_csSup h' (lt_sub_iff_add_lt.mp (H _ (neg_pos.mpr ε_neg)))

Premises used: Iff.mpr, neg_pos, exists_lt_of_lt_csSup, Iff.mp, lt_sub_iff_add_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
refine_2 : ∀ (x : ℝ) (x_in : x ∈ s) (hx : a + -ε < x), a < sSup s + ε
⊢ a < sSup s + ε

Tactic:
rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩

Premises used: Iff.mpr, neg_lt_zero
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : a + -ε < x
⊢ a < sSup s + ε

Tactic:
sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)

Premises used: Iff.mp, lt_csSup_of_lt, sub_lt_iff_lt_add
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : a + -ε < x
⊢ a < sSup s + ε

Tactic:
exact sub_lt_iff_lt_add.mp (lt_csSup_of_lt h x_in hx)

Premises used: Iff.mp, lt_csSup_of_lt, sub_lt_iff_lt_add
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ ¬(Set.Nonempty (α := ℝ) ∅ ∧ BddAbove (α := ℝ) ∅)

Tactic:
simp
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ Eq (α := ℝ) (sInf Set.univ) 0

Tactic:
simp [sInf_def]

Premises used: Real.sInf_def
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ
⊢ Eq (α := ℝ) (sSup ∅) 0

Tactic:
Real.sSup_empty

Premises used: Real.sSup_empty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ
h : Eq (α := Set ℝ) (Set.range fun (i : ι) ↦ f i) ∅
⊢ Eq (α := ℝ) (sSup (Set.range fun (i : ι) ↦ f i)) 0

Tactic:
convert! Real.sSup_empty

Premises used: Real.sSup_empty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ
h : IsEmpty ι
⊢ Eq (α := Set ℝ) (Set.range fun (i : ι) ↦ f i) ∅

Tactic:
rw [Set.range_eq_empty_iff]

Premises used: Set.range_eq_empty_iff
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ
⊢ IsEmpty ι

Tactic:
infer_instance
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
inl : IsEmpty ι → Eq (α := ℝ) (⨆ (x : ι), 0) 0
inr : Nonempty ι → Eq (α := ℝ) (⨆ (x : ι), 0) 0
⊢ Eq (α := ℝ) (⨆ (x : ι), 0) 0

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
h : IsEmpty ι
⊢ Eq (α := ℝ) (⨆ (x : ι), 0) 0

Tactic:
Real.iSup_of_isEmpty _

Premises used: Real.iSup_of_isEmpty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
h : IsEmpty ι
⊢ Eq (α := ℝ) (⨆ (x : ι), 0) 0

Tactic:
exact Real.iSup_of_isEmpty _

Premises used: Real.iSup_of_isEmpty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
h : Nonempty ι
⊢ Eq (α := ℝ) (⨆ (x : ι), 0) 0

Tactic:
ciSup_const

Premises used: ciSup_const
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
h : Nonempty ι
⊢ Eq (α := ℝ) (⨆ (x : ι), 0) 0

Tactic:
exact ciSup_const

Premises used: ciSup_const
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
dif_neg fun h => hs h.2

Premises used: dif_neg
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
hf : ¬BddAbove (Set.range f)
⊢ Eq (α := ℝ) (⨆ (i : ι), f i) 0

Tactic:
sSup_of_not_bddAbove hf

Premises used: iSup, Real.sSup_of_not_bddAbove
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ Eq (α := ℝ) (sSup Set.univ) 0

Tactic:
Real.sSup_of_not_bddAbove not_bddAbove_univ

Premises used: not_bddAbove_univ, Real.sSup_of_not_bddAbove
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ Eq (α := ℝ) (sInf ∅) 0

Tactic:
simp [sInf_def, sSup_empty]

Premises used: Real.sSup_empty, Real.sInf_def
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ
rw : Eq (α := ℝ) (sInf ∅) 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) (⨅ (i : ι), f i) 0

Tactic:
rw [iInf_of_isEmpty, sInf_empty]

Premises used: Real.iInf_of_isEmpty, Real.sInf_empty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
inl : IsEmpty ι → Eq (α := ℝ) (⨅ (x : ι), 0) 0
inr : Nonempty ι → Eq (α := ℝ) (⨅ (x : ι), 0) 0
⊢ Eq (α := ℝ) (⨅ (x : ι), 0) 0

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
h : IsEmpty ι
⊢ Eq (α := ℝ) (⨅ (x : ι), 0) 0

Tactic:
Real.iInf_of_isEmpty _

Premises used: Real.iInf_of_isEmpty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
h : IsEmpty ι
⊢ Eq (α := ℝ) (⨅ (x : ι), 0) 0

Tactic:
exact Real.iInf_of_isEmpty _

Premises used: Real.iInf_of_isEmpty
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
h : Nonempty ι
⊢ Eq (α := ℝ) (⨅ (x : ι), 0) 0

Tactic:
ciInf_const

Premises used: ciInf_const
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
h : Nonempty ι
⊢ Eq (α := ℝ) (⨅ (x : ι), 0) 0

Tactic:
exact ciInf_const

Premises used: ciInf_const
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ¬BddBelow s
⊢ sInf s = 0

Tactic:
neg_eq_zero.2 <| sSup_of_not_bddAbove <| mt bddAbove_neg.1 hs

Premises used: Iff.mpr, bddAbove_neg, mt, neg_eq_zero, Iff.mp, Real.sSup_of_not_bddAbove
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
hf : ¬BddBelow (Set.range f)
⊢ Eq (α := ℝ) (⨅ (i : ι), f i) 0

Tactic:
sInf_of_not_bddBelow hf

Premises used: iInf, Real.sInf_of_not_bddBelow
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
inl : Eq (α := ℝ) (sSup (-∅)) (-sInf ∅)
inr : ∀ (hn : s.Nonempty), sSup (-s) = -sInf s
⊢ sSup (-s) = -sInf s

Tactic:
obtain rfl | hn := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Archimedean
Goal:
⊢ Eq (α := ℝ) (sSup (-∅)) (-sInf ∅)

Tactic:
simp
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hn : s.Nonempty
pos : ∀ (hb : BddBelow s), sSup (-s) = -sInf s
neg : ∀ (hb : ¬BddBelow s), sSup (-s) = -sInf s
⊢ sSup (-s) = -sInf s

Tactic:
by_cases hb : BddBelow s

Premises used: BddBelow
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hn : s.Nonempty
hb : BddBelow s
pos pos₁ : -sInf s = -sInf s
⊢ sSup (-s) = -sInf s

Tactic:
rw [csSup_neg hn hb]

Premises used: csSup_neg
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
neg : sSup (-s) = -sInf ∅
neg₁ : sSup (-s) = -0
neg₂ : Eq (α := ℝ) (sSup ∅) (-0)
neg₃ : Eq (α := ℝ) 0 (-0)
neg₄ neg₅ : Eq (α := ℝ) 0 0
⊢ sSup (-s) = -sInf s

Tactic:
rw [csInf_of_not_bddBelow hb, Real.sInf_empty, csSup_of_not_bddAbove (bddAbove_neg.not.2 hb),
      Real.sSup_empty, neg_zero]

Premises used: Iff.mpr, csInf_of_not_bddBelow, Real.sSup_empty, bddAbove_neg, Iff.not, csSup_of_not_bddAbove, Real.sInf_empty, neg_zero
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
rw : -sInf (-s) = sSup s
rw₁ : sSup (- -s) = sSup s
rw₂ rw₃ : sSup s = sSup s
⊢ sInf (-s) = -sSup s

Tactic:
rw [← neg_eq_iff_eq_neg, ← Real.sSup_neg, neg_neg]

Premises used: neg_neg, neg_eq_iff_eq_neg, Real.sSup_neg
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ a), sSup ∅ ≤ a
inr : ∀ (hs' : s.Nonempty), sSup s ≤ a
⊢ sSup s ≤ a

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 0 ≤ a
hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ a
⊢ sSup ∅ ≤ a

Tactic:
sSup_empty.trans_le ha

Premises used: Real.sSup_empty, Eq.trans_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
hs' : s.Nonempty
⊢ sSup s ≤ a

Tactic:
csSup_le hs' hs

Premises used: csSup_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : 0 ≤ a
hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ a
⊢ sSup ∅ ≤ a

Tactic:
exacts [sSup_empty.trans_le ha, csSup_le hs' hs]

Premises used: Real.sSup_empty, Eq.trans_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
a : ℝ
hf : ∀ (i : ι), f i ≤ a
ha : 0 ≤ a
⊢ ⨆ (i : ι), f i ≤ a

Tactic:
Real.sSup_le (Set.forall_mem_range.2 hf) ha

Premises used: Iff.mpr, Set.forall_mem_range, iSup, Real.sSup_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → a ≤ x), a ≤ sInf ∅
inr : ∀ (hs' : s.Nonempty), a ≤ sInf s
⊢ a ≤ sInf s

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : a ≤ 0
hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → a ≤ x
⊢ a ≤ sInf ∅

Tactic:
ha.trans_eq sInf_empty.symm

Premises used: LE.le.trans_eq, Real.sInf_empty, Eq.symm
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
hs' : s.Nonempty
⊢ a ≤ sInf s

Tactic:
le_csInf hs' hs

Premises used: le_csInf
-- Module: Mathlib.Data.Real.Archimedean
Goal:
a : ℝ
ha : a ≤ 0
hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → a ≤ x
⊢ a ≤ sInf ∅

Tactic:
exacts [ha.trans_eq sInf_empty.symm, le_csInf hs' hs]

Premises used: LE.le.trans_eq, Real.sInf_empty, Eq.symm
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
a : ℝ
hf : ∀ (i : ι), a ≤ f i
ha : a ≤ 0
⊢ a ≤ ⨅ (i : ι), f i

Tactic:
Real.le_sInf (Set.forall_mem_range.2 hf) ha

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Real.le_sInf
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
⊢ sSup s ≤ 0

Tactic:
Real.sSup_le hs le_rfl

Premises used: le_rfl, Real.sSup_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
hf : ∀ (i : ι), f i ≤ 0
⊢ LE.le (α := ℝ) (⨆ (i : ι), f i) 0

Tactic:
Real.iSup_le hf le_rfl

Premises used: le_rfl, Real.iSup_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
⊢ 0 ≤ sInf s

Tactic:
Real.le_sInf hs le_rfl

Premises used: le_rfl, Real.le_sInf
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ iInf f

Tactic:
Real.le_iInf hf le_rfl

Premises used: le_rfl, Real.le_iInf
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∃ x ∈ s, 0 ≤ x
obtain : ∀ (x : ℝ) (hxs : x ∈ s) (hx : 0 ≤ x), 0 ≤ sSup s
⊢ 0 ≤ sSup s

Tactic:
obtain ⟨x, hxs, hx⟩ := hs
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
x : ℝ
hxs : x ∈ s
hx : 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
dite _ (fun h ↦ le_csSup_of_le h hxs hx) fun h ↦ (sSup_of_not_bddAbove h).ge

Premises used: Eq.ge, dite, le_csSup_of_le, Real.sSup_of_not_bddAbove
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
x : ℝ
hxs : x ∈ s
hx : 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
exact dite _ (fun h ↦ le_csSup_of_le h hxs hx) fun h ↦ (sSup_of_not_bddAbove h).ge

Premises used: Eq.ge, dite, le_csSup_of_le, Real.sSup_of_not_bddAbove
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∃ x ∈ s, 0 ≤ x
obtain : ∀ (x : ℝ) (hxs : x ∈ s) (hx : 0 ≤ x), 0 ≤ sSup s
⊢ 0 ≤ sSup s

Tactic:
classical
  obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ le_csSup_of_le h hxs hx) fun h ↦ (sSup_of_not_bddAbove h).ge
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
hf : ∃ (i : ι), 0 ≤ f i
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), f i)

Tactic:
sSup_nonneg' <| Set.exists_range_iff.2 hf

Premises used: Iff.mpr, iSup, Set.exists_range_iff, Real.sSup_nonneg'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
obtain : ∀ (x : ℝ) (hxs : x ∈ s) (hx : x ≤ 0), sInf s ≤ 0
⊢ sInf s ≤ 0

Tactic:
obtain ⟨x, hxs, hx⟩ := hs
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
x : ℝ
hxs : x ∈ s
hx : x ≤ 0
⊢ sInf s ≤ 0

Tactic:
dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le

Premises used: Real.sInf_of_not_bddBelow, csInf_le_of_le, Eq.le, dite
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
x : ℝ
hxs : x ∈ s
hx : x ≤ 0
⊢ sInf s ≤ 0

Tactic:
exact dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le

Premises used: Real.sInf_of_not_bddBelow, csInf_le_of_le, Eq.le, dite
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
obtain : ∀ (x : ℝ) (hxs : x ∈ s) (hx : x ≤ 0), sInf s ≤ 0
⊢ sInf s ≤ 0

Tactic:
classical
  obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
hf : ∃ (i : ι), f i ≤ 0
⊢ LE.le (α := ℝ) (⨅ (i : ι), f i) 0

Tactic:
sInf_nonpos' <| Set.exists_range_iff.2 hf

Premises used: Iff.mpr, iInf, Set.exists_range_iff, Real.sInf_nonpos'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → 0 ≤ x), LE.le (α := ℝ) 0 (sSup ∅)
inr : ∀ (x : ℝ) (hx : x ∈ s), 0 ≤ sSup s
⊢ 0 ≤ sSup s

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Archimedean
Goal:
hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → 0 ≤ x
⊢ LE.le (α := ℝ) 0 (sSup ∅)

Tactic:
sSup_empty.ge

Premises used: Real.sSup_empty, Eq.ge
-- Module: Mathlib.Data.Real.Archimedean
Goal:
hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → 0 ≤ x
⊢ LE.le (α := ℝ) 0 (sSup ∅)

Tactic:
exact sSup_empty.ge

Premises used: Real.sSup_empty, Eq.ge
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s

Tactic:
sSup_nonneg' ⟨x, hx, hs _ hx⟩

Premises used: And.intro, Exists.intro, Real.sSup_nonneg'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s

Tactic:
exact sSup_nonneg' ⟨x, hx, hs _ hx⟩

Premises used: And.intro, Exists.intro, Real.sSup_nonneg'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), f i)

Tactic:
sSup_nonneg <| Set.forall_mem_range.2 hf

Premises used: Iff.mpr, Set.forall_mem_range, iSup, Real.sSup_nonneg
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Type u_2
F : Type u_3
α : Type u_4
inst : FunLike F α ℝ
inst_1 : NonnegHomClass F α ℝ
f : F
g : ι → α
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), (f : (a : α) → ℝ) (g i))

Tactic:
iSup_nonneg (fun i ↦ apply_nonneg f (g i))

Premises used: NonnegHomClass.apply_nonneg, Real.iSup_nonneg
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ 0), LE.le (α := ℝ) (sInf ∅) 0
inr : ∀ (x : ℝ) (hx : x ∈ s), sInf s ≤ 0
⊢ sInf s ≤ 0

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Real.Archimedean
Goal:
hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ 0
⊢ LE.le (α := ℝ) (sInf ∅) 0

Tactic:
sInf_empty.le

Premises used: Eq.le, Real.sInf_empty