awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
this : ∀ (i : ι), ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
have choose : ∀ (c : (i : ι) → 𝕜) (hc₀ : ∀ (i : ι), c i ≠ 0) (hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i),
  Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
Tactic: choose c hc₀ hc using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
have rw : ∃ (i : ℝ),
  0 < i ∧
    ∀ ⦃x : 𝕜⦄,
      Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < i} x →
        MapsTo (fun (x_1 : F) ↦ x • x_1) ((⇑f : (a : (i : ι) → E i) → F) '' s) V
Tactic: rw [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV),
      NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
⊢ ∃ (i : ℝ),
    0 < i ∧
      ∀ ⦃x : 𝕜⦄,
        Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < i} x →
          MapsTo (fun (x_1 : F) ↦ x • x_1) ((⇑f : (a : (i : ι) → E i) → F) '' s) V
have hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
Tactic: have hc₀' : ∏ i ∈ I, c i ≠ 0 := Finset.prod_ne_zero_iff.2 fun i _ ↦ hc₀ i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
⊢ ∃ (i : ℝ),
    0 < i ∧
      ∀ ⦃x : 𝕜⦄,
        Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < i} x →
          MapsTo (fun (x_1 : F) ↦ x • x_1) ((⇑f : (a : (i : ι) → E i) → F) '' s) V
have refine : ∀ (a : 𝕜) (ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a) (x : (i : ι) → E i)
  (hx : x ∈ s), ((fun (x : F) ↦ a • x) ∘ (⇑f : (a : (i : ι) → E i) → F)) x ∈ V
Tactic: refine ⟨‖∏ i ∈ I, c i‖, norm_pos_iff.2 hc₀', fun a ha ↦ mapsTo_image_iff.2 fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
⊢ ((fun (x : F) ↦ a • x) ∘ (⇑f : (a : (i : ι) → E i) → F)) x ∈ V
have let : ∀ (i₀ : ι), ((fun (x : F) ↦ a • x) ∘ (⇑f : (a : (i : ι) → E i) → F)) x ∈ V
Tactic: let ⟨i₀⟩ := ‹Nonempty ι›
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
⊢ update (β := E) y i₀ ((a / ∏ i ∈ I, c i) • y i₀) i ∈ t i
have inl : update (β := E) y i ((a / ∏ i ∈ I, c i) • y i) i ∈ t i
Tactic: rcases eq_or_ne i i₀ with rfl | hne
Cleared hypotheses: i₀
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
inl : update (β := E) y i ((a / ∏ i ∈ I, c i) • y i) i ∈ t i
⊢ update (β := E) y i₀ ((a / ∏ i ∈ I, c i) • y i₀) i ∈ t i
have inr : ∀ (hne : i ≠ i₀), update (β := E) y i₀ ((a / ∏ i ∈ I, c i) • y i₀) i ∈ t i
Tactic: rcases eq_or_ne i i₀ with rfl | hne
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
⊢ update (β := E) y i ((a / ∏ i ∈ I, c i) • y i) i ∈ t i
have inl : ((a / ∏ i ∈ I, c i) * c i) • x i ∈ t i
Tactic: simp_rw [update_self, y, I.piecewise_eq_of_mem _ _ hi, smul_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
⊢ ((a / ∏ i ∈ I, c i) * c i) • x i ∈ t i
have inl : ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ ‖c i‖
Tactic: refine hc _ _ ?_ _ hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
⊢ ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖
have rw : ‖a‖ / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖ ≤
  norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖
Tactic: rw [norm_mul, norm_div]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
⊢ ‖a‖ / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖ ≤
    norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖
have hbc : ‖a‖ ≤ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
⊢ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖ ≤ 1 * ‖c i‖
have hbc : norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
⊢ ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ ‖c i‖
have i₁ : ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖
Tactic: calc
            ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ (‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖) * ‖c i‖ := by
              rw [norm_mul, norm_div]; gcongr; exact ha.out.le
            _ ≤ 1 * ‖c i‖ := by gcongr; apply div_self_le_one
            _ = ‖c i‖ := one_mul _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
i₁ : ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖
⊢ ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ ‖c i‖
have i₂ : norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖ ≤ 1 * ‖c i‖
Tactic: calc
            ‖(a / ∏ i ∈ I, c i) * c i‖ ≤ (‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖) * ‖c i‖ := by
              rw [norm_mul, norm_div]; gcongr; exact ha.out.le
            _ ≤ 1 * ‖c i‖ := by gcongr; apply div_self_le_one
            _ = ‖c i‖ := one_mul _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
hne : i ≠ i₀
⊢ update (β := E) y i₀ ((a / ∏ i ∈ I, c i) • y i₀) i ∈ t i
have inr : c i • x i ∈ t i
Tactic: simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
⊢ (f : (a : (i : ι) → E i) → F) (update (β := E) y i₀ ((a / ∏ i ∈ I, c i) • y i₀)) =
    HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : F)
have rw : HSMul.hSMul (β := F) (a / ∏ i ∈ I, c i) ((f : (a : (i : ι) → E i) → F) (update (β := E) y i₀ (y i₀)) : F) =
  HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : F)
Tactic: rw [f.map_update_smul, update_eq_self, f.map_piecewise_smul, div_eq_mul_inv, mul_smul,
          inv_smul_smul₀ hc₀']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Bounded (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_2, u_4} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
inst_7 : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x_1 : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)
hft : (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
c : (i : ι) → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : Ne.{u_2 + 1} (α := 𝕜) (∏ i ∈ I, c i) 0
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)} a
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
rw :
  HSMul.hSMul (β := F) (a / ∏ i ∈ I, c i) ((f : (a : (i : ι) → E i) → F) (update (β := E) y i₀ (y i₀)) : F) =
    HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : F)
⊢ (f : (a : (i : ι) → E i) → F) (update (β := E) y i₀ ((a / ∏ i ∈ I, c i) • y i₀)) =
    HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : F)
have rw₁ : HSMul.hSMul (β := F) (a / ∏ i ∈ I, c i) ((f : (a : (i : ι) → E i) → F) y : F) =
  HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : F)
Tactic: rw [f.map_update_smul, update_eq_self, f.map_piecewise_smul, div_eq_mul_inv, mul_smul,
          inv_smul_smul₀ hc₀']