awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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 : DecidableEq ι
inst_8 : Fintype ι
m m' : (i : ι) → M₁ i
⊢ Eq.{w₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (m + m') : M₂)
    (∑ s : Finset ι, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) m m') : M₂)

Tactic:
f.toMultilinearMap.map_add_univ _ _

Premises used: ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_add_univ
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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₂
α : ι → Type u_1
inst_7 : Fintype ι
g : (i : ι) → α i → M₁ i
A : (i : ι) → Finset (α i)
inst_8 : DecidableEq ι
⊢ Eq.{w₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j ∈ A i, g i j : M₂)
    (∑ r ∈ piFinset (δ := α) A, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)

Tactic:
f.toMultilinearMap.map_sum_finset _ _

Premises used: ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_sum_finset
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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₂
α : ι → Type u_1
inst_7 : Fintype ι
g : (i : ι) → α i → M₁ i
inst_8 : DecidableEq ι
inst_9 : (i : ι) → Fintype (α i)
⊢ Eq.{w₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ ∑ j : α i, g i j : M₂)
    (∑ r : (i : ι) → α i, (f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ g i (r i) : M₂)

Tactic:
f.toMultilinearMap.map_sum _

Premises used: MultilinearMap.map_sum, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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₂
A : Type u_1
inst_7 : Semiring A
inst_8 : SMul R A
inst_9 : (i : ι) → Module.{u_1, w₁} A (M₁ i)
inst_10 : Module A M₂
inst_11 : ∀ (i : ι), IsScalarTower.{u, u_1, w₁} R A (M₁ i)
inst_12 : IsScalarTower R A M₂
f : ContinuousMultilinearMap A M₁ M₂
⊢ Eq (α := (a : (i : ι) → M₁ i) → M₂) (⇑(restrictScalars R (M₁ := M₁) f) : (a : (i : ι) → M₁ i) → M₂)
    (⇑f : (a : (i : ι) → M₁ i) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Ring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup 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 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x - y)) =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)

Tactic:
f.toMultilinearMap.map_update_sub _ _ _ _

Premises used: MultilinearMap.map_update_sub, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Ring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup 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 : IsTopologicalAddGroup M₂
m : (i : ι) → M₁ i
⊢ Eq.{w₂ + 1} (α := M₂) ((-f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (-(f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : Ring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup 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 f' : ContinuousMultilinearMap R M₁ M₂
inst_7 : IsTopologicalAddGroup M₂
m : (i : ι) → M₁ i
⊢ (f - f' : (a : (i : ι) → M₁ i) → M₂) m =
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) ((f' : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Ring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup 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₂
inst_7 : IsTopologicalAddGroup M₂
inst_8 : AddCommGroup M₃
inst_9 : Module R M₃
inst_10 : TopologicalSpace M₃
inst_11 : IsTopologicalAddGroup M₃
f : ContinuousMultilinearMap R M₁ M₂
g : ContinuousMultilinearMap R M₁ M₃
⊢ (-f).prod (M₁ := M₁) (-g) = -f.prod (M₁ := M₁) g

Tactic:
rfl

Premises used: MultilinearMap.prod, ContinuousMultilinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst : Ring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup 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₂
inst_7 : IsTopologicalAddGroup M₂
inst_8 : AddCommGroup M₃
inst_9 : Module R M₃
inst_10 : TopologicalSpace M₃
inst_11 : IsTopologicalAddGroup M₃
f₁ f₂ : ContinuousMultilinearMap R M₁ M₂
g₁ g₂ : ContinuousMultilinearMap R M₁ M₃
⊢ (f₁ - f₂).prod (M₁ := M₁) (g₁ - g₂) = f₁.prod (M₁ := M₁) g₁ - f₂.prod (M₁ := M₁) g₂

Tactic:
rfl

Premises used: MultilinearMap.prod, ContinuousMultilinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : CommSemiring 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 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s : Finset ι
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{u, w₂, w₂} (α := R) (β := M₂) (∏ i ∈ s, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
f.toMultilinearMap.map_piecewise_smul _ _ _

Premises used: MultilinearMap.map_piecewise_smul, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : CommSemiring 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 : Fintype ι
c : ι → R
m : (i : ι) → M₁ i
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (i : ι) ↦ c i • m i) =
    HSMul.hSMul.{u, w₂, w₂} (α := R) (β := M₂) (∏ i : ι, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
f.toMultilinearMap.map_smul_univ _ _

Premises used: ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_smul_univ
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
M₂ : Type w₂
inst : CommSemiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : TopologicalSpace M₂
inst_4 : Finite ι
inst_5 : TopologicalSpace R
f g : ContinuousMultilinearMap R (fun (x : ι) ↦ R) M₂
h :
  Eq.{w₂ + 1} (α := M₂) ((f : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
    ((g : (a : (i : ι) → R) → M₂) fun (x : ι) ↦ 1 : M₂)
⊢ f = g

Tactic:
toMultilinearMap_injective <| MultilinearMap.ext_ring h

Premises used: MultilinearMap.ext_ring, ContinuousMultilinearMap.toMultilinearMap_injective
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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
change : Continuous (Y := A) fun (m : Fin n → A) ↦ (List.ofFn m).prod
⊢ Continuous (MultilinearMap.toFun (M₁ := fun (i : Fin n) ↦ A) (MultilinearMap.mkPiAlgebraFin R n A))

Tactic:
change Continuous fun m => (List.ofFn m).prod

Premises used: Continuous, List.ofFn, List.prod
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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
simp_rw : Continuous (Y := A) fun (m : Fin n → A) ↦ (List.map m (List.finRange n)).prod
⊢ Continuous (Y := A) fun (m : Fin n → A) ↦ (List.ofFn m).prod

Tactic:
simp_rw [List.ofFn_eq_map]

Premises used: List.ofFn_eq_map
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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.map m (List.finRange n)).prod

Tactic:
continuous_list_prod _ fun i _ => continuous_apply _

Premises used: continuous_list_prod, continuous_apply
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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.map m (List.finRange n)).prod

Tactic:
exact continuous_list_prod _ fun i _ => continuous_apply _

Premises used: continuous_list_prod, continuous_apply
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
n : ℕ
A : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : TopologicalSpace A
inst_4 : ContinuousMul A
m : Fin n → A
⊢ (ContinuousMultilinearMap.mkPiAlgebraFin R n A : (a : (i : Fin n) → A) → A) m = (List.ofFn m).prod

Tactic:
rfl

Premises used: rfl, List.prod
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
R : Type u
ι : Type v
A : Type u_1
inst : Fintype ι
inst_1 : CommSemiring R
inst_2 : CommSemiring A
inst_3 : Algebra R A
inst_4 : TopologicalSpace A
inst_5 : ContinuousMul A
m : ι → A
⊢ Eq.{u_1 + 1} (α := A) ((ContinuousMultilinearMap.mkPiAlgebra R ι A : (a : (i : ι) → A) → A) m : A) (∏ i : ι, m i : A)

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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 : ℕ
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)
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : Fin n) ↦ A) A) (ContinuousMultilinearMap.mkPiAlgebra R (Fin n) A)
    (ContinuousMultilinearMap.mkPiAlgebraFin R n A)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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 : ℕ
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:
simp [List.prod_ofFn]

Premises used: List.prod_ofFn
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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
m : ι → R
⊢ (ContinuousMultilinearMap.mkPiRing R ι z : (a : (i : ι) → R) → M) m =
    HSMul.hSMul.{u, u_1, u_1} (α := R) (∏ i : ι, m i) z

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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
f : ContinuousMultilinearMap R (fun (x : ι) ↦ R) M
⊢ ContinuousMultilinearMap.mkPiRing R ι ((f : (a : (i : ι) → R) → M) fun (x : ι) ↦ 1) = f

Tactic:
toMultilinearMap_injective f.toMultilinearMap.mkPiRing_apply_one_eq_self

Premises used: ContinuousMultilinearMap.toMultilinearMap, ContinuousMultilinearMap.toMultilinearMap_injective, MultilinearMap.mkPiRing_apply_one_eq_self
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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
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₂
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι z₁)
      (ContinuousMultilinearMap.mkPiRing R ι z₂) ↔
    z₁ = z₂

Tactic:
rw [← toMultilinearMap_injective.eq_iff]

Premises used: Function.Injective.eq_iff, ContinuousMultilinearMap.toMultilinearMap_injective
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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 (α := 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:
MultilinearMap.mkPiRing_eq_iff

Premises used: MultilinearMap.smulRight, MultilinearMap.mkPiRing, LinearMap.compMultilinearMap, MultilinearMap.mkPiRing_eq_iff
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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 (α := 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:
exact MultilinearMap.mkPiRing_eq_iff

Premises used: MultilinearMap.mkPiRing_eq_iff
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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 :
  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)
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι 0) 0

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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)
h₂ h₃ : Eq.{u_1 + 1} (α := M) 0 0
⊢ 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:
rw [mkPiRing_apply, smul_zero, ContinuousMultilinearMap.zero_apply]

Premises used: ContinuousMultilinearMap.mkPiRing_apply, smul_zero, ContinuousMultilinearMap.zero_apply
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
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
rw₁ rw₂ : z = 0 ↔ z = 0
⊢ Eq (α := ContinuousMultilinearMap R (fun (x : ι) ↦ R) M) (ContinuousMultilinearMap.mkPiRing R ι z) 0 ↔ z = 0

Tactic:
rw [← mkPiRing_zero, mkPiRing_eq_iff]

Premises used: ContinuousMultilinearMap.mkPiRing_zero, ContinuousMultilinearMap.mkPiRing_eq_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 : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
h₁ : ∀ (c : 𝕜), ‖c‖ ≤ 1
c : 𝕜
hc : 2 ≤ ‖c‖
linarith : -1 + (2 - ‖c‖) + (‖c‖ - 1) = 0
⊢ (⇑f : (a : (i : ι) → E i) → F) '' s ⊆ c • V

Tactic:
linarith [h₁ c]
-- 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
⊢ Absorbs 𝕜 V ((⇑f : (a : (i : ι) → E i) → F) '' s)

Tactic:
exact absorbs_iff_norm.2 ⟨2, fun c hc ↦ by linarith [h₁ c]⟩

Premises used: Iff.mpr, absorbs_iff_norm, Exists.intro, OfNat.ofNat
-- 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 < ‖x‖

Tactic:
simpa using h₁
-- 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 := ⋯ }
⊢ 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
-- 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 := ⋯ }
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
rwa₂ rwa₃ rwa₄ 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
⊢ ∃ (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

Premises used: nhds_pi, Set.exists_finite_iff_finset, Filter.mem_pi