awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
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
x : ℝ
xS : x ∈ s
z : ℝ
xz : z < x
K : ℕ
hK : (x - z)⁻¹ < (↑K : ℝ)
⊢ z ≤ mk g
have refine_1 : ∀ (n : ℕ) (nK : n ≥ K), z ≤ (↑((↑g : ℕ → ℚ) n) : ℝ)
Tactic: refine le_mk_of_forall_le ⟨K, fun n nK => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
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
x : ℝ
xS : x ∈ s
z : ℝ
xz : z < x
K : ℕ
hK : (x - z)⁻¹ < (↑K : ℝ)
n : ℕ
nK : n ≥ K
⊢ z ≤ (↑((↑g : ℕ → ℚ) n) : ℝ)
have xz₁ : 0 < x - z
Tactic: replace xz := sub_pos.2 xz
Cleared hypotheses: xz
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
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
x : ℝ
xS : x ∈ s
z : ℝ
K : ℕ
hK : (x - z)⁻¹ < (↑K : ℝ)
n : ℕ
nK : n ≥ K
xz : 0 < x - z
⊢ z ≤ (↑((↑g : ℕ → ℚ) n) : ℝ)
have hK₁ : (x - z)⁻¹ ≤ (↑n : ℝ)
Tactic: replace hK := hK.le.trans (Nat.cast_le.2 nK)
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
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
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ (↑n : ℝ)
⊢ z ≤ (↑((↑g : ℕ → ℚ) n) : ℝ)
have n0 : 0 < n
Tactic: have n0 : 0 < n := Nat.cast_pos.1 ((inv_pos.2 xz).trans_le hK)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
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
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ (↑n : ℝ)
n0 : 0 < n
⊢ z ≤ (↑((↑g : ℕ → ℚ) n) : ℝ)
have refine_1 : z ≤ x - (↑n : ℝ)⁻¹
Tactic: refine le_trans ?_ (hf₂ _ n0 _ xS).le
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
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
x : ℝ
xS : x ∈ s
z : ℝ
K n : ℕ
nK : n ≥ K
xz : 0 < x - z
hK : (x - z)⁻¹ ≤ (↑n : ℝ)
n0 : 0 < n
⊢ z ≤ x - (↑n : ℝ)⁻¹
have refine_1 : (↑n : ℝ)⁻¹ ≤ x - z
Tactic: rwa [le_sub_comm, inv_le_comm₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _) xz]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
⊢ ∃ (x : ℝ), IsGLB s x
have hne' : (-s).Nonempty
Tactic: have hne' : (-s).Nonempty := Set.nonempty_neg.mpr hne
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
⊢ ∃ (x : ℝ), IsGLB s x
have hbdd' : BddAbove (-s)
Tactic: have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hbdd
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ ∃ (x : ℝ), IsGLB s x
have h : IsGLB s (-Classical.choose (p := IsLUB (-s)) sorry)
Tactic: use -Classical.choose (Real.exists_isLUB hne' hbdd')
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsGLB s (-Classical.choose (p := IsLUB (-s)) ⋯)
have h : IsLUB (-s) (Classical.choose (p := IsLUB (-s)) sorry)
Tactic: rw [← isLUB_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ IsLUB s (sSup s)
have simp : IsLUB s (Classical.choose (p := IsLUB s) sorry)
Tactic: simp only [sSup_def, dif_pos (And.intro h₁ h₂)]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsGLB s (sInf s)
have rw : IsLUB (-s) (sSup (-s))
Tactic: rw [sInf_def, ← isLUB_neg', neg_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
have rw : (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
Tactic: rw [le_iff_forall_pos_lt_add]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
have mp : (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) → ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
mp : (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) → ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
have mpr : (∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε) → ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε
have mpr : ∀ (x : ℝ) (x_in : x ∈ s) (hx : x < a + ε), sInf s < a + ε
Tactic: rcases H ε ε_pos with ⟨x, x_in, hx⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
⊢ a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x
have rw : (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x
Tactic: rw [le_iff_forall_pos_lt_add]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x
have refine_1 : ∀ (H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε) (ε : ℝ) (ε_neg : ε < 0), ∃ x ∈ s, a + ε < x
Tactic: refine ⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
refine_1 : ∀ (H : ∀ (ε : ℝ), 0 < ε → a < sSup s + ε) (ε : ℝ) (ε_neg : ε < 0), ∃ x ∈ s, a + ε < x
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x
have refine_2 : ∀ (H : ∀ ε < 0, ∃ x ∈ s, a + ε < x) (ε : ℝ) (ε_pos : 0 < ε), a < sSup s + ε
Tactic: refine ⟨fun H ε ε_neg => ?_, fun H ε ε_pos => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
H : ∀ ε < 0, ∃ x ∈ s, a + ε < x
ε : ℝ
ε_pos : 0 < ε
⊢ a < sSup s + ε
have refine_2 : ∀ (x : ℝ) (x_in : x ∈ s) (hx : a + -ε < x), a < sSup s + ε
Tactic: rcases H _ (neg_lt_zero.mpr ε_pos) with ⟨x, x_in, hx⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ
⊢ Eq (α := ℝ) (sSup (Set.range fun (i : ι) ↦ f i)) 0
have h : Eq (α := Set ℝ) (Set.range fun (i : ι) ↦ f i) ∅
Tactic: convert! Real.sSup_empty
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
ι : Sort u_1
⊢ Eq (α := ℝ) (⨆ (x : ι), 0) 0
have inl : IsEmpty ι → Eq (α := ℝ) (⨆ (x : ι), 0) 0
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
ι : Sort u_1
inl : IsEmpty ι → Eq (α := ℝ) (⨆ (x : ι), 0) 0
⊢ Eq (α := ℝ) (⨆ (x : ι), 0) 0
have inr : Nonempty ι → Eq (α := ℝ) (⨆ (x : ι), 0) 0
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ
⊢ Eq (α := ℝ) (⨅ (i : ι), f i) 0
have rw : Eq (α := ℝ) (sInf ∅) 0
Tactic: rw [iInf_of_isEmpty, sInf_empty]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ
rw : Eq (α := ℝ) (sInf ∅) 0
⊢ Eq (α := ℝ) (⨅ (i : ι), f i) 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [iInf_of_isEmpty, sInf_empty]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
ι : Sort u_1
⊢ Eq (α := ℝ) (⨅ (x : ι), 0) 0
have inl : IsEmpty ι → Eq (α := ℝ) (⨅ (x : ι), 0) 0
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
ι : Sort u_1
inl : IsEmpty ι → Eq (α := ℝ) (⨅ (x : ι), 0) 0
⊢ Eq (α := ℝ) (⨅ (x : ι), 0) 0
have inr : Nonempty ι → Eq (α := ℝ) (⨅ (x : ι), 0) 0
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
⊢ sSup (-s) = -sInf s
have inl : Eq (α := ℝ) (sSup (-∅)) (-sInf ∅)
Tactic: obtain rfl | hn := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
inl : Eq (α := ℝ) (sSup (-∅)) (-sInf ∅)
⊢ sSup (-s) = -sInf s
have inr : ∀ (hn : s.Nonempty), sSup (-s) = -sInf s
Tactic: obtain rfl | hn := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hn : s.Nonempty
⊢ sSup (-s) = -sInf s
have pos : ∀ (hb : BddBelow s), sSup (-s) = -sInf s
Tactic: by_cases hb : BddBelow s
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hn : s.Nonempty
pos : ∀ (hb : BddBelow s), sSup (-s) = -sInf s
⊢ sSup (-s) = -sInf s
have neg : ∀ (hb : ¬BddBelow s), sSup (-s) = -sInf s
Tactic: by_cases hb : BddBelow s
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hn : s.Nonempty
hb : BddBelow s
⊢ sSup (-s) = -sInf s
have pos : -sInf s = -sInf s
Tactic: rw [csSup_neg hn hb]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s
have neg : sSup (-s) = -sInf ∅
Tactic: rw [csInf_of_not_bddBelow hb, Real.sInf_empty, csSup_of_not_bddAbove (bddAbove_neg.not.2 hb),
      Real.sSup_empty, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
neg : sSup (-s) = -sInf ∅
⊢ sSup (-s) = -sInf s
have neg₁ : sSup (-s) = -0
Tactic: rw [csInf_of_not_bddBelow hb, Real.sInf_empty, csSup_of_not_bddAbove (bddAbove_neg.not.2 hb),
      Real.sSup_empty, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
neg : sSup (-s) = -sInf ∅
neg₁ : sSup (-s) = -0
⊢ sSup (-s) = -sInf s
have neg₂ : Eq (α := ℝ) (sSup ∅) (-0)
Tactic: rw [csInf_of_not_bddBelow hb, Real.sInf_empty, csSup_of_not_bddAbove (bddAbove_neg.not.2 hb),
      Real.sSup_empty, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
neg : sSup (-s) = -sInf ∅
neg₁ : sSup (-s) = -0
neg₂ : Eq (α := ℝ) (sSup ∅) (-0)
⊢ sSup (-s) = -sInf s
have neg₃ : Eq (α := ℝ) 0 (-0)
Tactic: rw [csInf_of_not_bddBelow hb, Real.sInf_empty, csSup_of_not_bddAbove (bddAbove_neg.not.2 hb),
      Real.sSup_empty, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
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)
⊢ sSup (-s) = -sInf s
have neg₄ : Eq (α := ℝ) 0 0
Tactic: rw [csInf_of_not_bddBelow hb, Real.sInf_empty, csSup_of_not_bddAbove (bddAbove_neg.not.2 hb),
      Real.sSup_empty, neg_zero]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
⊢ sInf (-s) = -sSup s
have rw : -sInf (-s) = sSup s
Tactic: rw [← neg_eq_iff_eq_neg, ← Real.sSup_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
rw : -sInf (-s) = sSup s
⊢ sInf (-s) = -sSup s
have rw₁ : sSup (- -s) = sSup s
Tactic: rw [← neg_eq_iff_eq_neg, ← Real.sSup_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
rw : -sInf (-s) = sSup s
rw₁ : sSup (- -s) = sSup s
⊢ sInf (-s) = -sSup s
have rw₂ : sSup s = sSup s
Tactic: rw [← neg_eq_iff_eq_neg, ← Real.sSup_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
⊢ sSup s ≤ a
have inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ a), sSup ∅ ≤ a
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ a), sSup ∅ ≤ a
⊢ sSup s ≤ a
have inr : ∀ (hs' : s.Nonempty), sSup s ≤ a
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
⊢ a ≤ sInf s
have inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → a ≤ x), a ≤ sInf ∅
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, a ≤ x
ha : a ≤ 0
inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → a ≤ x), a ≤ sInf ∅
⊢ a ≤ sInf s
have inr : ∀ (hs' : s.Nonempty), a ≤ sInf s
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hs : ∃ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s
have obtain : ∀ (x : ℝ) (hxs : x ∈ s) (hx : 0 ≤ x), 0 ≤ sSup s
Tactic: obtain ⟨x, hxs, hx⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hs : ∃ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s
have obtain : ∀ (x : ℝ) (hxs : x ∈ s) (hx : 0 ≤ x), 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0
have obtain : ∀ (x : ℝ) (hxs : x ∈ s) (hx : x ≤ 0), sInf s ≤ 0
Tactic: obtain ⟨x, hxs, hx⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0
have obtain : ∀ (x : ℝ) (hxs : x ∈ s) (hx : x ≤ 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s
have inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → 0 ≤ x), LE.le (α := ℝ) 0 (sSup ∅)
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → 0 ≤ x), LE.le (α := ℝ) 0 (sSup ∅)
⊢ 0 ≤ sSup s
have inr : ∀ (x : ℝ) (hx : x ∈ s), 0 ≤ sSup s
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0
have inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ 0), LE.le (α := ℝ) (sInf ∅) 0
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
inl : ∀ (hs : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ∅ x → x ≤ 0), LE.le (α := ℝ) (sInf ∅) 0
⊢ sInf s ≤ 0
have inr : ∀ (x : ℝ) (hx : x ∈ s), sInf s ≤ 0
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
⊢ sInf s ≤ sSup s
have inl : ∀ (h₁ : BddBelow (α := ℝ) ∅) (h₂ : BddAbove (α := ℝ) ∅), LE.le (α := ℝ) (sInf ∅) (sSup ∅)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
Cleared hypotheses: s, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
inl : ∀ (h₁ : BddBelow (α := ℝ) ∅) (h₂ : BddAbove (α := ℝ) ∅), LE.le (α := ℝ) (sInf ∅) (sSup ∅)
⊢ sInf s ≤ sSup s
have inr : ∀ (hne : s.Nonempty), sInf s ≤ sSup s
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
h₁ : BddBelow (α := ℝ) ∅
h₂ : BddAbove (α := ℝ) ∅
⊢ LE.le (α := ℝ) (sInf ∅) (sSup ∅)
have inl : LE.le (α := ℝ) 0 (sSup ∅)
Tactic: rw [sInf_empty, sSup_empty]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
h₁ : BddBelow (α := ℝ) ∅
h₂ : BddAbove (α := ℝ) ∅
inl : LE.le (α := ℝ) 0 (sSup ∅)
⊢ LE.le (α := ℝ) (sInf ∅) (sSup ∅)
have inl₁ : LE.le (α := ℝ) 0 0
Tactic: rw [sInf_empty, sSup_empty]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
⊢ ∃ (x : ℝ), f ≈ const abs x
have lb : ∃ (x : ℝ), x ∈ s
Tactic: have lb : ∃ x, x ∈ s := exists_lt f
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
⊢ ∃ (x : ℝ), f ≈ const abs x
have ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
Tactic: have ub' : ∀ x, f < const abs x → ∀ y ∈ s, y ≤ x := fun x h y yS =>
    le_of_lt <| const_lt.1 <| CauSeq.lt_trans yS h
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (hypothesis)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
⊢ ∃ (x : ℝ), f ≈ const abs x
have ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
Tactic: have ub : ∃ x, ∀ y ∈ s, y ≤ x := (exists_gt f).imp ub'
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
⊢ ∃ (x : ℝ), f ≈ const abs x
have refine_1 : ∀ (h : f < const abs (sSup s)), False
Tactic: refine ⟨sSup s, ((lt_total _ _).resolve_left fun h => ?_).resolve_right fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
refine_1 : ∀ (h : f < const abs (sSup s)), False
⊢ ∃ (x : ℝ), f ≈ const abs x
have refine_2 : ∀ (h : const abs (sSup s) < f), False
Tactic: refine ⟨sSup s, ((lt_total _ _).resolve_left fun h => ?_).resolve_right fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
h : f < const abs (sSup s)
⊢ False
have refine_1 : ∀ (ε : ℝ) (ε0 : ε > 0) (i : ℕ) (ih : ∀ j ≥ i, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j), False
Tactic: rcases h with ⟨ε, ε0, i, ih⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
⊢ False
have refine_1 : f < const abs (sSup s - ε / 2)
Tactic: refine (csSup_le lb (ub' _ ?_)).not_gt (sub_lt_self _ (half_pos ε0))
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
⊢ f < const abs (sSup s - ε / 2)
have refine_1 : ∀ (j : ℕ) (ij : j ≥ i), ε / 2 ≤ (↑(const abs (sSup s - ε / 2) - f) : ℕ → ℝ) j
Tactic: refine ⟨_, half_pos ε0, i, fun j ij => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ (↑(const abs (sSup s) - f) : ℕ → ℝ) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ (↑(const abs (sSup s - ε / 2) - f) : ℕ → ℝ) j
have refine_1 : ε ≤ sSup s - (↑f : ℕ → ℝ) j
Tactic: rw [sub_apply, const_apply, sub_right_comm, le_sub_iff_add_le, add_halves]
-- Lean 4 proof step from Mathlib.Data.Real.Archimedean (goal)
Goal:
f : CauSeq ℝ abs
s : Set ℝ := {x : ℝ | const abs x < f}
lb : ∃ (x : ℝ), x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ (x : ℝ), ∀ y ∈ s, y ≤ x
h : const abs (sSup s) < f
⊢ False
have refine_2 : ∀ (ε : ℝ) (ε0 : ε > 0) (i : ℕ) (ih : ∀ j ≥ i, ε ≤ (↑(f - const abs (sSup s)) : ℕ → ℝ) j), False
Tactic: rcases h with ⟨ε, ε0, i, ih⟩
Cleared hypotheses: h