awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
have rw : ∀ (hi : Inseparable (m i) 0), Inseparable.{wG} (X := G) ((f : (a : (i : ι) → E i) → G) m : G) (0 : G)
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
Cleared hypotheses: hi
-- 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
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)
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) = 0
have 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)
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
Cleared hypotheses: hi
-- 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 ι
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
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have pos : ∀ (hm : ∃ (i : ι), ‖m i‖ = 0), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
Tactic: by_cases! hm : ∃ i, ‖m i‖ = 0
-- 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 ι
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‖
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have neg : ∀ (hm : ∀ (i : ι), ‖m i‖ ≠ 0), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
Tactic: by_cases! hm : ∃ i, ‖m i‖ = 0
-- 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 ι
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
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have pos : ∀ (i : ι) (hi : ‖m i‖ = 0), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
Tactic: rcases hm with ⟨i, hi⟩
Cleared hypotheses: hm
-- 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 ι
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
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have pos : 0 ≤ C * ∏ i : ι, ‖m i‖
Tactic: rw [hf₀ hi, prod_eq_zero (mem_univ i) hi, mul_zero]
-- 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 ι
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‖
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have pos₁ : 0 ≤ C * 0
Tactic: rw [hf₀ hi, prod_eq_zero (mem_univ i) hi, mul_zero]
-- 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 ι
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
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have pos₂ : LE.le (α := ℝ) 0 0
Tactic: rw [hf₀ hi, prod_eq_zero (mem_univ i) hi, mul_zero]
-- 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 ι
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
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have 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‖
Tactic: choose δ hδ0 hδm_lt hle_δm _ using fun i => rescale_to_shell_semi_normed (hc i) (hε i) (hm i)
-- 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 ι
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‖
⊢ norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have hδ0₁ : LT.lt (α := ℝ) 0 (∏ i : ι, ‖δ i‖)
Tactic: have hδ0 : 0 < ∏ i, ‖δ i‖ := prod_pos fun i _ => norm_pos_iff.2 (hδ0 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 ι
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have 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‖
Tactic: cases isEmpty_or_nonempty ι
-- 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 ι
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‖
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have 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‖
Tactic: cases isEmpty_or_nonempty ι
-- 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 ι
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‖
have 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‖
Tactic: refine ⟨‖f 0‖ + 1, add_pos_of_nonneg_of_pos (norm_nonneg _) zero_lt_one, fun m => ?_⟩
-- 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 ι
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : IsEmpty ι
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‖
have 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)
Tactic: obtain rfl : m = 0 := funext (IsEmpty.elim ‹_›)
Cleared hypotheses: m
-- 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 ι
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑f : (a : (i : ι) → E i) → G)
h : Nonempty ι
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have 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‖
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
-- 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 ι
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
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have hε₁ : ∀ (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ε
Cleared hypotheses: 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 ι
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 : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have 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‖
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-- 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 ι
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‖
⊢ ∃ (C : ℝ),
    0 < C ∧ ∀ (m : (i : ι) → E i), norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ C * ∏ i : ι, ‖m i‖
have this : 0 < (‖c‖ / ε) ^ Fintype.card ι
Tactic: have : 0 < (‖c‖ / ε) ^ Fintype.card ι := pow_pos (div_pos (zero_lt_one.trans hc) ε0) _
-- 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 ι
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‖
have inr : ∀ (m : (i : ι) → E i),
  norm.{wG} (E := G) ((f : (a : (i : ι) → E i) → G) m : G) ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
Tactic: refine ⟨_, this, ?_⟩
-- 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 ι
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‖
have 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‖
Tactic: refine f.bound_of_shell_of_continuous hf (fun _ => ε0) (fun _ => hc) fun m hcm hm => ?_
-- 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 ι
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‖
have inr : 1 ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
Tactic: refine (hε m ((pi_norm_lt_iff ε0).2 hm)).le.trans ?_
-- 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 ι
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‖ < ε
⊢ 1 ≤ (‖c‖ / ε) ^ Fintype.card ι * ∏ i : ι, ‖m i‖
have inr : LE.le (α := ℝ) (∏ _x : ι, ε / ‖c‖) (∏ i : ι, ‖m i‖)
Tactic: rw [← div_le_iff₀' this, one_div, ← inv_pow, inv_div, Fintype.card, ← prod_const]
-- 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 ι
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‖ < ε
⊢ LE.le (α := ℝ) (∏ _x : ι, ε / ‖c‖) (∏ i : ι, ‖m i‖)
have inr : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → ε / ‖c‖ ≤ ‖m i‖
Tactic: gcongr
-- 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) (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 A : (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 _ _ _