Theorem: Imo2013P5.le_of_all_pow_lt_succ' (Compfiles/Imo2013P5.lean)

State before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
⊢ x ≤ y
Tactic:
refine le_of_all_pow_lt_succ hx ?_ h
State after:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
⊢ 1 < y

State before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
⊢ 1 < y
Tactic:
by_contra! hy''
State after:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
⊢ False

State before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
⊢ False
Tactic:
obtain ⟨y', h1_lt_y', h_y'_lt_x⟩ := exists_between hx
State after:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
⊢ False

State before:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
⊢ False
Tactic:
have h_y_lt_y' : y < y' := hy''.trans_lt h1_lt_y'
State after:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
⊢ False

State before:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
⊢ False
Tactic:
have hh : ∀ n, 0 < n → x^n - 1 < y'^n := by
  intro n hn
  calc x^n - 1 < y^n  := h n hn
       _  ≤ y'^n := pow_le_pow_left hy.le h_y_lt_y'.le n
State after:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
hh : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y' ^ n
⊢ False

State before:
case intro.intro
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
hh : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y' ^ n
⊢ False
Tactic:
exact h_y'_lt_x.not_le (le_of_all_pow_lt_succ hx h1_lt_y' hh)
State after:
no goals

State before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
⊢ ∀ (n : ℕ), 0 < n → x ^ n - 1 < y' ^ n
Tactic:
intro n hn
State after:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
n : ℕ
hn : 0 < n
⊢ x ^ n - 1 < y' ^ n

State before:
x y : ℝ
hx : 1 < x
hy : 0 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hy'' : y ≤ 1
y' : ℝ
h1_lt_y' : 1 < y'
h_y'_lt_x : y' < x
h_y_lt_y' : y < y'
n : ℕ
hn : 0 < n
⊢ x ^ n - 1 < y' ^ n
Tactic:
calc x^n - 1 < y^n  := h n hn
     _  ≤ y'^n := pow_le_pow_left hy.le h_y_lt_y'.le n
State after:
no goals