awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
⊢ Eq (α := (fb : (ι → R) × B) → C)
    (fun (fb : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) fb.1 : B →ₗ[R] C) : (a : B) → C) fb.2)
    fun (fb : (ι → R) × B) ↦
    ∑ i : ι,
      HSMul.hSMul (β := C) (fb.1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)

Tactic:
have h : (fun fb ↦ bil fb.1 fb.2 : ((ι → R) × B → C)) =
      (fun fb ↦ ∑ i, ((fb.1 i) • (bil (Finsupp.single i 1) fb.2) : C)) := by
    ext ⟨f, b⟩
    nth_rw 1 [← Finset.univ_sum_single f]
    simp_rw [← Finsupp.single_eq_pi_single, map_sum, LinearMap.coe_sum, Finset.sum_apply]
    refine Finset.sum_congr rfl (fun x _ ↦ ?_)
    rw [← Finsupp.smul_single_one]
    push_cast
    simp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
h :
  Eq (α := (fb : (ι → R) × B) → C)
    (fun (fb : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) fb.1 : B →ₗ[R] C) : (a : B) → C) fb.2)
    fun (fb : (ι → R) × B) ↦
    ∑ i : ι,
      HSMul.hSMul (β := C) (fb.1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)
intro :
  Continuous (Y := C) fun (fb : (ι → R) × B) ↦
    ∑ i : ι,
      HSMul.hSMul (β := C) (fb.1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)
⊢ Continuous (Y := C) fun (ab : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2

Tactic:
rw [h]
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
h :
  Eq (α := (fb : (ι → R) × B) → C)
    (fun (fb : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) fb.1 : B →ₗ[R] C) : (a : B) → C) fb.2)
    fun (fb : (ι → R) × B) ↦
    ∑ i : ι,
      HSMul.hSMul (β := C) (fb.1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)
⊢ ContinuousAdd C

Tactic:
haveI : ContinuousAdd C := toContinuousAdd R C
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
B : Type u_2
inst_2 : AddCommMonoid B
inst_3 : Module R B
inst_4 : TopologicalSpace B
inst_5 : IsModuleTopology R B
C : Type u_3
inst_6 : AddCommMonoid C
inst_7 : Module R C
inst_8 : TopologicalSpace C
inst_9 : IsModuleTopology R C
ι : Type u_4
inst_10 : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val : Fintype ι
h :
  Eq (α := (fb : (ι → R) × B) → C)
    (fun (fb : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) fb.1 : B →ₗ[R] C) : (a : B) → C) fb.2)
    fun (fb : (ι → R) × B) ↦
    ∑ i : ι,
      HSMul.hSMul (β := C) (fb.1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)
this : ContinuousAdd C
⊢ Continuous (Y := C) fun (fb : (ι → R) × B) ↦
    ∑ i : ι,
      HSMul.hSMul (β := C) (fb.1 i)
        ((((bil : (a : ι → R) → B →ₗ[R] C) (⇑(Finsupp.single i 1) : (a : ι) → R) : B →ₗ[R] C) : (a : B) → C) fb.2 : C)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
obtain :
  ∀ (m : ℕ) (f : (Fin m → R) →ₗ[R] A)
    (hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin m → R) (β := A) (⇑f : (a : Fin m → R) → A)),
    Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
⊢ Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2

Tactic:
obtain ⟨m, f, hf⟩ := Module.Finite.exists_fin' R A

Premises used: Module.Finite.exists_fin'
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin m → R) (β := A) (⇑f : (a : Fin m → R) → A)
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : Prod.{u_1, u_3} (Fin m → R) B →ₗ[R] A × B := f.prodMap LinearMap.id
⊢ Function.Surjective (α := Prod.{u_1, u_3} (Fin m → R) B) (β := A × B) (⇑φ : (a : (Fin m → R) × B) → A × B)

Tactic:
have hφ : Function.Surjective φ := Function.Surjective.prodMap hf fun b ↦ ⟨b, rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin m → R) (β := A) (⇑f : (a : Fin m → R) → A)
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : Prod.{u_1, u_3} (Fin m → R) B →ₗ[R] A × B := f.prodMap LinearMap.id
hφ : Function.Surjective (α := Prod.{u_1, u_3} (Fin m → R) B) (β := A × B) (⇑φ : (a : (Fin m → R) × B) → A × B)
rw :
  Continuous (X := Prod.{u_1, u_3} (Fin m → R) B) (Y := C)
    ((fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2) ∘
      (⇑φ : (a : (Fin m → R) × B) → A × B))
⊢ Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2

Tactic:
rw [Topology.IsQuotientMap.continuous_iff (isQuotientMap_of_surjective hφ)]

Premises used: IsModuleTopology.isQuotientMap_of_surjective, Topology.IsQuotientMap.continuous_iff
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin m → R) (β := A) (⇑f : (a : Fin m → R) → A)
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : Prod.{u_1, u_3} (Fin m → R) B →ₗ[R] A × B := f.prodMap LinearMap.id
hφ : Function.Surjective (α := Prod.{u_1, u_3} (Fin m → R) B) (β := A × B) (⇑φ : (a : (Fin m → R) × B) → A × B)
⊢ Continuous (X := Prod.{u_1, u_3} (Fin m → R) B) (Y := C)
    ((fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2) ∘
      (⇑φ : (a : (Fin m → R) × B) → A × B))

Tactic:
continuous_bilinear_of_pi_fintype (Fin m) bil'

Premises used: IsModuleTopology.continuous_bilinear_of_pi_fintype, Fin
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin m → R) (β := A) (⇑f : (a : Fin m → R) → A)
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : Prod.{u_1, u_3} (Fin m → R) B →ₗ[R] A × B := f.prodMap LinearMap.id
hφ : Function.Surjective (α := Prod.{u_1, u_3} (Fin m → R) B) (β := A × B) (⇑φ : (a : (Fin m → R) × B) → A × B)
⊢ Continuous (X := Prod.{u_1, u_3} (Fin m → R) B) (Y := C)
    ((fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2) ∘
      (⇑φ : (a : (Fin m → R) × B) → A × B))

Tactic:
exact continuous_bilinear_of_pi_fintype (Fin m) bil'

Premises used: IsModuleTopology.continuous_bilinear_of_pi_fintype, Fin
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
h :
  ∀ (x : A × B),
    Eq.{u_4 + 1} (α := C) ((((bil : (a : A) → B →ₗ[R] C) x.1 : B →ₗ[R] C) : (a : B) → C) x.2 : C)
      (((fun (ba : B × A) ↦ (((bil.flip : (a : B) → A →ₗ[R] C) ba.1 : A →ₗ[R] C) : (a : A) → C) ba.2) ∘ Prod.swap) x :
        C)
⊢ Eq (α := (ab : A × B) → C) (fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2)
    ((fun (ba : B × A) ↦ (((bil.flip : (a : B) → A →ₗ[R] C) ba.1 : A →ₗ[R] C) : (a : A) → C) ba.2) ∘ Prod.swap)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
x : A × B
⊢ Eq.{u_4 + 1} (α := C) ((((bil : (a : A) → B →ₗ[R] C) x.1 : B →ₗ[R] C) : (a : B) → C) x.2 : C)
    (((fun (ba : B × A) ↦ (((bil.flip : (a : B) → A →ₗ[R] C) ba.1 : A →ₗ[R] C) : (a : A) → C) ba.2) ∘ Prod.swap) x : C)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
rw :
  Continuous (X := A × B) (Y := C)
    ((fun (ba : B × A) ↦ (((bil.flip : (a : B) → A →ₗ[R] C) ba.1 : A →ₗ[R] C) : (a : A) → C) ba.2) ∘ Prod.swap)
⊢ Continuous (Y := C) fun (ab : A × B) ↦ (((bil : (a : A) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2

Tactic:
rw [show (fun ab ↦ bil ab.1 ab.2 : (A × B → C)) =
    ((fun ba ↦ bil.flip ba.1 ba.2 : (B × A → C)) ∘ (Prod.swap : A × B → B × A)) by ext; simp]
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsTopologicalRing R
A : Type u_2
inst_3 : AddCommGroup A
inst_4 : Module R A
aA : TopologicalSpace A
inst_5 : IsModuleTopology R A
B : Type u_3
inst_6 : AddCommGroup B
inst_7 : Module R B
aB : TopologicalSpace B
inst_8 : IsModuleTopology R B
C : Type u_4
inst_9 : AddCommGroup C
inst_10 : Module R C
aC : TopologicalSpace C
inst_11 : IsModuleTopology R C
inst_12 : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
⊢ Continuous (X := A × B) (Y := C)
    ((fun (ba : B × A) ↦ (((bil.flip : (a : B) → A →ₗ[R] C) ba.1 : A →ₗ[R] C) : (a : A) → C) ba.2) ∘ Prod.swap)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
D : Type u_2
inst_3 : Ring D
inst_4 : Algebra R D
inst_5 : Module.Finite R D
inst_6 : TopologicalSpace D
inst_7 : IsModuleTopology R D
⊢ Continuous (Y := D) fun (ab : D × D) ↦ ab.1 * ab.2

Tactic:
continuous_bilinear_of_finite_left (LinearMap.mul R D)

Premises used: IsModuleTopology.continuous_bilinear_of_finite_left, LinearMap.mul
-- 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 : MultilinearMap R M₁ M₂
hf : Continuous (f.toFun (M₁ := M₁))
g : MultilinearMap R M₁ M₂
hg : Continuous (g.toFun (M₁ := M₁))
h : (mk (M₁ := M₁) f hf).toMultilinearMap (M₁ := M₁) = (mk (M₁ := M₁) g hg).toMultilinearMap (M₁ := M₁)
subst :
  ∀ (hg : Continuous ((mk (M₁ := M₁) f hf).toMultilinearMap (M₁ := M₁).toFun (M₁ := M₁))),
    mk (M₁ := M₁) f hf = mk (M₁ := M₁) ((mk (M₁ := M₁) f hf).toMultilinearMap (M₁ := M₁)) hg
⊢ mk (M₁ := M₁) f hf = mk (M₁ := M₁) g hg

Tactic:
subst h
-- 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 : MultilinearMap R M₁ M₂
hf : Continuous (f.toFun (M₁ := M₁))
hg : Continuous ((mk (M₁ := M₁) f hf).toMultilinearMap (M₁ := M₁).toFun (M₁ := M₁))
⊢ mk (M₁ := M₁) f hf = mk (M₁ := M₁) ((mk (M₁ := M₁) f hf).toMultilinearMap (M₁ := M₁)) hg

Tactic:
rfl
-- 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₂
⊢ Continuous (X := (i : ι) → M₁ i) (Y := M₂) (⇑f : (a : (i : ι) → M₁ i) → M₂)

Tactic:
f.cont

Premises used: ContinuousMultilinearMap.cont
-- 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₂
⊢ Eq (α := (a : (i : ι) → M₁ i) → M₂) (⇑(f.toMultilinearMap (M₁ := M₁)) : (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 : 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 f' : ContinuousMultilinearMap R M₁ M₂
H :
  ∀ (x : (i : ι) → M₁ i),
    Eq.{w₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂) ((f' : (a : (i : ι) → M₁ i) → M₂) x : M₂)
⊢ f = f'

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- 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 ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + y)) =
    HAdd.hAdd (α := 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.map_update_add' m i x y

Premises used: MultilinearMap.map_update_add', 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₂
f : ContinuousMultilinearMap R M₁ M₂
inst_7 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)

Tactic:
f.map_update_smul' m i c x

Premises used: MultilinearMap.map_update_smul', 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₂
f : ContinuousMultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ Eq.{w₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)

Tactic:
f.toMultilinearMap.map_coord_zero i h

Premises used: ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_coord_zero
-- 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 : Nonempty ι
⊢ Eq.{w₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) 0 : M₂) (0 : M₂)

Tactic:
f.toMultilinearMap.map_zero

Premises used: MultilinearMap.map_zero, 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₂
m : (i : ι) → M₁ i
⊢ Eq.{w₂ + 1} (α := M₂) ((0 : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : 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 : 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₂
⊢ Eq (α := MultilinearMap R M₁ M₂) (toMultilinearMap (M₁ := M₁) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : (i : ι) → AddCommMonoid (M₁ i)
inst_1 : AddCommMonoid M₂
inst_2 : (i : ι) → TopologicalSpace (M₁ i)
inst_3 : TopologicalSpace M₂
R' : Type u_1
A : Type u_3
inst_4 : Semiring A
inst_5 : (i : ι) → Module.{u_3, w₁} A (M₁ i)
inst_6 : Module A M₂
inst_7 : DistribSMul R' M₂
inst_8 : ContinuousConstSMul R' M₂
inst_9 : SMulCommClass A R' M₂
f : ContinuousMultilinearMap A M₁ M₂
c : R'
m : (i : ι) → M₁ i
⊢ (c • f : (a : (i : ι) → M₁ i) → M₂) m = HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic
Goal:
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
inst : (i : ι) → AddCommMonoid (M₁ i)
inst_1 : AddCommMonoid M₂
inst_2 : (i : ι) → TopologicalSpace (M₁ i)
inst_3 : TopologicalSpace M₂
R' : Type u_1
A : Type u_3
inst_4 : Semiring A
inst_5 : (i : ι) → Module.{u_3, w₁} A (M₁ i)
inst_6 : Module A M₂
inst_7 : DistribSMul R' M₂
inst_8 : ContinuousConstSMul R' M₂
inst_9 : SMulCommClass A R' M₂
c : R'
f : ContinuousMultilinearMap A M₁ M₂
⊢ (c • f).toMultilinearMap (M₁ := M₁) = c • f.toMultilinearMap (M₁ := M₁)

Tactic:
rfl

Premises used: rfl
-- 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₄
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : (i : ι) → AddCommMonoid (M₁' i)
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₄
inst_7 : (i : Fin n.succ) → Module.{u, w} R (M i)
inst_8 : (i : ι) → Module.{u, w₁} R (M₁ i)
inst_9 : (i : ι) → Module.{u, w₁'} R (M₁' i)
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R M₄
inst_13 : (i : Fin n.succ) → TopologicalSpace (M i)
inst_14 : (i : ι) → TopologicalSpace (M₁ i)
inst_15 : (i : ι) → TopologicalSpace (M₁' i)
inst_16 : TopologicalSpace M₂
inst_17 : TopologicalSpace M₃
inst_18 : TopologicalSpace M₄
f f' : ContinuousMultilinearMap R M₁ M₂
R' : Type u_1
R'' : Type u_2
A : Type u_3
inst_19 : Semiring A
inst_20 : (i : ι) → Module.{u_3, w₁} A (M₁ i)
inst_21 : Module A M₂
inst_22 : DistribSMul R' M₂
inst_23 : ContinuousConstSMul R' M₂
inst_24 : SMulCommClass A R' M₂
inst_25 : DistribSMul R'' M₂
inst_26 : ContinuousConstSMul R'' M₂
inst_27 : SMulCommClass A R'' M₂
inst_28 : SMulCommClass R' R'' M₂
⊢ SMulCommClass R' R'' (ContinuousMultilinearMap A M₁ M₂)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩

Premises used: ContinuousMultilinearMap.ext, ContinuousMultilinearMap.toMultilinearMap, SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe