awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
rw :
  dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
      ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G) ≤
    dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G) +
      dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
          ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ +
      ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
          ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖

Tactic:
rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
      ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G) ≤
    dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G) +
      dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)

Tactic:
dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
      ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G) ≤
    dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G) +
      dist.{wG} (α := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)

Tactic:
exact dist_triangle _ _ _

Premises used: dist_triangle
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
          ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ +
      ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
          ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    (C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
      C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
(add_le_add Hrec I)

Premises used: add_le_add
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ((C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
      C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) =
    C * ∑ i ∈ insert i s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
simp [his, add_comm, left_distrib]

Premises used: add_comm, left_distrib
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
I :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
m₃ :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
          ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ +
      ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)
          ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖
m₄ :
  ((C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
      C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) =
    C * ∑ i ∈ insert i s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) ((insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ insert i s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
calc
        ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
            ‖f m₁ - f (s.piecewise m₂ m₁)‖ +
              ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ := by
          rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
          exact dist_triangle _ _ _
        _ ≤ (C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
              C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
          (add_le_add Hrec I)
        _ = C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
          simp [his, add_comm, left_distrib]

Premises used: Norm.norm, HMul.hMul, Finset.univ, add_le_add, HSub.hSub, Insert.insert, Finset.piecewise, Finset.prod, Max.max, Eq, DFunLike.coe, Finset.sum, ite
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
s : Finset ι
empty :
  ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (piecewise (π := E) ∅ m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ ∅, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (Hrec :
      ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
            ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
        C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖),
    ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
          ((f : (a : (i : ι) → E i) → G) ((Insert.insert i s).piecewise (π := E) m₂ m₁) : G)‖ ≤
      C * ∑ i ∈ Insert.insert i s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
    C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
induction s using Finset.induction with
    | empty => simp
    | insert i s his Hrec =>
      have I :
        ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
          C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
        have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) :=
          s.piecewise_insert _ _ _
        have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by
          simp [his]
        rw [B, A, ← f.map_update_sub]
        apply le_trans (H _)
        gcongr with j
        by_cases h : j = i
        · rw [h]
          simp
        · by_cases h' : j ∈ s <;> simp [h', h]
      calc
        ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
            ‖f m₁ - f (s.piecewise m₂ m₁)‖ +
              ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ := by
          rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
          exact dist_triangle _ _ _
        _ ≤ (C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
              C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
          (add_le_add Hrec I)
        _ = C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
          simp [his, add_comm, left_distrib]

Premises used: Norm.norm, HMul.hMul, Finset.univ, HSub.hSub, Insert.insert, Finset.piecewise, Finset.prod, Max.max, Eq, DFunLike.coe, Finset.sum, ite
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
⊢ ∀ (s : Finset ι),
    ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
          ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
      C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
have A :
    ∀ s : Finset ι,
      ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤
        C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := fun s ↦ by
    induction s using Finset.induction with
    | empty => simp
    | insert i s his Hrec =>
      have I :
        ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
          C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
        have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) :=
          s.piecewise_insert _ _ _
        have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by
          simp [his]
        rw [B, A, ← f.map_update_sub]
        apply le_trans (H _)
        gcongr with j
        by_cases h : j = i
        · rw [h]
          simp
        · by_cases h' : j ∈ s <;> simp [h', h]
      calc
        ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
            ‖f m₁ - f (s.piecewise m₂ m₁)‖ +
              ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ := by
          rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
          exact dist_triangle _ _ _
        _ ≤ (C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
              C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
          (add_le_add Hrec I)
        _ = C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
          simp [his, add_comm, left_distrib]
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (s : Finset ι),
    ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
          ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
      C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
        ((f : (a : (i : ι) → E i) → G) (piecewise (π := E) univ m₂ m₁) : G)‖ ≤
    C * ∑ i : ι, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
A univ

Premises used: Finset.univ
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (s : Finset ι),
    ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
          ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
      C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
h : m₂ = piecewise (π := E) univ m₂ m₁
⊢ ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G) ((f : (a : (i : ι) → E i) → G) m₂ : G)‖ ≤
    C * ∑ i : ι, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
convert! A univ

Premises used: Finset.univ
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
inst_6 : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (s : Finset ι),
    ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m₁ : G)
          ((f : (a : (i : ι) → E i) → G) (s.piecewise (π := E) m₂ m₁) : G)‖ ≤
      C * ∑ i ∈ s, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ m₂ = piecewise (π := E) univ m₂ m₁

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
h1 :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) univ j →
      (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
        update (β := fun (x : ι) ↦ ℝ) (fun (x : ι) ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j
⊢ LE.le (α := ℝ) (∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖)
    (∏ j : ι, update (β := fun (x : ι) ↦ ℝ) (fun (x : ι) ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j)

Tactic:
gcongr with j
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
h : Membership.mem (γ := Finset ι) univ j
h1 :
  (if j = j then ‖m₁ j - m₂ j‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
    update (β := fun (x : ι) ↦ ℝ) (fun (x : ι) ↦ max ‖m₁‖ ‖m₂‖) j ‖m₁ - m₂‖ j
h1₁ :
  ∀ (h : j ≠ i),
    (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
      update (β := fun (x : ι) ↦ ℝ) (fun (x : ι) ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j
⊢ (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
    update (β := fun (x : ι) ↦ ℝ) (fun (x : ι) ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j

Tactic:
rcases eq_or_ne j i with rfl | h

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
j : ι
h : Membership.mem (γ := Finset ι) univ j
h1 : ‖m₁ j - m₂ j‖ ≤ ‖m₁ - m₂‖
⊢ (if j = j then ‖m₁ j - m₂ j‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
    update (β := fun (x : ι) ↦ ℝ) (fun (x : ι) ↦ max ‖m₁‖ ‖m₂‖) j ‖m₁ - m₂‖ j

Tactic:
simp only [ite_true, Function.update_self]

Premises used: ite_true, Function.update_self
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
j : ι
h : Membership.mem (γ := Finset ι) univ j
⊢ ‖m₁ j - m₂ j‖ ≤ ‖m₁ - m₂‖

Tactic:
norm_le_pi_norm (m₁ - m₂) _

Premises used: HSub.hSub, norm_le_pi_norm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
j : ι
h : Membership.mem (γ := Finset ι) univ j
⊢ ‖m₁ j - m₂ j‖ ≤ ‖m₁ - m₂‖

Tactic:
exact norm_le_pi_norm (m₁ - m₂) _

Premises used: HSub.hSub, norm_le_pi_norm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
h_1 : Membership.mem (γ := Finset ι) univ j
h : j ≠ i
⊢ (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
    update (β := fun (x : ι) ↦ ℝ) (fun (x : ι) ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j

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

Premises used: sup_le_sup, norm_le_pi_norm, sup_le_iff, le_sup_iff