awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ 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‖
have B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)
Tactic: have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by
          simp [his]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ 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‖
have rw : norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) (update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i)) : G) ≤
  C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Tactic: rw [B, A, ← f.map_update_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)
⊢ norm.{wG} (E := G)
      ((f : (a : (i : ι) → E i) → G) (update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i)) : G) ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
have apply : C * ∏ i_1 : ι, ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) i_1‖ ≤
  C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Tactic: apply le_trans (H _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)
⊢ C * ∏ i_1 : ι, ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) i_1‖ ≤
    C * ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
have hbc : ∀ (j : ι),
  Membership.mem (γ := Finset ι) univ j →
    ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤
      if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Tactic: gcongr with j
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)
j : ι
h : Membership.mem (γ := Finset ι) univ j
⊢ ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
have pos : ∀ (h : j = i),
  ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)
j : ι
h : Membership.mem (γ := Finset ι) univ j
pos :
  ∀ (h : j = i),
    ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤
      if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
have neg : ∀ (h : ¬j = i),
  ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)
j : ι
h_1 : Membership.mem (γ := Finset ι) univ j
h : j = i
⊢ ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
have pos : ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) i‖ ≤ if i = i then ‖m₁ i - m₂ i‖ else max ‖m₁ i‖ ‖m₂ i‖
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)
j : ι
h_1 : Membership.mem (γ := Finset ι) univ j
h : ¬j = i
⊢ ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
have pos : ∀ (h' : j ∈ s),
  ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Tactic: by_cases h' : j ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
B : s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)
j : ι
h_1 : Membership.mem (γ := Finset ι) univ j
h : ¬j = i
pos :
  ∀ (h' : j ∈ s),
    ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤
      if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
have neg : ∀ (h' : j ∉ s),
  ‖update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Tactic: by_cases h' : j ∈ s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
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‖
⊢ ‖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‖
have 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‖
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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) ((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)‖
have 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)
Tactic: rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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) ((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‖
have 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)‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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)‖
⊢ ‖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‖
have 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‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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‖
have 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‖
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]
Cleared hypotheses: s