case zero
𝓕 : Type ?u.748962
𝕜 : Type ?u.748965
α : Type ?u.748968
ι : Type ?u.748971
κ : Type ?u.748974
E : Type u_1
F : Type ?u.748980
G : Type ?u.748983
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
⊢ ‖a ^ Nat.zero‖ ≤ ↑Nat.zero * ‖a‖

case succ
𝓕 : Type ?u.748962
𝕜 : Type ?u.748965
α : Type ?u.748968
ι : Type ?u.748971
κ : Type ?u.748974
E : Type u_1
F : Type ?u.748980
G : Type ?u.748983
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
n : ℕ
ih : ‖a ^ n‖ ≤ ↑n * ‖a‖
⊢ ‖a ^ Nat.succ n‖ ≤ ↑(Nat.succ n) * ‖a‖
𝓕 : Type ?u.748962
𝕜 : Type ?u.748965
α : Type ?u.748968
ι : Type ?u.748971
κ : Type ?u.748974
E : Type u_1
F : Type ?u.748980
G : Type ?u.748983
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
n : ℕ
a : E
⊢ ‖a ^ n‖ ≤ ↑n * ‖a‖
induction' n with n ih
no goals
case succ
𝓕 : Type ?u.748962
𝕜 : Type ?u.748965
α : Type ?u.748968
ι : Type ?u.748971
κ : Type ?u.748974
E : Type u_1
F : Type ?u.748980
G : Type ?u.748983
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
n : ℕ
ih : ‖a ^ n‖ ≤ ↑n * ‖a‖
⊢ ‖a ^ Nat.succ n‖ ≤ ↑(Nat.succ n) * ‖a‖
simpa only [pow_succ', Nat.cast_succ, add_mul, one_mul] using norm_mul_le_of_le ih le_rfl
no goals
case zero
𝓕 : Type ?u.748962
𝕜 : Type ?u.748965
α : Type ?u.748968
ι : Type ?u.748971
κ : Type ?u.748974
E : Type u_1
F : Type ?u.748980
G : Type ?u.748983
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a✝ a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
a : E
⊢ ‖a ^ Nat.zero‖ ≤ ↑Nat.zero * ‖a‖
simp