-- Mathlib/Analysis/Normed/Group/Ultra.lean
/-- Nonarchimedean norm of a product is less than or equal the norm of any term in the product.
This version is phrased using `Finset.sup'` and `Finset.Nonempty` due to `Finset.sup`
operating over an `OrderBot`, which `ℝ` is not.
-/
@[to_additive "Nonarchimedean norm of a sum is less than or equal the norm of any term in the sum.
This version is phrased using `Finset.sup'` and `Finset.Nonempty` due to `Finset.sup`
operating over an `OrderBot`, which `ℝ` is not. "]
lemma _root_.Finset.Nonempty.norm_prod_le_sup'_norm {s : Finset ι} (hs : s.Nonempty) (f : ι → M) :
    ‖∏ i ∈ s, f i‖ ≤ s.sup' hs (‖f ·‖)

Proof state:
case cons
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Tactic:
refine (le_total ‖∏ i ∈ t, f i‖ ‖f j‖).imp ?_ ?_ <;> intro h

Result:
case cons.refine_1
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
h : ‖∏ i ∈ t, f i‖ ≤ ‖f j‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖

case cons.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
h : ‖f j‖ ≤ ‖∏ i ∈ t, f i‖
⊢ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Proof state:
case cons
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ∃ b ∈ Finset.cons j t hj, ‖∏ i ∈ Finset.cons j t hj, f i‖ ≤ ‖f b‖

Tactic:
simp only [Finset.prod_cons, Finset.mem_cons, exists_eq_or_imp]

Result:
case cons
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Proof state:
case cons.refine_1
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
h : ‖∏ i ∈ t, f i‖ ≤ ‖f j‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖

Tactic:
exact (norm_mul_le_max _ _).trans (max_eq_left h).le

Result:
no goals

Proof state:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
hs : s.Nonempty
f : ι → M
⊢ ‖∏ i ∈ s, f i‖ ≤ s.sup' hs fun x => ‖f x‖

Tactic:
simp only [Finset.le_sup'_iff]

Result:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
hs : s.Nonempty
f : ι → M
⊢ ∃ b ∈ s, ‖∏ i ∈ s, f i‖ ≤ ‖f b‖

Proof state:
case singleton
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
⊢ ∃ b ∈ {j}, ‖∏ i ∈ {j}, f i‖ ≤ ‖f b‖

Tactic:
simp only [Finset.mem_singleton, Finset.prod_singleton, exists_eq_left, le_refl]

Result:
no goals

Proof state:
case cons.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs✝ : t.Nonempty
IH : ∃ b ∈ t, ‖∏ i ∈ t, f i‖ ≤ ‖f b‖
h : ‖f j‖ ≤ ‖∏ i ∈ t, f i‖
⊢ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Tactic:
exact ⟨_, IH.choose_spec.left, (norm_mul_le_max _ _).trans <|
  ((max_eq_right h).le.trans IH.choose_spec.right)⟩

Result:
no goals