-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem add_pow_le {F α : Type*} [CommRing α] [FunLike F α ℝ]
    [RingSeminormClass F α ℝ] {f : F} (hna : IsNonarchimedean f) (n : ℕ) (a b : α) :
    ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Proof state:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
hm_lt : m < n + 1
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
refine ⟨m, hm_lt, ?_⟩

Result:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
hm_lt : m < n + 1
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Proof state:
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
obtain ⟨m, hm_lt, hM⟩ := finset_image_add hna
  (fun m => a ^ m * b ^ (n - m) * ↑(n.choose m)) (Finset.range (n + 1))

Result:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : (Finset.range (n + 1)).Nonempty → m ∈ Finset.range (n + 1)
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Proof state:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
hm_lt : m < n + 1
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
simp only [← add_pow] at hM

Result:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : m < n + 1
hM : f ((a + b) ^ n) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Proof state:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : (Finset.range (n + 1)).Nonempty → m ∈ Finset.range (n + 1)
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
simp only [Finset.nonempty_range_iff, ne_eq, Nat.succ_ne_zero, not_false_iff, Finset.mem_range,
  if_true, forall_true_left] at hm_lt

Result:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hM : f (∑ m ∈ Finset.range (n + 1), a ^ m * b ^ (n - m) * ↑(n.choose m)) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
hm_lt : m < n + 1
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Proof state:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : m < n + 1
hM : f ((a + b) ^ n) ≤ f (a ^ m * b ^ (n - m) * ↑(n.choose m))
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
rw [mul_comm] at hM

Result:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : m < n + 1
hM : f ((a + b) ^ n) ≤ f (↑(n.choose m) * (a ^ m * b ^ (n - m)))
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Proof state:
case intro.intro
F : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : m < n + 1
hM : f ((a + b) ^ n) ≤ f (↑(n.choose m) * (a ^ m * b ^ (n - m)))
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
exact le_trans hM (le_trans (nmul_le hna) (map_mul_le_mul _ _ _))

Result:
no goals