awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 := ⋯ }
obtain :
  ∀ (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),
    Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
obtain ⟨I, t, ht₀, hft⟩ :
        ∃ (I : Finset ι) (t : ∀ i, Set (E i)), (∀ i, t i ∈ 𝓝 0) ∧ Set.pi I t ⊆ f ⁻¹' V := by
      have hfV : f ⁻¹' V ∈ 𝓝 0 := (map_continuous f).tendsto' _ _ f.map_zero hV
      rwa [nhds_pi, Filter.mem_pi, exists_finite_iff_finset] at hfV

Premises used: Finset
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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
i : ι
rw :
  ∀ (hs : ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' s)) (f : ContinuousMultilinearMap 𝕜 E F) (V : Set F)
    (hV : Membership.mem (γ := Filter F) (𝓝 0) V) (h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1) (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) (i : ι),
    ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i

Tactic:
rw [isVonNBounded_pi_iff] at hs

Premises used: Bornology.isVonNBounded_pi_iff
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 : ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' 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
i : ι
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, x • eval (β := E) i '' s ⊆ t i

Tactic:
have := (hs i).tendsto_smallSets_nhds.eventually (mem_lift' (ht₀ i))
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 : ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' 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
i : ι
this : ∀ᶠ (x : 𝕜) in 𝓝 0, x • eval (β := E) i '' s ⊆ t i
rcases :
  ∀ (r : ℝ) (hr₀ : 0 < r)
    (hr : ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < r} x → x • eval (β := E) i '' s ⊆ t i),
    ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i

Tactic:
rcases NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff.1 this with ⟨r, hr₀, hr⟩

Premises used: Iff.mp, Filter.HasBasis.eventually_iff, NormedAddGroup.nhds_zero_basis_norm_lt
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 : ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' 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
i : ι
this : ∀ᶠ (x : 𝕜) in 𝓝 0, x • eval (β := E) i '' s ⊆ t i
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < r} x → x • eval (β := E) i '' s ⊆ t i
rcases : ∀ (c : 𝕜) (hc₀ : 0 < ‖c‖) (hc : ‖c‖ < r), ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i

Tactic:
rcases NormedField.exists_norm_lt 𝕜 hr₀ with ⟨c, hc₀, hc⟩

Premises used: NormedField.exists_norm_lt
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 : ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' 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
i : ι
this : ∀ᶠ (x : 𝕜) in 𝓝 0, x • eval (β := E) i '' s ⊆ t i
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < r} x → x • eval (β := E) i '' s ⊆ t i
c : 𝕜
hc₀ : 0 < ‖c‖
hc : ‖c‖ < r
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i

Tactic:
⟨c, norm_pos_iff.1 hc₀, fun c' hle x hx ↦ ?_⟩

Premises used: norm_pos_iff, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 : ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' 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
i : ι
this : ∀ᶠ (x : 𝕜) in 𝓝 0, x • eval (β := E) i '' s ⊆ t i
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < r} x → x • eval (β := E) i '' s ⊆ t i
c : 𝕜
hc₀ : 0 < ‖c‖
hc : ‖c‖ < r
refine : ∀ (c' : 𝕜) (hle : ‖c'‖ ≤ ‖c‖) (x : (i : ι) → E i) (hx : x ∈ s), c' • x i ∈ t i
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i

Tactic:
refine ⟨c, norm_pos_iff.1 hc₀, fun c' hle x hx ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 : ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' 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
i : ι
this : ∀ᶠ (x : 𝕜) in 𝓝 0, x • eval (β := E) i '' s ⊆ t i
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < r} x → x • eval (β := E) i '' s ⊆ t i
c : 𝕜
hc₀ : 0 < ‖c‖
hc : ‖c‖ < r
c' : 𝕜
hle : ‖c'‖ ≤ ‖c‖
x : (i : ι) → E i
hx : x ∈ s
⊢ c' • x i ∈ t i

Tactic:
hr (hle.trans_lt hc) ⟨_, ⟨x, hx, rfl⟩, rfl⟩

Premises used: And.intro, Exists.intro, LE.le.trans_lt, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 : ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' 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
i : ι
this : ∀ᶠ (x : 𝕜) in 𝓝 0, x • eval (β := E) i '' s ⊆ t i
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : 𝕜⦄, Membership.mem (γ := Set 𝕜) {y : 𝕜 | ‖y‖ < r} x → x • eval (β := E) i '' s ⊆ t i
c : 𝕜
hc₀ : 0 < ‖c‖
hc : ‖c‖ < r
c' : 𝕜
hle : ‖c'‖ ≤ ‖c‖
x : (i : ι) → E i
hx : x ∈ s
⊢ c' • x i ∈ t i

Tactic:
exact hr (hle.trans_lt hc) ⟨_, ⟨x, hx, rfl⟩, rfl⟩

Premises used: And.intro, Exists.intro, LE.le.trans_lt, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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
⊢ ∀ (i : ι), ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i

Tactic:
have : ∀ i, ∃ c : 𝕜, c ≠ 0 ∧ ∀ c' : 𝕜, ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i := fun i ↦ by
      rw [isVonNBounded_pi_iff] at hs
      have := (hs i).tendsto_smallSets_nhds.eventually (mem_lift' (ht₀ i))
      rcases NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff.1 this with ⟨r, hr₀, hr⟩
      rcases NormedField.exists_norm_lt 𝕜 hr₀ with ⟨c, hc₀, hc⟩
      refine ⟨c, norm_pos_iff.1 hc₀, fun c' hle x hx ↦ ?_⟩
      exact hr (hle.trans_lt hc) ⟨_, ⟨x, hx, rfl⟩, rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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
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)
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
choose c hc₀ hc using this
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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
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
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
rw [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV),
      NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]

Premises used: mem_of_mem_nhds, Filter.HasBasis.eventually_iff, absorbs_iff_eventually_nhds_zero, NormedAddGroup.nhds_zero_basis_norm_lt
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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
⊢ 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
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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

Tactic:
⟨‖∏ i ∈ I, c i‖, norm_pos_iff.2 hc₀', fun a ha ↦ mapsTo_image_iff.2 fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, Finset.prod, Set.mapsTo_image_iff, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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
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
⊢ ∃ (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:
refine ⟨‖∏ i ∈ I, c i‖, norm_pos_iff.2 hc₀', fun a ha ↦ mapsTo_image_iff.2 fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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
let : ∀ (i₀ : ι), ((fun (x : F) ↦ a • x) ∘ (⇑f : (a : (i : ι) → E i) → F)) x ∈ V
⊢ ((fun (x : F) ↦ a • x) ∘ (⇑f : (a : (i : ι) → E i) → F)) x ∈ V

Tactic:
let ⟨i₀⟩ := ‹Nonempty ι›
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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
inr : ∀ (hne : i ≠ i₀), 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

Tactic:
rcases eq_or_ne i i₀ with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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 ι)
inl : ((a / ∏ i ∈ I, c i) * c i) • x i ∈ t i
⊢ update (β := E) y i ((a / ∏ i ∈ I, c i) • y i) i ∈ t i

Tactic:
simp_rw [update_self, y, I.piecewise_eq_of_mem _ _ hi, smul_smul]

Premises used: smul_smul, Function.update_self, Finset.piecewise_eq_of_mem
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded
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

Tactic:
hc _ _ ?_ _ hx

Premises used: Set.Mem