-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem bound_of_shell_of_norm_map_coord_zero (f : MultilinearMap 𝕜 E G)
    (hf₀ : ∀ {m i}, ‖m i‖ = 0 → ‖f m‖ = 0)
    {ε : ι → ℝ} {C : ℝ} (hε : ∀ i, 0 < ε i) {c : ι → 𝕜} (hc : ∀ i, 1 < ‖c i‖)
    (hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖)
    (m : ∀ i, E i) : ‖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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
⊢ ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
choose δ hδ0 hδm_lt hle_δm _ using fun i => rescale_to_shell_semi_normed (hc i) (hε i) (hm i)

Result:
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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : ι → 𝕜
hδ0 : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
⊢ ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
⊢ ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
rcases em (∃ i, ‖m i‖ = 0) with (⟨i, hi⟩ | hm)

Result:
case inl.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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ ‖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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ¬∃ i, ‖m i‖ = 0
⊢ ‖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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : ι → 𝕜
hδ0 : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
⊢ ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
have hδ0 : 0 < ∏ i, ‖δ i‖ := prod_pos fun i _ => norm_pos_iff.2 (hδ0 i)

Result:
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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : ι → 𝕜
hδ0✝ : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
hδ0 : 0 < ∏ i : ι, ‖δ i‖
⊢ ‖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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ¬∃ i, ‖m i‖ = 0
⊢ ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
push_neg at hm

Result:
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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
⊢ ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Proof state:
case inl.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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖

Tactic:
rw [hf₀ hi, prod_eq_zero (mem_univ i) hi, mul_zero]

Result:
no goals