-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_image_sub_le_of_bound' [DecidableEq ι] (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 * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Proof state:
case h.e'_3.h.e'_3.h.e'_6.h.e'_6
𝕜 : 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 ι
inst✝ : DecidableEq ι
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 :
  ∀ (s : Finset ι),
    ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖
⊢ m₂ = univ.piecewise m₂ m₁

Tactic:
simp

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 ι
inst✝ : DecidableEq ι
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 : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖
I :
  ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖
⊢ ((C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖) +
      C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖) =
    C * ∑ i ∈ insert i s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖

Tactic:
simp [his, add_comm, left_distrib]

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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
s : Finset ι
⊢ ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖

Tactic:
induction' s using Finset.induction with i s his Hrec

Result:
case empty
𝕜 : 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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
⊢ ‖f m₁ - f (∅.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ ∅, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖

case insert
𝕜 : 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 ι
inst✝ : DecidableEq ι
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 : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖
⊢ ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∑ i ∈ insert i s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖

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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
⊢ ∀ (s : Finset ι),
    ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖

Tactic:
intro s

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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
s : Finset ι
⊢ ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖

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 ι
inst✝ : DecidableEq ι
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 : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
⊢ ‖f (update (s.piecewise m₂ m₁) i (m₁ i - m₂ i))‖ ≤ C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖

Tactic:
apply le_trans (H _)

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 ι
inst✝ : DecidableEq ι
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 : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
⊢ C * ∏ i_1 : ι, ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) i_1‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖