-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleNumber.lean
theorem liouville_liouvilleNumber {m : ℕ} (hm : 2 ≤ m) : Liouville (liouvilleNumber m)

Proof state:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n

Tactic:
have hpos := remainder_pos m1 n

Result:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n

Proof state:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n : ℕ
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n

Tactic:
rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩

Result:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n

Proof state:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ 2 ≤ ↑m

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n

Tactic:
refine ⟨p, m ^ n !, one_lt_pow₀ mZ1 n.factorial_ne_zero, ?_⟩

Result:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑↑p / ↑(↑m ^ n !) ∧ |liouvilleNumber ↑m - ↑↑p / ↑(↑m ^ n !)| < 1 / ↑(↑m ^ n !) ^ n

Proof state:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n

Tactic:
simpa [abs_of_pos hpos, hpos.ne'] using @remainder_lt n m (by assumption_mod_cast)

Result:
no goals

Proof state:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n

Tactic:
rw [← partialSum_add_remainder m1 n, ← hp]

Result:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n

Proof state:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)

Tactic:
have m1 : 1 < (m : ℝ) := by norm_cast

Result:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)

Proof state:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ 1 < ↑m

Tactic:
norm_cast

Result:
no goals

Proof state:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑↑p / ↑(↑m ^ n !) ∧ |liouvilleNumber ↑m - ↑↑p / ↑(↑m ^ n !)| < 1 / ↑(↑m ^ n !) ^ n

Tactic:
push_cast

Result:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n

Proof state:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n

Tactic:
rw [Nat.cast_pow] at hp

Result:
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n

Proof state:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)

Tactic:
intro n

Result:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n : ℕ
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n

Proof state:
m : ℕ
hm : 2 ≤ m
⊢ 1 < ↑m

Tactic:
norm_cast

Result:
no goals

Proof state:
m : ℕ
hm : 2 ≤ m
⊢ Liouville (liouvilleNumber ↑m)

Tactic:
have mZ1 : 1 < (m : ℤ) := by norm_cast

Result:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)