-- Mathlib/Analysis/Analytic/Uniqueness.lean
theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {n : ℕ} {p : E[×n]→L[𝕜] F}
    (h : (fun y => p fun _ => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)) (y : E) : (p fun _ => y) = 0

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)
y : E
c : ℝ
c_pos : c > 0
hc : IsBigOWith c (𝓝 0) (fun y => p fun x => y) fun y => ‖y‖ ^ (n + 1)
t : Set E
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖
t_open : IsOpen t
z_mem : 0 ∈ t
⊢ (p fun x => y) = 0

Tactic:
obtain ⟨δ, δ_pos, δε⟩ := (Metric.isOpen_iff.mp t_open) 0 z_mem

Result:
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)
y : E
c : ℝ
c_pos : c > 0
hc : IsBigOWith c (𝓝 0) (fun y => p fun x => y) fun y => ‖y‖ ^ (n + 1)
t : Set E
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖
t_open : IsOpen t
z_mem : 0 ∈ t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
⊢ (p fun x => y) = 0

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)
y : E
c : ℝ
c_pos : c > 0
hc : IsBigOWith c (𝓝 0) (fun y => p fun x => y) fun y => ‖y‖ ^ (n + 1)
⊢ (p fun x => y) = 0

Tactic:
obtain ⟨t, ht, t_open, z_mem⟩ := eventually_nhds_iff.mp (isBigOWith_iff.mp hc)

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)
y : E
c : ℝ
c_pos : c > 0
hc : IsBigOWith c (𝓝 0) (fun y => p fun x => y) fun y => ‖y‖ ^ (n + 1)
t : Set E
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖
t_open : IsOpen t
z_mem : 0 ∈ t
⊢ (p fun x => y) = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < δ * ‖y‖⁻¹ ⊓ ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹
h₁ : ‖k • y‖ < δ
h₂ : ‖p fun x => k • y‖ ≤ ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))
h₃ : ‖k‖ * (c * ‖y‖ ^ (n.succ + 1)) < ε
⊢ ‖k⁻¹ ^ n.succ‖ * ‖p fun x => k • y‖ ≤ ‖k⁻¹ ^ n.succ‖ * (‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))))

Tactic:
gcongr

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (0 + 1)‖
⊢ ‖p fun x => y‖ = 0

Tactic:
simpa only [fin0_apply_norm, norm_eq_zero, norm_zero, zero_add, pow_one,
  mul_zero, norm_le_zero_iff] using ht 0 (δε (Metric.mem_ball_self δ_pos))

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
⊢ ‖p fun x => y‖ ≤ 0 + ε

Tactic:
obtain ⟨k, k_pos, k_norm⟩ := NormedField.exists_norm_lt 𝕜
  (lt_min (mul_pos δ_pos (inv_pos.mpr hy)) (mul_pos ε_pos (inv_pos.mpr h₀)))

Result:
case intro.intro.intro.intro.intro.intro.intro.succ.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < δ * ‖y‖⁻¹ ⊓ ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹
⊢ ‖p fun x => y‖ ≤ 0 + ε

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)
y : E
⊢ (p fun x => y) = 0

Tactic:
obtain ⟨c, c_pos, hc⟩ := h.exists_pos

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
h : (fun y => p fun x => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)
y : E
c : ℝ
c_pos : c > 0
hc : IsBigOWith c (𝓝 0) (fun y => p fun x => y) fun y => ‖y‖ ^ (n + 1)
⊢ (p fun x => y) = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < δ * ‖y‖⁻¹ ⊓ ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹
h₁ : ‖k • y‖ < δ
⊢ ‖p fun x => k • y‖ ≤ c * ‖k • y‖ ^ (n.succ + 1)

Tactic:
simpa only [norm_pow, _root_.norm_norm] using ht (k • y) (δε (mem_ball_zero_iff.mpr h₁))

Result:
no goals