-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_image_sub_le_of_bound (f : MultilinearMap 𝕜 E G)
    {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : ∀ i, E i) :
    ‖f m₁ - f m₂‖ ≤ C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Proof state:
case h0
𝕜 : 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
a✝ : j ∈ univ
⊢ 0 ≤ if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖

Tactic:
by_cases h : j = i <;> simp [h, norm_nonneg]

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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ (∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖) ≤ ∏ j : ι, update (fun x => ‖m₁‖ ⊔ ‖m₂‖) i ‖m₁ - m₂‖ j

Tactic:
apply Finset.prod_le_prod

Result:
case h0
𝕜 : 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ∀ i_1 ∈ univ, 0 ≤ if i_1 = i then ‖m₁ i - m₂ i‖ else ‖m₁ i_1‖ ⊔ ‖m₂ i_1‖

case h1
𝕜 : 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ∀ i_1 ∈ univ, (if i_1 = i then ‖m₁ i - m₂ i‖ else ‖m₁ i_1‖ ⊔ ‖m₂ i_1‖) ≤ update (fun x => ‖m₁‖ ⊔ ‖m₂‖) i ‖m₁ - m₂‖ i_1

Proof state:
case pos
𝕜 : 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
a✝ : j ∈ univ
h : j = i
⊢ ‖m₁ i - m₂ i‖ ≤ ‖m₁ - m₂‖

Tactic:
exact norm_le_pi_norm (m₁ - m₂) 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (i : ι),
    (∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖) ≤ ‖m₁ - m₂‖ * (‖m₁‖ ⊔ ‖m₂‖) ^ (Fintype.card ι - 1)
⊢ ‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * (‖m₁‖ ⊔ ‖m₂‖) ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Tactic:
calc
  ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
    f.norm_image_sub_le_of_bound' hC H m₁ m₂
  _ ≤ C * ∑ _i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by gcongr; apply A
  _ = C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ := by
    rw [sum_const, card_univ, nsmul_eq_mul]
    ring

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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (i : ι),
    (∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖) ≤ ‖m₁ - m₂‖ * (‖m₁‖ ⊔ ‖m₂‖) ^ (Fintype.card ι - 1)
⊢ C * (↑(Fintype.card ι) * (‖m₁ - m₂‖ * (‖m₁‖ ⊔ ‖m₂‖) ^ (Fintype.card ι - 1))) =
    C * ↑(Fintype.card ι) * (‖m₁‖ ⊔ ‖m₂‖) ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Tactic:
ring

Result:
no goals

Proof state:
case neg
𝕜 : 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ (if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖) ≤ update (fun x => ‖m₁‖ ⊔ ‖m₂‖) i ‖m₁ - m₂‖ j

Tactic:
simp [h, - le_sup_iff, - sup_le_iff, sup_le_sup, norm_le_pi_norm]

Result:
no goals

Proof state:
case pos
𝕜 : 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
a✝ : j ∈ univ
h : j = i
⊢ (if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖) ≤ update (fun x => ‖m₁‖ ⊔ ‖m₂‖) i ‖m₁ - m₂‖ j

Tactic:
rw [h]

Result:
case pos
𝕜 : 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
a✝ : j ∈ univ
h : j = i
⊢ (if i = i then ‖m₁ i - m₂ i‖ else ‖m₁ i‖ ⊔ ‖m₂ i‖) ≤ update (fun x => ‖m₁‖ ⊔ ‖m₂‖) i ‖m₁ - 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ∏ j : ι, update (fun x => ‖m₁‖ ⊔ ‖m₂‖) i ‖m₁ - m₂‖ j = ‖m₁ - m₂‖ * (‖m₁‖ ⊔ ‖m₂‖) ^ (Fintype.card ι - 1)

Tactic:
rw [prod_update_of_mem (Finset.mem_univ _)]

Result:
𝕜 : 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
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ‖m₁ - m₂‖ * ∏ x ∈ univ \ {i}, ‖m₁‖ ⊔ ‖m₂‖ = ‖m₁ - m₂‖ * (‖m₁‖ ⊔ ‖m₂‖) ^ (Fintype.card ι - 1)