awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : Finite ι
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : TopologicalSpace F
inst_5 : AddCommGroup F
inst_6 : IsTopologicalAddGroup F
inst_7 : Module 𝕜 F
G : Type u_5
inst_8 : AddCommGroup G
inst_9 : TopologicalSpace G
inst_10 : Module 𝕜 G
inst_11 : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
s : Set (G × ((i : ι) → E i))
x : G × ((i : ι) → E i)
⊢ ContinuousWithinAt (Y := F)
    (fun (p : G × ((i : ι) → E i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 E F) p.1 : ContinuousMultilinearMap 𝕜 E F) : (a : (i : ι) → E i) → F)
        p.2)
    s x

Tactic:
f.continuous_uncurry_of_multilinear.continuousWithinAt

Premises used: ContinuousLinearMap.continuous_uncurry_of_multilinear, Continuous.continuousWithinAt
-- 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
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
rw : ∀ (hi : Inseparable (m i) 0), Inseparable.{wG} (X := G) ((f : (a : (i : ι) → E i) → G) m : G) (0 : G)
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0

Tactic:
rw [← inseparable_zero_iff_norm] at hi ⊢

Premises used: inseparable_zero_iff_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
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
m : (i : ι) → E i
i : ι
hi : Inseparable (m i) 0
⊢ Inseparable (update (β := E) m i 0) m

Tactic:
have : Inseparable (update m i 0) m := inseparable_pi.2 <|
    (forall_update_iff m fun i a ↦ Inseparable a (m i)).2 ⟨hi.symm, fun _ _ ↦ 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
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
m : (i : ι) → E i
i : ι
hi : Inseparable (m i) 0
this : Inseparable (update (β := E) m i 0) m
⊢ Inseparable.{wG} (X := G) ((f : (a : (i : ι) → E i) → G) m : G) (0 : G)

Tactic:
simpa only [map_update_zero] using this.symm.map hf

Premises used: MultilinearMap.map_update_zero, Inseparable.symm, Inseparable.map
-- 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
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
rw rw₁ rw₂ : ∀ (hi : Inseparable (m i) 0), Inseparable.{wG} (X := G) ((f : (a : (i : ι) → E i) → G) m : G) (0 : G)
rw₃ :
  ∀ (hi : Inseparable (m i) 0) (this : Inseparable (update (β := E) m i 0) m),
    Inseparable.{wG} (X := G) ((f : (a : (i : ι) → E i) → G) m : G) (0 : G)
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0

Tactic:
classical
  rw [← inseparable_zero_iff_norm] at hi ⊢
  have : Inseparable (update m i 0) m := inseparable_pi.2 <|
    (forall_update_iff m fun i a ↦ Inseparable a (m i)).2 ⟨hi.symm, fun _ _ ↦ rfl⟩
  simpa only [map_update_zero] using this.symm.map hf

Premises used: MultilinearMap.map_update_zero, inseparable_zero_iff_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
hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : (i : ι) → E i),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
pos : ∀ (hm : ∃ (i : ι), ‖m i‖ = 0), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
neg : ∀ (hm : ∀ (i : ι), ‖m i‖ ≠ 0), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
by_cases! hm : ∃ i, ‖m i‖ = 0
-- 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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : (i : ι) → E i),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∃ (i : ι), ‖m i‖ = 0
pos : ∀ (i : ι) (hi : ‖m i‖ = 0), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
rcases hm with ⟨i, hi⟩
-- 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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : (i : ι) → E i),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
pos : 0 ≤ C * ∏ i : ι, ‖m i‖
pos₁ : 0 ≤ C * 0
pos₂ pos₃ : LE.le (α := ℝ) 0 0
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
rw [hf₀ hi, prod_eq_zero (mem_univ i) hi, mul_zero]

Premises used: Finset.mem_univ, MulZeroClass.mul_zero, Finset.prod_eq_zero
-- 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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : (i : ι) → E i),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
neg :
  ∀ (δ : (i : ι) → 𝕜) (hδ0 : ∀ (i : ι), δ i ≠ 0) (hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i)
    (hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖),
    (∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖) →
      norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
choose δ hδ0 hδm_lt hle_δm _ using fun i => rescale_to_shell_semi_normed (hc i) (hε i) (hm i)

Premises used: rescale_to_shell_semi_normed
-- 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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : (i : ι) → E i),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : (i : ι) → 𝕜
hδ0 : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
h : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
⊢ LT.lt (α := ℝ) 0 (∏ i : ι, ‖δ i‖)

Tactic:
have hδ0 : 0 < ∏ i, ‖δ i‖ := prod_pos fun i _ => norm_pos_iff.2 (hδ0 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 ι
f : MultilinearMap 𝕜 E G
hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : (i : ι) → E i),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : (i : ι) → 𝕜
hδ0_1 : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
h : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
hδ0 : LT.lt (α := ℝ) 0 (∏ i : ι, ‖δ i‖)
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
simpa [map_smul_univ, norm_smul, prod_mul_distrib, mul_left_comm C, hδ0] using
    hf (fun i => δ i • m i) hle_δm hδm_lt

Premises used: Finset.prod_mul_distrib, norm_smul, mul_left_comm, HSMul.hSMul, MultilinearMap.map_smul_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 ι
f : MultilinearMap 𝕜 E G
hfc :
  Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf :
  ∀ (m : (i : ι) → E i),
    (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) →
      (∀ (i : ι), ‖m i‖ < ε i) → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
m : (i : ι) → E i
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
bound_of_shell_of_norm_map_coord_zero f (norm_map_coord_zero f hfc) hε hc hf m

Premises used: MultilinearMap.bound_of_shell_of_norm_map_coord_zero, MultilinearMap.norm_map_coord_zero
-- 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)
inl :
  IsEmpty ι →
    ∃ (C : ℝ),
      0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
inr :
  Nonempty ι →
    ∃ (C : ℝ),
      0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- 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 : IsEmpty ι
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
⟨‖f 0‖ + 1, add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one, fun m => ?_⟩

Premises used: Norm.norm, zero_lt_one, add_pos_of_nonneg_of_pos, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, DFunLike.coe, norm_nonneg
-- 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 : IsEmpty ι
inl :
  ∀ (m : (i : ι) → E i),
    norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤
      (norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) 0 : G) + 1) * ∏ i : ι, ‖m i‖
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
refine ⟨‖f 0‖ + 1, add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one, fun m => ?_⟩
-- 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 : IsEmpty ι
m : (i : ι) → E i
⊢ m = 0

Tactic:
funext (IsEmpty.elim ‹_›)

Premises used: IsEmpty.elim, funext
-- 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 : IsEmpty ι
m : (i : ι) → E i
inl :
  norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) 0 : G) ≤
    (norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) 0 : G) + 1) * ∏ i : ι, norm.{wE} (E := E i) (0 i)
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤
    (norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) 0 : G) + 1) * ∏ i : ι, ‖m i‖

Tactic:
obtain rfl : m = 0 := funext (IsEmpty.elim ‹_›)

Premises used: IsEmpty.elim, funext, 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : IsEmpty ι
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) 0 : G) ≤
    (norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) 0 : G) + 1) * ∏ i : ι, norm.{wE} (E := E i) (0 i)

Tactic:
simp [univ_eq_empty, zero_le_one]

Premises used: Finset.univ_eq_empty, zero_le_one
-- 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 ι
inr :
  ∀ (ε : ℝ) (ε0 : 0 < ε)
    (hε :
      ∀ (m : (i : ι) → E i),
        ‖m - 0‖ < ε →
          ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m : G) ((f : (a : (i : ι) → E i) → G) 0 : G)‖ <
            1),
    ∃ (C : ℝ),
      0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
obtain ⟨ε : ℝ, ε0 : 0 < ε, hε : ∀ m : ∀ i, E i, ‖m - 0‖ < ε → ‖f m - f 0‖ < 1⟩ :=
    NormedAddCommGroup.tendsto_nhds_nhds.1 (hf.tendsto 0) 1 zero_lt_one

Premises used: NormedAddCommGroup.tendsto_nhds_nhds, Continuous.tendsto, zero_lt_one, Iff.mp, OfNat.ofNat
-- 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 - 0‖ < ε →
      ‖HSub.hSub (α := G) (β := G) ((f : (a : (i : ι) → E i) → G) m : G) ((f : (a : (i : ι) → E i) → G) 0 : G)‖ < 1
⊢ ∀ (m : (i : ι) → E i), ‖m‖ < ε → norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) < 1

Tactic:
simp only [sub_zero, f.map_zero] at hε

Premises used: sub_zero, MultilinearMap.map_zero
-- 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
inr :
  ∀ (c : 𝕜) (hc : 1 < ‖c‖),
    ∃ (C : ℝ),
      0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Premises used: NormedField.exists_one_lt_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
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‖
⊢ 0 < (‖c‖ / ε) ^ Fintype.card ι

Tactic:
have : 0 < (‖c‖ / ε) ^ Fintype.card ι := pow_pos (div_pos (zero_lt_one.trans hc) ε0) _
-- 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 ι
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
⟨_, this, ?_⟩

Premises used: And.intro, Exists.intro
-- 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),
    norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖

Tactic:
refine ⟨_, this, ?_⟩
-- 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),
    norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖

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

Premises used: MultilinearMap.bound_of_shell_of_continuous