case intro
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
hk : Nat.succ l ≠ 0
⊢ 1 < a ^ Nat.succ l
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
k : ℕ
hk : k ≠ 0
⊢ 1 < a ^ k
rcases Nat.exists_eq_succ_of_ne_zero hk with ⟨l, rfl⟩
case intro
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
⊢ 1 < a ^ Nat.succ l
case intro
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
hk : Nat.succ l ≠ 0
⊢ 1 < a ^ Nat.succ l
clear hk
case intro.zero
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
⊢ 1 < a ^ Nat.succ Nat.zero

case intro.succ
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
IH : 1 < a ^ Nat.succ l
⊢ 1 < a ^ Nat.succ (Nat.succ l)
case intro
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
⊢ 1 < a ^ Nat.succ l
induction' l with l IH
case intro.zero
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
⊢ 1 < a * a ^ Nat.zero
case intro.zero
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
⊢ 1 < a ^ Nat.succ Nat.zero
rw [pow_succ]
no goals
case intro.zero
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
⊢ 1 < a * a ^ Nat.zero
simpa using ha
case intro.succ
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
IH : 1 < a ^ Nat.succ l
⊢ 1 < a * a ^ (l + 1)
case intro.succ
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
IH : 1 < a ^ Nat.succ l
⊢ 1 < a ^ Nat.succ (Nat.succ l)
rw [pow_succ]
no goals
case intro.succ
β : Type ?u.30171
A : Type ?u.30174
G : Type ?u.30177
M : Type u_1
R : Type ?u.30183
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x a : M
ha : 1 < a
l : ℕ
IH : 1 < a ^ Nat.succ l
⊢ 1 < a * a ^ (l + 1)
exact one_lt_mul'' ha IH