-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem exists_bound_of_continuous (f : MultilinearMap 𝕜 E G) (hf : Continuous f) :
    ∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖

Proof state:
case inr
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
obtain ⟨ε : ℝ, ε0 : 0 < ε, hε : ∀ m : ∀ i, E i, ‖m - 0‖ < ε → ‖f m - f 0‖ < 1⟩ :=
  NormedAddCommGroup.tendsto_nhds_nhds.1 (hf.tendsto 0) 1 zero_lt_one

Result:
case inr.intro.intro
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m - 0‖ < ε → ‖f m - f 0‖ < 1
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Proof state:
case inl
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : IsEmpty ι
m : (i : ι) → E i
⊢ ‖f m‖ ≤ (‖f 0‖ + 1) * ∏ i : ι, ‖m i‖

Tactic:
obtain rfl : m = 0 := funext (IsEmpty.elim ‹_›)

Result:
case inl
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : IsEmpty ι
⊢ ‖f 0‖ ≤ (‖f 0‖ + 1) * ∏ i : ι, ‖0 i‖

Proof state:
case inr.intro.intro.intro
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
refine ⟨_, this, ?_⟩

Result:
case inr.intro.intro.intro
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
⊢ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖

Proof state:
case inr.intro.intro.intro
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
⊢ 1 ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖

Tactic:
rw [← div_le_iff₀' this, one_div, ← inv_pow, inv_div, Fintype.card, ← prod_const]

Result:
case inr.intro.intro.intro
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
⊢ ∏ _x : ι, ε / ‖c‖ ≤ ∏ i : ι, ‖m i‖

Proof state:
case inl
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : IsEmpty ι
⊢ ‖f 0‖ ≤ (‖f 0‖ + 1) * ∏ i : ι, ‖0 i‖

Tactic:
simp [univ_eq_empty, zero_le_one]

Result:
no goals

Proof state:
case inr.intro.intro.intro
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
⊢ ∏ _x : ι, ε / ‖c‖ ≤ ∏ i : ι, ‖m i‖

Tactic:
exact prod_le_prod (fun _ _ => div_nonneg ε0.le (norm_nonneg _)) fun i _ => hcm i

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : IsEmpty ι
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

case inr
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Proof state:
case inr.intro.intro
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m - 0‖ < ε → ‖f m - f 0‖ < 1
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
simp only [sub_zero, f.map_zero] at hε

Result:
case inr.intro.intro
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf : Continuous ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖