awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → TopologicalSpace (M₁ i)
inst_6 : TopologicalSpace M₂
f : ContinuousMultilinearMap R M₁ M₂
inst_7 : ContinuousAdd M₂
inst_8 : DecidableEq ι
inst_9 : Fintype ι
x y : (i : ι) → M₁ i
⊢ Eq.{w₂ + 1} (α := M₂)
    ((∑ i : ι,
            ContinuousLinearMap.comp (σ₂₃ := RingHom.id R)
              (let __src := f.toMultilinearMap (M₁ := M₁).toLinearMap (M₁ := M₁) x i;
              { toLinearMap := __src, cont := ⋯ })
              (ContinuousLinearMap.proj (φ := M₁) i) :
          (a : (i : ι) → M₁ i) → M₂)
        y :
      M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)
have simp : Eq.{w₂ + 1} (α := M₂)
  (∑ c : ι,
    comp (β := M₁ c) (⇑(f.toMultilinearMap (M₁ := M₁).toLinearMap (M₁ := M₁) x c) : (a : M₁ c) → M₂)
      (⇑(ContinuousLinearMap.proj (φ := M₁) c) : (a : (i : ι) → M₁ i) → M₁ c) y)
  (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)))
Tactic: simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
    ContinuousLinearMap.coe_mk', Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
n : ℕ
M : Fin n.succ → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
A : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : ContinuousMul A
⊢ Continuous (MultilinearMap.toFun (M₁ := fun (i : Fin n) ↦ A) (MultilinearMap.mkPiAlgebraFin R n A))
have change : Continuous (Y := A) fun (m : Fin n → A) ↦ (List.ofFn m).prod
Tactic: change Continuous fun m => (List.ofFn m).prod
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
n : ℕ
M : Fin n.succ → Type w
M₁ : ι → Type w₁
M₁' : ι → Type w₁'
M₂ : Type w₂
M₃ : Type w₃
M₄ : Type w₄
A : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : ContinuousMul A
⊢ Continuous (Y := A) fun (m : Fin n → A) ↦ (List.ofFn m).prod
have simp_rw : Continuous (Y := A) fun (m : Fin n → A) ↦ (List.map m (List.finRange n)).prod
Tactic: simp_rw [List.ofFn_eq_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
A : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : ContinuousMul A
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra R (Fin n) A)
    (ContinuousMultilinearMap.mkPiAlgebraFin R n A)
have H : ∀ (x : (i : Fin n) → A),
  Eq (α := A) ((ContinuousMultilinearMap.mkPiAlgebra R (Fin n) A : (a : (i : Fin n) → A) → A) x : A)
    ((ContinuousMultilinearMap.mkPiAlgebraFin R n A : (a : (i : Fin n) → A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M : Type u_1
inst : Fintype ι
inst_1 : CommRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace R
inst_5 : TopologicalSpace M
inst_6 : ContinuousMul R
inst_7 : ContinuousSMul R M
z₁ z₂ : M
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι z₁)
      (ContinuousMultilinearMap.mkPiRing R ι z₂) ↔
    z₁ = z₂
have rw : Eq (α := MultilinearMap R (fun (x : ι) ↦ R) M)
    (toMultilinearMap (M₁ := fun (x : ι) ↦ R) (ContinuousMultilinearMap.mkPiRing R ι z₁))
    (toMultilinearMap (M₁ := fun (x : ι) ↦ R) (ContinuousMultilinearMap.mkPiRing R ι z₂)) ↔
  z₁ = z₂
Tactic: rw [← toMultilinearMap_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M : Type u_1
inst : Fintype ι
inst_1 : CommRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace R
inst_5 : TopologicalSpace M
inst_6 : ContinuousMul R
inst_7 : ContinuousSMul R M
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι 0) 0
have h : Eq.{u_1 + 1} (α := M) ((ContinuousMultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
  ((0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M : Type u_1
inst : Fintype ι
inst_1 : CommRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace R
inst_5 : TopologicalSpace M
inst_6 : ContinuousMul R
inst_7 : ContinuousSMul R M
⊢ Eq.{u_1 + 1} (α := M) ((ContinuousMultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
    ((0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
have h : HSMul.hSMul.{u, u_1, u_1} (α := R) (β := M) (∏ i : ι, 1) 0 = (0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1
Tactic: rw [mkPiRing_apply, smul_zero, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M : Type u_1
inst : Fintype ι
inst_1 : CommRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace R
inst_5 : TopologicalSpace M
inst_6 : ContinuousMul R
inst_7 : ContinuousSMul R M
h : HSMul.hSMul.{u, u_1, u_1} (α := R) (β := M) (∏ i : ι, 1) 0 = (0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1
⊢ Eq.{u_1 + 1} (α := M) ((ContinuousMultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
    ((0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
have h₁ : Eq.{u_1 + 1} (α := M) (0 : M) ((0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
Tactic: rw [mkPiRing_apply, smul_zero, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M : Type u_1
inst : Fintype ι
inst_1 : CommRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace R
inst_5 : TopologicalSpace M
inst_6 : ContinuousMul R
inst_7 : ContinuousSMul R M
h : HSMul.hSMul.{u, u_1, u_1} (α := R) (β := M) (∏ i : ι, 1) 0 = (0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1
h₁ : Eq.{u_1 + 1} (α := M) (0 : M) ((0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
⊢ Eq.{u_1 + 1} (α := M) ((ContinuousMultilinearMap.mkPiRing R ι 0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
    ((0 : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1 : M)
have h₂ : Eq.{u_1 + 1} (α := M) 0 0
Tactic: rw [mkPiRing_apply, smul_zero, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M : Type u_1
inst : Fintype ι
inst_1 : CommRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace R
inst_5 : TopologicalSpace M
inst_6 : ContinuousMul R
inst_7 : ContinuousSMul R M
z : M
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι z) 0 ↔ z = 0
have rw : Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι z)
    (ContinuousMultilinearMap.mkPiRing R ι 0) ↔
  z = 0
Tactic: rw [← mkPiRing_zero, mkPiRing_eq_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Multilinear.Basic (goal)
Goal:
R : Type u
ι : Type v
M : Type u_1
inst : Fintype ι
inst_1 : CommRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace R
inst_5 : TopologicalSpace M
inst_6 : ContinuousMul R
inst_7 : ContinuousSMul R M
z : M
rw :
  Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι z)
      (ContinuousMultilinearMap.mkPiRing R ι 0) ↔
    z = 0
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι z) 0 ↔ z = 0
have rw₁ : z = 0 ↔ z = 0
Tactic: rw [← mkPiRing_zero, mkPiRing_eq_iff]
-- 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
c : 𝕜
hc : 2 ≤ ‖c‖
⊢ (⇑f : (a : (i : ι) → E i) → F) '' s ⊆ c • V
have linarith : -1 + (2 - ‖c‖) + (‖c‖ - 1) = 0
Tactic: linarith [h₁ c]
-- 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)),
    (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
      (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
have hfV : Membership.mem (γ := Filter ((i : ι) → E i)) (𝓝 0) ((⇑f : (a : (i : ι) → E i) → F) ⁻¹' V)
Tactic: have hfV : f ⁻¹' V ∈ 𝓝 0 := (map_continuous f).tendsto' _ _ f.map_zero hV
-- 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 := ⋯ }
hfV : Membership.mem (γ := Filter ((i : ι) → E i)) (𝓝 0) ((⇑f : (a : (i : ι) → E i) → F) ⁻¹' V)
⊢ ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
    (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
      (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
have rwa : ∀
  (hfV :
    Membership.mem (γ := Filter ((i : ι) → E i)) (Filter.pi (α := E) fun (i : ι) ↦ 𝓝 (0 i))
      ((⇑f : (a : (i : ι) → E i) → F) ⁻¹' V)),
  ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
    (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
      (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
Tactic: rwa [nhds_pi, Filter.mem_pi, exists_finite_iff_finset] at hfV
Cleared hypotheses: hfV
-- 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 := ⋯ }
hfV : Membership.mem (γ := Filter ((i : ι) → E i)) (𝓝 0) ((⇑f : (a : (i : ι) → E i) → F) ⁻¹' V)
rwa :
  ∀
    (hfV :
      Membership.mem (γ := Filter ((i : ι) → E i)) (Filter.pi (α := E) fun (i : ι) ↦ 𝓝 (0 i))
        ((⇑f : (a : (i : ι) → E i) → F) ⁻¹' V)),
    ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
      (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
        (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
⊢ ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
    (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
      (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
have rwa₁ : ∀
  (hfV :
    ∃ (I : Set ι),
      I.Finite ∧
        ∃ (t : (i : ι) → Set (E i)),
          (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 (0 i)) (t i)) ∧
            I.pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V),
  ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
    (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
      (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
Tactic: rwa [nhds_pi, Filter.mem_pi, exists_finite_iff_finset] at hfV
Cleared hypotheses: hfV
-- 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 := ⋯ }
hfV : Membership.mem (γ := Filter ((i : ι) → E i)) (𝓝 0) ((⇑f : (a : (i : ι) → E i) → F) ⁻¹' V)
rwa :
  ∀
    (hfV :
      Membership.mem (γ := Filter ((i : ι) → E i)) (Filter.pi (α := E) fun (i : ι) ↦ 𝓝 (0 i))
        ((⇑f : (a : (i : ι) → E i) → F) ⁻¹' V)),
    ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
      (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
        (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
rwa₁ :
  ∀
    (hfV :
      ∃ (I : Set ι),
        I.Finite ∧
          ∃ (t : (i : ι) → Set (E i)),
            (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 (0 i)) (t i)) ∧
              I.pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V),
    ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
      (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
        (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
⊢ ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
    (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
      (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
have rwa₂ : ∀
  (hfV :
    ∃ (s : Finset ι) (t : (i : ι) → Set (E i)),
      (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 (0 i)) (t i)) ∧
        (↑s : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V),
  ∃ (I : Finset ι) (t : (i : ι) → Set (E i)),
    (∀ (i : ι), Membership.mem (γ := Filter (E i)) (𝓝 0) (t i)) ∧
      (↑I : Set ι).pi (α := E) t ⊆ (⇑f : (a : (i : ι) → E i) → F) ⁻¹' V
Tactic: rwa [nhds_pi, Filter.mem_pi, exists_finite_iff_finset] at hfV
Cleared hypotheses: hfV
-- 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 := ⋯ }
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
have 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)
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
-- 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
i : ι
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
have 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
Tactic: rw [isVonNBounded_pi_iff] at hs
Cleared hypotheses: hs, f, V, hV, h₁, x, I, t, ht₀, hft, i
-- 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 : ∀ (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 : ι
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
have this : ∀ᶠ (x : 𝕜) in 𝓝 0, x • eval (β := E) i '' s ⊆ t i
Tactic: have := (hs i).tendsto_smallSets_nhds.eventually (mem_lift' (ht₀ 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 : ∀ (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
⊢ ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
have 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
Tactic: rcases NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff.1 this with ⟨r, hr₀, hr⟩
-- 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 : ∀ (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 : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
have rcases : ∀ (c : 𝕜) (hc₀ : 0 < ‖c‖) (hc : ‖c‖ < r), ∃ (c : 𝕜), c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
Tactic: rcases NormedField.exists_norm_lt 𝕜 hr₀ with ⟨c, hc₀, 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 : ∀ (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
have refine : ∀ (c' : 𝕜) (hle : ‖c'‖ ≤ ‖c‖) (x : (i : ι) → E i) (hx : x ∈ s), c' • x i ∈ t i
Tactic: refine ⟨c, norm_pos_iff.1 hc₀, fun c' hle x hx ↦ ?_⟩
-- 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
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)
have this : ∀ (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⟩