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_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)
⊢ (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₂ : (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)
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)
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)
⊢ (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₃ : (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)
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)
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)
⊢ (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₄ : 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)
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)
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)
⊢ (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 ((f : (a : (i : ι) → E i) → F) x : 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
⊢ ((fun (x : F) ↦ a • x) ∘ (⇑f : (a : (i : ι) → E i) → F)) x ∈ V
have 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: 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₀']
-- 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
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
have if : ∀ (h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1), 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₀']
-- 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
if : ∀ (h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
have if₁ : ∀ (h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1), 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₀']
-- 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
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
have if : ∀ (h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
Tactic: classical
  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₀']
-- 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
if : ∀ (h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
have if₁ : ∀ (h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1), Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
Tactic: classical
  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₀']
-- 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 : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
⊢ IsVonNBounded.{u_2, u_3} 𝕜 (E := F) ((⇑f : (a : (i : ι) → E i) → F) '' s)
have x : IsEmpty ι ∨ Nonempty ι
Tactic: cases isEmpty_or_nonempty ι with
  | inl h =>
    exact (isBounded_iff_isVonNBounded _).1 <|
      @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)
  | inr h => exact hs.image_multilinear' f
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Topology (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst : NormedField 𝕜
inst_1 : (i : ι) → TopologicalSpace (E i)
inst_2 : (i : ι) → AddCommGroup (E i)
inst_3 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : UniformSpace F
inst_7 : IsUniformAddGroup F
⊢ Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F)) (instTopologicalSpace (E := E))
    UniformSpace.toTopologicalSpace
have rw : Eq (α := TopologicalSpace (ContinuousMultilinearMap 𝕜 E F))
  (TopologicalSpace.induced (toUniformOnFun (E := E))
    (UniformOnFun.topologicalSpace ((i : ι) → E i) F {s : Set ((i : ι) → E i) | IsVonNBounded 𝕜 s}))
  UniformSpace.toTopologicalSpace
Tactic: rw [instTopologicalSpace, IsUniformAddGroup.rightUniformSpace_eq]