Theorem: Nat.pow_lt_pow_of_lt_left (Extra/Nat/Lemmas.lean)

State before:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
⊢ a ^ (n + 1) < b ^ (n + 1)
Tactic:
have hpos : 0 < b ^ n := Nat.pos_pow_of_pos n (Nat.zero_lt_of_lt h)
State after:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ (n + 1) < b ^ (n + 1)

State before:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ (n + 1) < b ^ (n + 1)
Tactic:
simp [Nat.pow_succ]
State after:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ n * a < b ^ n * b

State before:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ n * a < b ^ n * b
Tactic:
apply Nat.mul_lt_mul_of_le_of_lt _ h hpos
State after:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ n ≤ b ^ n

State before:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ n ≤ b ^ n
Tactic:
exact Nat.pow_le_pow_of_le_left (Nat.le_of_lt h) n
State after:
no goals