-- 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.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 : ¬y = 0
⊢ (p fun x => y) = 0

Tactic:
replace hy := norm_pos_iff.mpr hy

Result:
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‖
⊢ (p fun x => y) = 0

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‖
⊢ (p fun x => y) = 0

Tactic:
refine norm_eq_zero.mp (le_antisymm (le_of_forall_pos_le_add fun ε ε_pos => ?_) (norm_nonneg _))

Result:
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 < ε
⊢ ‖p fun x => y‖ ≤ 0 + ε

Proof state:
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
y : E
c : ℝ
c_pos : c > 0
t : Set E
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
⊢ (p fun x => y) = 0

Tactic:
rcases n with - | n

Result:
case intro.intro.intro.intro.intro.intro.intro.zero
𝕜 : 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

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)‖
⊢ (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 : y = 0
⊢ (p fun x => y) = 0

Tactic:
simpa only [hy] using p.map_zero

Result:
no goals

Proof state:
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

Tactic:
clear h hc 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
y : E
c : ℝ
c_pos : c > 0
t : Set E
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 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)) < ε
⊢ ‖1 ^ n.succ‖ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) ≤ 0 + ε

Tactic:
simpa using h₃.le

Result:
no goals

Proof state:
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))⁻¹
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)) < ε
⊢ ‖p fun x => y‖ ≤ 0 + ε

Tactic:
calc
  ‖p fun _ => y‖ = ‖k⁻¹ ^ n.succ‖ * ‖p fun _ => k • y‖ := by
    simpa only [inv_smul_smul₀ (norm_pos_iff.mp k_pos), norm_smul, Finset.prod_const,
      Finset.card_fin] using
      congr_arg norm (p.map_smul_univ (fun _ : Fin n.succ => k⁻¹) fun _ : Fin n.succ => k • y)
  _ ≤ ‖k⁻¹ ^ n.succ‖ * (‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))) := by gcongr
  _ = ‖(k⁻¹ * k) ^ n.succ‖ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) := by
    rw [← mul_assoc]
    simp [norm_mul, mul_pow]
  _ ≤ 0 + ε := by
    rw [inv_mul_cancel₀ (norm_pos_iff.mp k_pos)]
    simpa using h₃.le

Result:
no goals