awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Sqrt
Goal:
n : ℕ
rw : sqrt (↑(↑n : ℤ) : ℚ) = (↑n.sqrt : ℚ)
rw₁ : Eq (α := ℚ) (↑(Int.sqrt (↑n : ℤ)) : ℚ) (↑n.sqrt : ℚ)
rw₂ : Eq (α := ℚ) (↑(↑n.sqrt : ℤ) : ℚ) (↑n.sqrt : ℚ)
rw₃ rw₄ : Eq (α := ℚ) (↑n.sqrt : ℚ) (↑n.sqrt : ℚ)
⊢ sqrt (↑n : ℚ) = (↑n.sqrt : ℚ)

Tactic:
rw [← Int.cast_natCast, sqrt_intCast, Int.sqrt_natCast, Int.cast_natCast]

Premises used: Int.cast_natCast, Rat.sqrt_intCast, Int.sqrt_natCast
-- Module: Mathlib.Data.Rat.Sqrt
Goal:
n : ℕ
⊢ sqrt (OfNat.ofNat n) = (↑(Nat.sqrt (OfNat.ofNat n)) : ℚ)

Tactic:
sqrt_natCast _

Premises used: Rat.sqrt_natCast
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
⊢ Eq (α := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) ⊤

Tactic:
(eq_top_iff' _).2 fun x ↦ ?_

Premises used: Iff.mpr, AddSubmonoid.eq_top_iff'
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
refine : ∀ (x : ℚ≥0), Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) x
⊢ Eq (α := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) ⊤

Tactic:
refine (eq_top_iff' _).2 fun x ↦ ?_

Premises used: Iff.mpr, AddSubmonoid.eq_top_iff'
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
rw :
  Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n))
    ((x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n)
⊢ Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) x

Tactic:
rw [this]
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
⊢ Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n))
    ((x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n)

Tactic:
nsmul_mem (subset_closure <| mem_range_self _) _

Premises used: Set.mem_range_self, AddSubmonoid.subset_closure, nsmul_mem
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
this : x = (x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
⊢ Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n))
    ((x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n)

Tactic:
exact nsmul_mem (subset_closure <| mem_range_self _) _

Premises used: Set.mem_range_self, AddSubmonoid.subset_closure, nsmul_mem
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
suffices : x = (x.num * x.den ^ (n - 1)) • HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
⊢ Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x ^ n)) x

Tactic:
suffices x = (x.num * x.den ^ (n - 1)) • (x.den : ℚ≥0)⁻¹ ^ n by
    rw [this]
    exact nsmul_mem (subset_closure <| mem_range_self _) _
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
push_cast : x = (↑x.num : ℚ≥0) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0) (n - 1) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n
⊢ x = (↑(x.num * x.den ^ (n - 1)) : ℚ≥0) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n

Tactic:
push_cast
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
rw ha : Ne (α := ℚ≥0) (↑x.den : ℚ≥0) 0
h : 1 ≤ n
⊢ x = (↑x.num : ℚ≥0) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0) (n - 1) * HPow.hPow (α := ℚ≥0) (↑x.den : ℚ≥0)⁻¹ n

Tactic:
rw [mul_assoc, pow_sub₀, pow_one, mul_right_comm, ← mul_pow, mul_inv_cancel₀, one_pow, one_mul,
    ← div_eq_mul_inv, num_div_den]

Premises used: one_pow, mul_inv_cancel₀, mul_assoc, div_eq_mul_inv, mul_right_comm, pow_one, pow_sub₀, mul_pow, one_mul, NNRat.num_div_den
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ Ne (α := ℚ≥0) (↑x.den : ℚ≥0) 0

Tactic:
simp [x.den_pos.ne', Nat.one_le_iff_ne_zero, *]

Premises used: LT.lt.ne', NNRat.den_pos, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
x : ℚ≥0
⊢ 1 ≤ n

Tactic:
simp [x.den_pos.ne', Nat.one_le_iff_ne_zero, *]

Premises used: LT.lt.ne', NNRat.den_pos, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Rat.Star
Goal:
⊢ Eq (α := AddSubmonoid ℚ≥0) (closure (range fun (x : ℚ≥0) ↦ x * x)) ⊤

Tactic:
simpa only [sq] using addSubmonoid_closure_range_pow two_ne_zero

Premises used: sq, NNRat.addSubmonoid_closure_range_pow, two_ne_zero
-- Module: Mathlib.Data.Rat.Star
Goal:
a b : ℚ≥0
⊢ a ≤ b ↔ ∃ (p : ℚ≥0), Membership.mem (γ := AddSubmonoid ℚ≥0) (closure (range fun (s : ℚ≥0) ↦ star s * s)) p ∧ b = a + p

Tactic:
simp [eq_comm, le_iff_exists_nonneg_add (a := a)]

Premises used: eq_comm, le_iff_exists_nonneg_add
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ Eq (α := AddSubmonoid ℚ) (closure (image (α := ℚ≥0) (⇑NNRat.coeHom : (a : ℚ≥0) → ℚ) (range fun (x : ℚ≥0) ↦ x ^ n)))
    (map NNRat.coeHom (closure (range fun (x : ℚ≥0) ↦ x ^ n)))

Tactic:
(AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm

Premises used: NNRat.coeHom, AddMonoidHom.map_mclosure, HPow.hPow, Set.range, Eq.symm
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
h :
  Eq (α := Set ℚ) (range fun (x : ℚ) ↦ x ^ n)
    (image (α := ℚ≥0) (⇑NNRat.coeHom : (a : ℚ≥0) → ℚ) (range fun (x : ℚ≥0) ↦ x ^ n))
h₁ : Eq (α := AddSubmonoid ℚ) (nonneg ℚ) (map NNRat.coeHom (closure (range fun (x : ℚ≥0) ↦ x ^ n)))
⊢ Eq (α := AddSubmonoid ℚ) (closure (range fun (x : ℚ) ↦ x ^ n)) (nonneg ℚ)

Tactic:
convert! (AddMonoidHom.map_mclosure NNRat.coeHom <| range fun x ↦ x ^ n).symm

Premises used: NNRat.coeHom, AddMonoidHom.map_mclosure, HPow.hPow, Set.range, Eq.symm
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
x : ℚ
⊢ HPow.hPow (α := ℚ) (↑(nnabs x) : ℚ) n = x ^ n

Tactic:
simp [hn.pow_abs]

Premises used: Even.pow_abs
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
⊢ ∀ (x : ℚ), ∃ (y : ℚ≥0), HPow.hPow (α := ℚ) (↑y : ℚ) n = x ^ n

Tactic:
have (x : ℚ) : ∃ y : ℚ≥0, y ^ n = x ^ n := ⟨x.nnabs, by simp [hn.pow_abs]⟩
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
this : ∀ (x : ℚ), ∃ (y : ℚ≥0), HPow.hPow (α := ℚ) (↑y : ℚ) n = x ^ n
⊢ Eq (α := Set ℚ) (range fun (x : ℚ) ↦ x ^ n)
    (image (α := ℚ≥0) (⇑NNRat.coeHom : (a : ℚ≥0) → ℚ) (range fun (x : ℚ≥0) ↦ x ^ n))

Tactic:
simp [subset_antisymm_iff, range_subset_iff, this]

Premises used: subset_antisymm_iff, Set.range_subset_iff
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
h :
  ∀ (x : ℚ),
    Membership.mem (γ := AddSubmonoid ℚ) (nonneg ℚ) x ↔
      Membership.mem (γ := AddSubmonoid ℚ) (map NNRat.coeHom (closure (range fun (x : ℚ≥0) ↦ x ^ n))) x
⊢ Eq (α := AddSubmonoid ℚ) (nonneg ℚ) (map NNRat.coeHom (closure (range fun (x : ℚ≥0) ↦ x ^ n)))

Tactic:
ext
-- Module: Mathlib.Data.Rat.Star
Goal:
n : ℕ
hn₀ : n ≠ 0
hn : Even n
x : ℚ
⊢ Membership.mem (γ := AddSubmonoid ℚ) (nonneg ℚ) x ↔
    Membership.mem (γ := AddSubmonoid ℚ) (map NNRat.coeHom (closure (range fun (x : ℚ≥0) ↦ x ^ n))) x

Tactic:
simp [NNRat.addSubmonoid_closure_range_pow hn₀, NNRat.exists]

Premises used: NNRat.addSubmonoid_closure_range_pow, NNRat.exists
-- Module: Mathlib.Data.Rat.Star
Goal:
⊢ Eq (α := AddSubmonoid ℚ) (closure (range fun (x : ℚ) ↦ x * x)) (nonneg ℚ)

Tactic:
simpa only [sq] using addSubmonoid_closure_range_pow two_ne_zero even_two

Premises used: even_two, Rat.addSubmonoid_closure_range_pow, sq, two_ne_zero
-- Module: Mathlib.Data.Rat.Star
Goal:
a b : ℚ
⊢ a ≤ b ↔ ∃ (p : ℚ), Membership.mem (γ := AddSubmonoid ℚ) (closure (range fun (s : ℚ) ↦ star s * s)) p ∧ b = a + p

Tactic:
simp [eq_comm, le_iff_exists_nonneg_add (a := a)]

Premises used: eq_comm, le_iff_exists_nonneg_add
-- Module: Mathlib.Data.Real.Archimedean
Goal:
ι : Sort u_1
f : ι → ℝ
s : Set ℝ
a : ℝ
⊢ Archimedean ℝ

Tactic:
archimedean_iff_rat_le.2 fun x =>
    Real.ind_mk x fun f =>
      let ⟨M, _, H⟩ := f.bounded' 0
      ⟨M, mk_le_of_forall_le ⟨0, fun i _ => Rat.cast_le.2 <| le_of_lt (abs_lt.1 (H i)).2⟩⟩

Premises used: Iff.mpr, archimedean_iff_rat_le, Real.ind_mk
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : (↑δ : ℝ) < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |HSub.hSub (α := ℝ) (↑(f j) : ℝ) (↑(f i) : ℝ)| < ε

Tactic:
lt_trans (mod_cast hi _ ij) δε

Premises used: lt_trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℕ → ℚ
H : IsCauSeq abs f
ε : ℝ
ε0 : ε > 0
δ : ℚ
δ0 : 0 < δ
δε : (↑δ : ℝ) < ε
i : ℕ
hi : ∀ j ≥ i, |f j - f i| < δ
j : ℕ
ij : j ≥ i
⊢ |HSub.hSub (α := ℝ) (↑(f j) : ℝ) (↑(f i) : ℝ)| < ε

Tactic:
exact lt_trans (mod_cast hi _ ij) δε

Premises used: lt_trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℕ → ℚ
H : IsCauSeq (α := ℝ) abs fun (i : ℕ) ↦ (↑(f i) : ℝ)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |HSub.hSub (α := ℝ) (↑(f j) : ℝ) (↑(f i) : ℝ)| < (↑ε : ℝ)
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε

Tactic:
mod_cast hi _ ij

Premises used: abs, congrArg, HSub.hSub, cast, Rat.cast, Rat.cast_sub._simp_1, LT.lt, congrFun', Rat.cast_lt._simp_1, Rat.cast_abs._simp_1, Eq.trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℕ → ℚ
H : IsCauSeq (α := ℝ) abs fun (i : ℕ) ↦ (↑(f i) : ℝ)
ε : ℚ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |HSub.hSub (α := ℝ) (↑(f j) : ℝ) (↑(f i) : ℝ)| < (↑ε : ℝ)
j : ℕ
ij : j ≥ i
⊢ |f j - f i| < ε

Tactic:
exact mod_cast hi _ ij
-- Module: Mathlib.Data.Real.Archimedean
Goal:
f : ℕ → ℚ
x : ℝ
h : ∀ ε > 0, ∃ (i : ℕ), ∀ j ≥ i, |(↑(f j) : ℝ) - x| < ε
⊢ ∃ (h' : IsCauSeq abs f), mk (Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq abs f) f h') = x

Tactic:
⟨isCauSeq_iff_lift.2 (CauSeq.of_near _ (const abs x) h),
    sub_eq_zero.1 <|
      abs_eq_zero.1 <|
        (eq_of_le_of_forall_lt_imp_le_of_dense (abs_nonneg _)) fun _ε ε0 =>
          mk_near_of_forall_near <| (h _ ε0).imp fun _i h j ij => le_of_lt (h j ij)⟩

Premises used: Iff.mpr, abs, sub_eq_zero, le_of_lt, CauSeq.of_near, Exists.imp, eq_of_le_of_forall_lt_imp_le_of_dense, abs_eq_zero, Exists.intro, Iff.mp, Real.mk_near_of_forall_near, CauSeq.const, Real.isCauSeq_iff_lift
-- Module: Mathlib.Data.Real.Archimedean
Goal:
x : ℝ
⊢ ∃ (ub : ℤ), (↑ub : ℝ) ≤ x ∧ ∀ (z : ℤ), (↑z : ℝ) ≤ x → z ≤ ub

Tactic:
⟨⌊x⌋, Int.floor_le x, fun _ ↦ Int.le_floor.mpr⟩

Premises used: Iff.mpr, Int.floor, And.intro, Int.le_floor, Exists.intro, Int.floor_le
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
hne : s.Nonempty
hbdd : BddAbove s
rcases : ∀ (L : ℝ) (hL : L ∈ s) (U : ℝ) (hU : U ∈ upperBounds s), ∃ (x : ℝ), IsLUB s x
⊢ ∃ (x : ℝ), IsLUB s x

Tactic:
rcases hne, hbdd with ⟨⟨L, hL⟩, ⟨U, hU⟩⟩
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
obtain : ∀ (k : ℤ) (hk : U < (↑k : ℝ)) (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}
⊢ ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}

Tactic:
obtain ⟨k, hk⟩ := exists_int_gt U

Premises used: exists_int_gt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
⊢ ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}

Tactic:
fun d => ⟨k * d, fun z h => ?_⟩

Premises used: HMul.hMul, Nat.cast, BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
refine :
  ∀ (d : ℕ) (z : ℤ) (h : Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z), z ≤ k * (↑d : ℤ)
⊢ ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}

Tactic:
refine fun d => ⟨k * d, fun z h => ?_⟩
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
h : Membership.mem (γ := Set ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)} z
rcases : ∀ (y : ℝ) (yS : y ∈ s) (hy : (↑z : ℝ) ≤ y * (↑d : ℝ)), z ≤ k * (↑d : ℤ)
⊢ z ≤ k * (↑d : ℤ)

Tactic:
rcases h with ⟨y, yS, hy⟩
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
⊢ z ≤ k * (↑d : ℤ)

Tactic:
Int.cast_le.1 (hy.trans ?_)

Premises used: Int.cast_le, Iff.mp, LE.le.trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
refine : y * (↑d : ℝ) ≤ (↑(k * (↑d : ℤ)) : ℝ)
⊢ z ≤ k * (↑d : ℤ)

Tactic:
refine Int.cast_le.1 (hy.trans ?_)

Premises used: Int.cast_le, Iff.mp, LE.le.trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
push_cast : y * (↑d : ℝ) ≤ HMul.hMul (α := ℝ) (↑k : ℝ) (↑d : ℝ)
⊢ y * (↑d : ℝ) ≤ (↑(k * (↑d : ℤ)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
hbc : y ≤ (↑k : ℝ)
⊢ y * (↑d : ℝ) ≤ HMul.hMul (α := ℝ) (↑k : ℝ) (↑d : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
⊢ y ≤ (↑k : ℝ)

Tactic:
(hU yS).trans hk.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < (↑k : ℝ)
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : (↑z : ℝ) ≤ y * (↑d : ℝ)
⊢ y ≤ (↑k : ℝ)

Tactic:
exact (hU yS).trans hk.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
⊢ ∀ (d : ℕ), BddAbove (α := ℤ) {m : ℤ | ∃ y ∈ s, (↑m : ℝ) ≤ y * (↑d : ℝ)}

Tactic:
have : ∀ d : ℕ, BddAbove { m : ℤ | ∃ y ∈ s, (m : ℝ) ≤ y * d } := by
    obtain ⟨k, hk⟩ := exists_int_gt U
    refine fun d => ⟨k * d, fun z h => ?_⟩
    rcases h with ⟨y, yS, hy⟩
    refine Int.cast_le.1 (hy.trans ?_)
    push_cast
    gcongr
    exact (hU yS).trans hk.le
-- 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 : ℝ)}
choose :
  ∀ (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),
    ∃ (x : ℝ), IsLUB s x
⊢ ∃ (x : ℝ), IsLUB s x

Tactic:
choose f hf using fun d : ℕ =>
    Int.exists_greatest_of_bdd (this d) ⟨⌊L * d⌋, L, hL, Int.floor_le _⟩

Premises used: HMul.hMul, Int.floor, Nat.cast, And.intro, Exists.intro, Int.floor_le, Int.exists_greatest_of_bdd
-- 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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
hy : (↑(f n) : ℝ) ≤ y * (↑n : ℝ)
⊢ (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y

Tactic:
simpa using (div_le_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy

Premises used: Iff.mpr, div_le_iff₀, Nat.cast_pos
-- 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
⊢ ∀ n > 0, ∃ y ∈ s, (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ) ≤ y

Tactic:
have hf₁ : ∀ n > 0, ∃ y ∈ s, ((f n / n : ℚ) : ℝ) ≤ y := fun n n0 =>
    let ⟨y, yS, hy⟩ := (hf n).1
    ⟨y, yS, by simpa using (div_le_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy⟩
-- 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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
⊢ y * (↑n : ℝ) - 1 < (↑(f n) : ℝ)

Tactic:
have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * (↑n : ℝ) - 1 < (↑(f n) : ℝ)
simp : y - (↑n : ℝ)⁻¹ < HDiv.hDiv (α := ℝ) (↑(f n) : ℝ) (↑n : ℝ)
⊢ y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)

Tactic:
simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, gt_iff_lt]

Premises used: Rat.cast_intCast, Rat.cast_div, Rat.cast_natCast, gt_iff_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * (↑n : ℝ) - 1 < (↑(f n) : ℝ)
rwa : Ne (α := ℝ) (↑n : ℝ) 0
⊢ y - (↑n : ℝ)⁻¹ < HDiv.hDiv (α := ℝ) (↑(f n) : ℝ) (↑n : ℝ)

Tactic:
rwa [lt_div_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀]

Premises used: Iff.mpr, Nat.cast_pos, lt_div_iff₀, sub_mul, inv_mul_cancel₀
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * (↑n : ℝ) - 1 < (↑(f n) : ℝ)
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
(Nat.cast_pos.2 n0).ne'

Premises used: Iff.mpr, Nat.cast_pos, LT.lt.ne'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (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
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * (↑n : ℝ) - 1 < (↑(f n) : ℝ)
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
exact (Nat.cast_pos.2 n0).ne'

Premises used: Iff.mpr, Nat.cast_pos, LT.lt.ne'
-- 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
⊢ ∀ n > 0, ∀ y ∈ s, y - (↑n : ℝ)⁻¹ < (↑(HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) : ℝ)

Tactic:
have hf₂ : ∀ n > 0, ∀ y ∈ s, (y - ((n : ℕ) : ℝ)⁻¹) < (f n / n : ℚ) := by
    intro n n0 y yS
    have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
    simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, gt_iff_lt]
    rwa [lt_div_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀]
    exact (Nat.cast_pos.2 n0).ne'
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (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 : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
this :
  ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      |HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j)
            ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) i)| <
        ε

Tactic:
⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩

Premises used: Iff.mpr, le_rfl, Inv.inv, Nat.ceil, And.intro, Exists.intro, abs_lt
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (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 : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
this :
  ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
refine :
  ∀ (j : ℕ) (ij : j ≥ ⌈ε⁻¹⌉₊),
    -ε <
      HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j)
        ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) ⌈ε⁻¹⌉₊)
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      |HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j)
            ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) i)| <
        ε

Tactic:
refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
-- Module: Mathlib.Data.Real.Archimedean
Goal:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this_1 : ∀ (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 : ℚ)) : ℝ)
ε : ℚ
ε0 : ε > 0
this :
  ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, HDiv.hDiv (α := ℚ) (↑(f j) : ℚ) (↑j : ℚ) - HDiv.hDiv (α := ℚ) (↑(f k) : ℚ) (↑k : ℚ) < ε
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
rw :
  HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) ⌈ε⁻¹⌉₊)
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j) <
    ε
⊢ -ε <
    HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) j)
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℚ) (↑(f n) : ℚ) (↑n : ℚ)) ⌈ε⁻¹⌉₊)

Tactic:
rw [neg_lt, neg_sub]

Premises used: neg_sub, neg_lt