-- Mathlib/Analysis/Normed/Group/Ultra.lean
@[to_additive]
lemma norm_tprod_le (f : ι → M) : ‖∏' i, f i‖ ≤ ⨆ i, ‖f i‖

Proof state:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
have h_bd : BddAbove (Set.range fun i ↦ ‖f i‖) :=
  h.tendsto_cofinite_one.norm'.bddAbove_range_of_cofinite

Result:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i => ‖f i‖)
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Proof state:
case inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
by_cases h : Multipliable f

Result:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Proof state:
case pos.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i => ‖f i‖)
s : Finset ι
⊢ ∀ i ∈ s, ‖f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
exact fun i _ ↦ le_ciSup h_bd i

Result:
no goals

Proof state:
case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
rw [tprod_eq_one_of_not_multipliable h, norm_one']

Result:
case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ 0 ≤ ⨆ i, ‖f i‖

Proof state:
case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
h_bd : ¬BddAbove (Set.range fun i => ‖f i‖)
⊢ 0 ≤ ⨆ i, ‖f i‖

Tactic:
rw [Real.iSup_of_not_bddAbove h_bd]

Result:
no goals

Proof state:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
h_bd : BddAbove (Set.range fun i => ‖f i‖)
⊢ 0 ≤ ⨆ i, ‖f i‖

Tactic:
exact le_ciSup_of_le h_bd hι.some (norm_nonneg' _)

Result:
no goals

Proof state:
case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : IsEmpty ι
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
simp only [tprod_empty, norm_one', Real.iSup_of_isEmpty, le_refl]

Result:
no goals

Proof state:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i => ‖f i‖)
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
refine le_of_tendsto' h.hasProd.norm' (fun s ↦ norm_prod_le_of_forall_le_of_nonneg ?_ ?_)

Result:
case pos.refine_1
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i => ‖f i‖)
s : Finset ι
⊢ 0 ≤ ⨆ i, ‖f i‖

case pos.refine_2
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i => ‖f i‖)
s : Finset ι
⊢ ∀ i ∈ s, ‖f i‖ ≤ ⨆ i, ‖f i‖

Proof state:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

Result:
case inl
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : IsEmpty ι
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

case inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Proof state:
case pos.refine_1
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i => ‖f i‖)
s : Finset ι
⊢ 0 ≤ ⨆ i, ‖f i‖

Tactic:
exact le_ciSup_of_le h_bd hι.some (norm_nonneg' _)

Result:
no goals

Proof state:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
swap

Result:
case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Proof state:
case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ 0 ≤ ⨆ i, ‖f i‖

Tactic:
by_cases h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)

Result:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
h_bd : BddAbove (Set.range fun i => ‖f i‖)
⊢ 0 ≤ ⨆ i, ‖f i‖

case neg
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
h_bd : ¬BddAbove (Set.range fun i => ‖f i‖)
⊢ 0 ≤ ⨆ i, ‖f i‖