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_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‖ ≤ ‖c i‖
⊢ ((a / ∏ i ∈ I, c i) * c i) • x i ∈ t i

Tactic:
refine hc _ _ ?_ _ 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
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
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‖
⊢ ‖(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:
rw [norm_mul, norm_div]

Premises used: norm_mul, norm_div
-- 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 ι)
hbc : ‖a‖ ≤ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)
⊢ ‖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:
gcongr
-- 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‖ ≤ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)

Tactic:
ha.out.le

Premises used: Membership.mem.out, LT.lt.le
-- 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‖ ≤ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i)

Tactic:
exact ha.out.le

Premises used: Membership.mem.out, LT.lt.le
-- 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 ι)
hbc : norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) ≤ 1
⊢ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖ ≤ 1 * ‖c i‖

Tactic:
gcongr
-- 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 ι)
⊢ norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) ≤ 1

Tactic:
apply div_self_le_one

Premises used: div_self_le_one
-- 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 ι)
⊢ 1 * ‖c i‖ = ‖c i‖

Tactic:
one_mul _

Premises used: one_mul
-- 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 ι)
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‖
i₂ : norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) / norm.{u_2} (E := 𝕜) (∏ i ∈ I, c i) * ‖c i‖ ≤ 1 * ‖c i‖
⊢ ‖(a / ∏ i ∈ I, c 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 _

Premises used: Norm.norm, HDiv.hDiv, Finset.prod, one_mul
-- 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 ι)
hne : i ≠ i₀
inr : c i • x i ∈ t i
⊢ update (β := E) y i₀ ((a / ∏ i ∈ I, c i) • y i₀) i ∈ t i

Tactic:
simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]

Premises used: Finset.piecewise_eq_of_mem, Function.update_of_ne
-- 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 ι)
hne : i ≠ i₀
⊢ c i • x i ∈ t i

Tactic:
hc _ _ le_rfl _ hx

Premises used: le_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
i₀ : ι
y : (i : ι) → E i := I.piecewise (π := E) (fun (i : ι) ↦ c i • x i) x
i : ι
hi : i ∈ (↑I : Set ι)
hne : i ≠ i₀
⊢ c i • x i ∈ t i

Tactic:
exact hc _ _ le_rfl _ hx

Premises used: le_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
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)
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)
rw₂ :
  (a / ∏ i ∈ I, c i) •
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := F) (∏ i ∈ I, c i) ((f : (a : (i : ι) → E i) → F) x : F) =
    HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : F)
rw₃ :
  (a * (∏ i ∈ I, c i)⁻¹) •
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := F) (∏ i ∈ I, c i) ((f : (a : (i : ι) → E i) → F) x : F) =
    HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : F)
rw₄ :
  a •
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (∏ i ∈ I, c i)⁻¹
        (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := F) (∏ i ∈ I, c i) ((f : (a : (i : ι) → E i) → F) x : F)) =
    HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : F)
rw₅ rw₆ :
  HSMul.hSMul (β := F) a ((f : (a : (i : ι) → E i) → F) x : 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)

Tactic:
rw [f.map_update_smul, update_eq_self, f.map_piecewise_smul, div_eq_mul_inv, mul_smul,
          inv_smul_smul₀ hc₀']

Premises used: ContinuousMultilinearMap.map_piecewise_smul, Function.update_eq_self, inv_smul_smul₀, div_eq_mul_inv, ContinuousMultilinearMap.map_update_smul, SemigroupAction.mul_smul
-- 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
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)
⊢ ((fun (x : F) ↦ a • x) ∘ (⇑f : (a : (i : ι) → E i) → F)) x ∈ V

Tactic:
calc
      f (update y i₀ ((a / ∏ i ∈ I, c i) • y i₀)) ∈ V := hft fun i hi => by
        rcases eq_or_ne i i₀ with rfl | hne
        · simp_rw [update_self, y, I.piecewise_eq_of_mem _ _ hi, smul_smul]
          refine hc _ _ ?_ _ hx
          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 _
        · simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]
          exact hc _ _ le_rfl _ hx
      _ = a • f x := by
        rw [f.map_update_smul, update_eq_self, f.map_piecewise_smul, div_eq_mul_inv, mul_smul,
          inv_smul_smul₀ hc₀']

Premises used: Function.update, HDiv.hDiv, Finset.prod, HSMul.hSMul, DFunLike.coe
-- 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
if : ∀ (h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
if₁ : ∀ (h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
if₂ : ∀ (h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
if₃ if₄ : ∀ (h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
if h₁ : ∀ c : 𝕜, ‖c‖ ≤ 1 then
    exact absorbs_iff_norm.2 ⟨2, fun c hc ↦ by linarith [h₁ c]⟩
  else
    let _ : NontriviallyNormedField 𝕜 := ⟨by simpa using h₁⟩
    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
    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⟩
    choose c hc₀ hc using this
    rw [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV),
      NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]
    have hc₀' : ∏ i ∈ I, c i ≠ 0 := Finset.prod_ne_zero_iff.2 fun i _ ↦ hc₀ i
    refine ⟨‖∏ i ∈ I, c i‖, norm_pos_iff.2 hc₀', fun a ha ↦ mapsTo_image_iff.2 fun x hx ↦ ?_⟩
    let ⟨i₀⟩ := ‹Nonempty ι›
    set y := I.piecewise (fun i ↦ c i • x i) x
    calc
      f (update y i₀ ((a / ∏ i ∈ I, c i) • y i₀)) ∈ V := hft fun i hi => by
        rcases eq_or_ne i i₀ with rfl | hne
        · simp_rw [update_self, y, I.piecewise_eq_of_mem _ _ hi, smul_smul]
          refine hc _ _ ?_ _ hx
          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 _
        · simp_rw [update_of_ne hne, y, I.piecewise_eq_of_mem _ _ hi]
          exact hc _ _ le_rfl _ hx
      _ = a • f x := by
        rw [f.map_update_smul, update_eq_self, f.map_piecewise_smul, div_eq_mul_inv, mul_smul,
          inv_smul_smul₀ hc₀']

Premises used: Iff.mpr, Finset, mem_of_mem_nhds, absorbs_iff_norm, Exists.intro, Filter.HasBasis.eventually_iff, absorbs_iff_eventually_nhds_zero, NormedAddGroup.nhds_zero_basis_norm_lt, OfNat.ofNat