internlm/Lean-Github huggingface dataset:
Theorem: lt_exp_ofNat
Proof state before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (b < 2.7182818283 ^ a) _auto✝
⊢ b < (↑a).exp
Tactic:
rw [←Real.exp_one_pow a]
Proof state after:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (b < 2.7182818283 ^ a) _auto✝
⊢ b < exp 1 ^ a
Theorem: lt_exp_ofNat
Proof state before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (b < 2.7182818283 ^ a) _auto✝
⊢ b < exp 1 ^ a
Tactic:
exact _root_.trans h0 (pow_lt_pow_left Real.exp_one_gt_d9 (by norm_num) a0)
Proof state after:
no goals
Theorem: lt_exp_ofNat
Proof state before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (b < 2.7182818283 ^ a) _auto✝
⊢ 0 ≤ 2.7182818283
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt_exp_div
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
⊢ c < (↑a / ↑b).exp
Tactic:
have e : exp (a/b : ℝ) = exp 1 ^ (a / b : ℝ) := by rw [Real.exp_one_rpow]
Proof state after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ c < (↑a / ↑b).exp
Theorem: lt_exp_div
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ c < (↑a / ↑b).exp
Tactic:
rw [e, div_eq_mul_inv, Real.rpow_mul (Real.exp_nonneg _), Real.lt_rpow_inv_iff_of_pos,
  Real.rpow_natCast, Real.rpow_natCast]
Proof state after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ c ^ b < exp 1 ^ a

case hx
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ c

case hy
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ exp 1 ^ ↑a

case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 < ↑b
Theorem: lt_exp_div
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
⊢ (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
Tactic:
rw [Real.exp_one_rpow]
Proof state after:
no goals
Theorem: lt_exp_div
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ c ^ b < exp 1 ^ a
Tactic:
exact _root_.trans h0 (pow_lt_pow_left Real.exp_one_gt_d9 (by norm_num) a0)
Proof state after:
no goals
Theorem: lt_exp_div
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ 2.7182818283
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt_exp_div
Proof state before:
case hx
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ c
Tactic:
exact c0.le
Proof state after:
no goals
Theorem: lt_exp_div
Proof state before:
case hy
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ exp 1 ^ ↑a
Tactic:
apply Real.rpow_nonneg (Real.exp_nonneg _)
Proof state after:
no goals
Theorem: lt_exp_div
Proof state before:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 < ↑b
Tactic:
simp only [Nat.cast_pos, Nat.pos_iff_ne_zero]
Proof state after:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ b ≠ 0
Theorem: lt_exp_div
Proof state before:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c ^ b < 2.7182818283 ^ a) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ b ≠ 0
Tactic:
exact b0
Proof state after:
no goals
Theorem: exp_div_lt
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
⊢ (↑a / ↑b).exp < c
Tactic:
have e : exp (a/b : ℝ) = exp 1 ^ (a / b : ℝ) := by rw [Real.exp_one_rpow]
Proof state after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ (↑a / ↑b).exp < c
Theorem: exp_div_lt
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ (↑a / ↑b).exp < c
Tactic:
rw [e, div_eq_mul_inv, Real.rpow_mul (Real.exp_nonneg _), Real.rpow_inv_lt_iff_of_pos,
  Real.rpow_natCast, Real.rpow_natCast]
Proof state after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ exp 1 ^ a < c ^ b

case hx
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ exp 1 ^ ↑a

case hy
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ c

case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 < ↑b
Theorem: exp_div_lt
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
⊢ (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
Tactic:
rw [Real.exp_one_rpow]
Proof state after:
no goals
Theorem: exp_div_lt
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ exp 1 ^ a < c ^ b
Tactic:
exact _root_.trans (pow_lt_pow_left Real.exp_one_lt_d9 (Real.exp_nonneg _) a0) h0
Proof state after:
no goals
Theorem: exp_div_lt
Proof state before:
case hx
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ exp 1 ^ ↑a
Tactic:
apply Real.rpow_nonneg (Real.exp_nonneg _)
Proof state after:
no goals
Theorem: exp_div_lt
Proof state before:
case hy
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 ≤ c
Tactic:
exact c0.le
Proof state after:
no goals
Theorem: exp_div_lt
Proof state before:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ 0 < ↑b
Tactic:
simp only [Nat.cast_pos, Nat.pos_iff_ne_zero]
Proof state after:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ b ≠ 0
Theorem: exp_div_lt
Proof state before:
case hz
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c ^ b) _auto✝
e : (↑a / ↑b).exp = exp 1 ^ (↑a / ↑b)
⊢ b ≠ 0
Tactic:
exact b0
Proof state after:
no goals
Theorem: exp_neg_div_lt
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c⁻¹ ^ b < 2.7182818283 ^ a) _auto✝
⊢ (-(↑a / ↑b)).exp < c
Tactic:
rw [Real.exp_neg, inv_lt (Real.exp_pos _) c0]
Proof state after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c⁻¹ ^ b < 2.7182818283 ^ a) _auto✝
⊢ c⁻¹ < (↑a / ↑b).exp
Theorem: exp_neg_div_lt
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (c⁻¹ ^ b < 2.7182818283 ^ a) _auto✝
⊢ c⁻¹ < (↑a / ↑b).exp
Tactic:
exact lt_exp_div a0 b0 (inv_pos.mpr c0) h0
Proof state after:
no goals
Theorem: lt_exp_neg_div
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c⁻¹ ^ b) _auto✝
⊢ c < (-(↑a / ↑b)).exp
Tactic:
rw [Real.exp_neg, lt_inv c0 (Real.exp_pos _)]
Proof state after:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c⁻¹ ^ b) _auto✝
⊢ (↑a / ↑b).exp < c⁻¹
Theorem: lt_exp_neg_div
Proof state before:
a b : ℕ
c : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (b ≠ 0) _auto✝
c0 : autoParam (0 < c) _auto✝
h0 : autoParam (2.7182818286 ^ a < c⁻¹ ^ b) _auto✝
⊢ (↑a / ↑b).exp < c⁻¹
Tactic:
exact exp_div_lt a0 b0 (inv_pos.mpr c0) h0
Proof state after:
no goals
Theorem: lt_log_2
Proof state before:
⊢ 0.693 < log 2
Tactic:
rw [Real.lt_log_iff_exp_lt (by norm_num)]
Proof state after:
⊢ exp 0.693 < 2
Theorem: lt_log_2
Proof state before:
⊢ exp 0.693 < 2
Tactic:
norm_num
Proof state after:
⊢ (693 / 1000).exp < 2
Theorem: lt_log_2
Proof state before:
⊢ (693 / 1000).exp < 2
Tactic:
exact exp_div_lt
Proof state after:
no goals
Theorem: lt_log_2
Proof state before:
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt_log_3
Proof state before:
⊢ 1.098 < log 3
Tactic:
rw [Real.lt_log_iff_exp_lt (by norm_num)]
Proof state after:
⊢ exp 1.098 < 3
Theorem: lt_log_3
Proof state before:
⊢ exp 1.098 < 3
Tactic:
norm_num
Proof state after:
⊢ (549 / 500).exp < 3
Theorem: lt_log_3
Proof state before:
⊢ (549 / 500).exp < 3
Tactic:
exact exp_div_lt
Proof state after:
no goals
Theorem: lt_log_3
Proof state before:
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: log_3_lt
Proof state before:
⊢ log 3 < 1.099
Tactic:
rw [Real.log_lt_iff_lt_exp (by norm_num)]
Proof state after:
⊢ 3 < exp 1.099
Theorem: log_3_lt
Proof state before:
⊢ 3 < exp 1.099
Tactic:
norm_num
Proof state after:
⊢ 3 < (1099 / 1000).exp
Theorem: log_3_lt
Proof state before:
⊢ 3 < (1099 / 1000).exp
Tactic:
exact lt_exp_div
Proof state after:
no goals
Theorem: log_3_lt
Proof state before:
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt_log_4
Proof state before:
⊢ 1.386 < log 4
Tactic:
rw [Real.lt_log_iff_exp_lt (by norm_num)]
Proof state after:
⊢ exp 1.386 < 4
Theorem: lt_log_4
Proof state before:
⊢ exp 1.386 < 4
Tactic:
norm_num
Proof state after:
⊢ (693 / 500).exp < 4
Theorem: lt_log_4
Proof state before:
⊢ (693 / 500).exp < 4
Tactic:
exact exp_div_lt
Proof state after:
no goals
Theorem: lt_log_4
Proof state before:
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: log_4_lt
Proof state before:
⊢ log 4 < 1.387
Tactic:
rw [Real.log_lt_iff_lt_exp (by norm_num)]
Proof state after:
⊢ 4 < exp 1.387
Theorem: log_4_lt
Proof state before:
⊢ 4 < exp 1.387
Tactic:
norm_num
Proof state after:
⊢ 4 < (1387 / 1000).exp
Theorem: log_4_lt
Proof state before:
⊢ 4 < (1387 / 1000).exp
Tactic:
exact lt_exp_div
Proof state after:
no goals
Theorem: log_4_lt
Proof state before:
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ -(1 - 1 / x).log < 0.41
Tactic:
rw [neg_lt, Real.lt_log_iff_exp_lt (lt_of_lt_of_le (by norm_num) le)]
Proof state after:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-0.41).exp < 1 - 1 / x
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-0.41).exp < 1 - 1 / x
Tactic:
refine lt_of_lt_of_le ?_ le
Proof state after:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-0.41).exp < 2 / 3
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-0.41).exp < 2 / 3
Tactic:
norm_num
Proof state after:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-(41 / 100)).exp < 2 / 3
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-(41 / 100)).exp < 2 / 3
Tactic:
exact exp_neg_div_lt
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ 2 / 3 ≤ 1 - 1 / x
Tactic:
rw [le_tsub_iff_le_tsub (by norm_num), one_div, inv_le (by positivity)]
Proof state after:
x : ℝ
x3 : 3 ≤ x
⊢ (1 - 2 / 3)⁻¹ ≤ x

x : ℝ
x3 : 3 ≤ x
⊢ 0 < 1 - 2 / 3

x : ℝ
x3 : 3 ≤ x
⊢ 1 / x ≤ 1
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ 2 / 3 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ 0 < x
Tactic:
positivity
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ (1 - 2 / 3)⁻¹ ≤ x
Tactic:
exact le_trans (by norm_num) x3
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ (1 - 2 / 3)⁻¹ ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ 0 < 1 - 2 / 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ 1 / x ≤ 1
Tactic:
rw [one_div, inv_le_one_iff]
Proof state after:
x : ℝ
x3 : 3 ≤ x
⊢ x ≤ 0 ∨ 1 ≤ x
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ x ≤ 0 ∨ 1 ≤ x
Tactic:
right
Proof state after:
case h
x : ℝ
x3 : 3 ≤ x
⊢ 1 ≤ x
Theorem: neg_log_one_sub_lt
Proof state before:
case h
x : ℝ
x3 : 3 ≤ x
⊢ 1 ≤ x
Tactic:
exact le_trans (by norm_num) x3
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
⊢ 1 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: neg_log_one_sub_lt
Proof state before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ 0 < 2 / 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: NontrivialAnalyticOn.isolated
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
have fa : AnalyticAt ℂ (fun w ↦ f w - f z) z := (n.analyticOn z zs).sub analyticAt_const
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Theorem: NontrivialAnalyticOn.isolated
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
cases' fa.eventually_eq_zero_or_eventually_ne_zero with h h
Proof state after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - f z = 0
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z

case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝[≠] z, f z_1 - f z ≠ 0
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Theorem: NontrivialAnalyticOn.isolated
Proof state before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - f z = 0
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
have b := h.and_frequently (n.nonconst z zs)
Proof state after:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - f z = 0
b : ∃ᶠ (x : ℂ) in 𝓝 z, f x - f z = 0 ∧ f x ≠ f z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Theorem: NontrivialAnalyticOn.isolated
Proof state before:
case inl
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - f z = 0
b : ∃ᶠ (x : ℂ) in 𝓝 z, f x - f z = 0 ∧ f x ≠ f z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
simp only [sub_eq_zero, Ne, and_not_self_iff, Filter.frequently_false] at b
Proof state after:
no goals
Theorem: NontrivialAnalyticOn.isolated
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝[≠] z, f z_1 - f z ≠ 0
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
simp only [sub_ne_zero] at h
Proof state after:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝[≠] z, f z_1 ≠ f z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Theorem: NontrivialAnalyticOn.isolated
Proof state before:
case inr
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
fa : AnalyticAt ℂ (fun w => f w - f z) z
h : ∀ᶠ (z_1 : ℂ) in 𝓝[≠] z, f z_1 ≠ f z
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ f z
Tactic:
exact h
Proof state after:
no goals
Theorem: NontrivialAnalyticOn.isolated'
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a
Tactic:
by_cases h : f z = a
Proof state after:
case pos
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a

case neg
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
n : NontrivialAnalyticOn f s
z : ℂ
zs : z ∈ s
a : ℂ
h : ¬f z = a
⊢ ∀ᶠ (w : ℂ) in 𝓝[≠] z, f w ≠ a