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 ι
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
inr :
  ∀ (m : (i : ι) → E i) (hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖) (hm : ∀ (i : ι), ‖m i‖ < ε),
    norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
⊢ ∀ (m : (i : ι) → E i),
    norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖

Tactic:
refine f.bound_of_shell_of_continuous hf (fun _ => ε0) (fun _ => hc) fun m hcm hm => ?_

Premises used: MultilinearMap.bound_of_shell_of_continuous
-- 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖

Tactic:
(hε m ((pi_norm_lt_iff ε0).2 hm)).le.trans ?_

Premises used: Iff.mpr, LT.lt.le, pi_norm_lt_iff, LE.le.trans
-- 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
inr : 1 ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖

Tactic:
refine (hε m ((pi_norm_lt_iff ε0).2 hm)).le.trans ?_

Premises used: Iff.mpr, LT.lt.le, pi_norm_lt_iff, LE.le.trans
-- 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
inr : LE.le (α := ℝ) (∏ _x : ι, ε / ‖c‖) (∏ i : ι, ‖m i‖)
⊢ 1 ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖

Tactic:
rw [← div_le_iff₀' this, one_div, ← inv_pow, inv_div, Fintype.card, ← prod_const]

Premises used: Fintype.card, Finset.prod_const, inv_pow, one_div, inv_div, div_le_iff₀'
-- 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
inr : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → ε / ‖c‖ ≤ ‖m i‖
⊢ LE.le (α := ℝ) (∏ _x : ι, ε / ‖c‖) (∏ i : ι, ‖m i‖)

Tactic:
gcongr
-- 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
i : ι
h_1 : Membership.mem (γ := Finset ι) univ i
⊢ ε / ‖c‖ ≤ ‖m i‖

Tactic:
apply hcm
-- 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
⊢ ‖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:
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 ι
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‖
⊢ (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)

Tactic:
have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) :=
          s.piecewise_insert _ _ _
-- 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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
⊢ s.piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₁ i)

Tactic:
simp [his]
-- 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‖
A : (insert i s).piecewise (π := E) m₂ m₁ = update (β := E) (s.piecewise (π := E) m₂ m₁) i (m₂ i)
⊢ 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]
-- 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‖
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)
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‖
⊢ ‖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:
rw [B, A, ← f.map_update_sub]

Premises used: MultilinearMap.map_update_sub
-- 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‖
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)
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‖
⊢ 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:
apply le_trans (H _)

Premises used: le_trans
-- 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‖
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)
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‖
⊢ 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:
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 ι
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‖
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‖
⊢ ‖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
-- 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‖
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 :
  ‖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‖
⊢ ‖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:
rw [h]
-- 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‖
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) i‖ ≤ if i = i then ‖m₁ i - m₂ i‖ else max ‖m₁ i‖ ‖m₂ i‖

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 ι
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‖
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‖
⊢ ‖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
-- 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‖
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
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:
simp [h', h]
-- 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‖
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
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:
simp [h', h]
-- 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‖
⊢ ‖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]