-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
private lemma uniformity_eq_seminorm :
    𝓤 (ContinuousMultilinearMap 𝕜 E G) = ⨅ r > 0, 𝓟 {f | ‖f.1 - f.2‖ < r}

Proof state:
case refine_2.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 ι
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
hf : f ∈ (ContinuousMultilinearMap.seminorm 𝕜 E G).ball 0 δ
x : (i : ι) → E i
hx : x ∈ (s, r).1
⊢ f x ∈ closedBall 0 (s, r).2

Tactic:
simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢

Result:
case refine_2.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 ι
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hx : x ∈ (s, r).1
hf : (ContinuousMultilinearMap.seminorm 𝕜 E G) f < δ
⊢ ‖f x‖ ≤ r

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 ι
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
i : ι
x✝ : i ∈ univ
⊢ 1 ≤ ‖x i‖

Tactic:
simpa only [div_self hc₀.ne'] using hcx i

Result:
no goals

Proof state:
case refine_1.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 ι
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ r, (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 r ∈ 𝓝 0

Tactic:
have hc₀ : 0 < ‖c‖ := one_pos.trans hc

Result:
case refine_1.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 ι
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ ∃ r, (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 r ∈ 𝓝 0

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 ι
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
this : ∀ (f : ContinuousMultilinearMap 𝕜 E G), (∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1) → ‖f‖ ≤ 1
⊢ (Bornology.IsVonNBounded 𝕜 (closedBall 0 ‖c‖) ∧ closedBall 0 1 ∈ 𝓝 0) ∧
    {f | Set.MapsTo (⇑f) (closedBall 0 ‖c‖) (closedBall 0 1)} ⊆ (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 1

Tactic:
simpa [NormedSpace.isVonNBounded_closedBall, closedBall_mem_nhds, Set.subset_def, Set.MapsTo]

Result:
no goals

Proof state:
case refine_1.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 ι
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ ∃ r, (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 r ∈ 𝓝 0

Tactic:
simp only [hasBasis_nhds_zero.mem_iff, Prod.exists]

Result:
case refine_1.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 ι
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
⊢ ∃ r a b,
    (Bornology.IsVonNBounded 𝕜 a ∧ b ∈ 𝓝 0) ∧
      {f | Set.MapsTo (⇑f) a b} ⊆ (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 r

Proof state:
case refine_2.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 ι
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hx : x ∈ (s, r).1
hf : ‖f‖ ≤ δ
⊢ ‖f x‖ ≤ r

Tactic:
replace hx : ‖x‖ ≤ ε := hε x hx

Result:
case refine_2.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 ι
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ ‖f x‖ ≤ r

Proof state:
case refine_1
𝕜 : 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 ι
⊢ ∃ r, (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 r ∈ 𝓝 0

Tactic:
rcases NormedField.exists_lt_norm 𝕜 1 with ⟨c, hc⟩

Result:
case refine_1.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 ι
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ r, (ContinuousMultilinearMap.seminorm 𝕜 E G).closedBall 0 r ∈ 𝓝 0

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 ι
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
this : 0 ≤ ε
⊢ ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι

Tactic:
gcongr

Result:
no goals