[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : CommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective ↑B
⊢ Tendsto f l (𝓝 x) ↔ ∀ (y : F), Tendsto (fun i => ↑(↑B (f i)) y) l (𝓝 (↑(↑B x) y))
[PROOFSTEP]
rw [← tendsto_pi_nhds, Embedding.tendsto_nhds_iff (embedding hB)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : CommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective ↑B
⊢ Tendsto ((fun x y => ↑(↑B x) y) ∘ f) l (𝓝 fun y => ↑(↑B x) y) ↔
    Tendsto (fun i y => ↑(↑B (f i)) y) l (𝓝 fun y => ↑(↑B x) y)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ ContinuousAdd (WeakBilin B)
[PROOFSTEP]
refine' ⟨continuous_induced_rng.2 _⟩
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ Continuous ((fun x y => ↑(↑B x) y) ∘ fun p => p.fst + p.snd)
[PROOFSTEP]
refine' cast (congr_arg _ _) (((coeFn_continuous B).comp continuous_fst).add ((coeFn_continuous B).comp continuous_snd))
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ (fun x => ((fun x y => ↑(↑B x) y) ∘ Prod.fst) x + ((fun x y => ↑(↑B x) y) ∘ Prod.snd) x) =
    (fun x y => ↑(↑B x) y) ∘ fun p => p.fst + p.snd
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
x✝¹ : WeakBilin B × WeakBilin B
x✝ : F
⊢ (((fun x y => ↑(↑B x) y) ∘ Prod.fst) x✝¹ + ((fun x y => ↑(↑B x) y) ∘ Prod.snd) x✝¹) x✝ =
    ((fun x y => ↑(↑B x) y) ∘ fun p => p.fst + p.snd) x✝¹ x✝
[PROOFSTEP]
simp only [Function.comp_apply, Pi.add_apply, map_add, LinearMap.add_apply]
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ ContinuousSMul 𝕜 (WeakBilin B)
[PROOFSTEP]
refine' ⟨continuous_induced_rng.2 _⟩
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ Continuous ((fun x y => ↑(↑B x) y) ∘ fun p => p.fst • p.snd)
[PROOFSTEP]
refine' cast (congr_arg _ _) (continuous_fst.smul ((coeFn_continuous B).comp continuous_snd))
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ (fun x => x.fst • ((fun x y => ↑(↑B x) y) ∘ Prod.snd) x) = (fun x y => ↑(↑B x) y) ∘ fun p => p.fst • p.snd
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
x✝¹ : 𝕜 × WeakBilin B
x✝ : F
⊢ (x✝¹.fst • ((fun x y => ↑(↑B x) y) ∘ Prod.snd) x✝¹) x✝ = ((fun x y => ↑(↑B x) y) ∘ fun p => p.fst • p.snd) x✝¹ x✝
[PROOFSTEP]
simp only [Function.comp_apply, Pi.smul_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, LinearMap.smul_apply]
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ ContinuousAdd (WeakBilin B)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ Continuous fun a => -a
[PROOFSTEP]
refine' continuous_induced_rng.2 (continuous_pi_iff.mpr fun y => _)
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
⊢ Continuous fun a => ((fun x y => ↑(↑B x) y) ∘ fun a => -a) a y
[PROOFSTEP]
refine' cast (congr_arg _ _) (eval_continuous B (-y))
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
⊢ (fun x => ↑(↑B x) (-y)) = fun a => ((fun x y => ↑(↑B x) y) ∘ fun a => -a) a y
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ ↑(↑B x) (-y) = ((fun x y => ↑(↑B x) y) ∘ fun a => -a) x y
[PROOFSTEP]
simp only [map_neg, Function.comp_apply, LinearMap.neg_apply]
  -- Porting note: mathlib3 proof was done here
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ -↑(↑B x) y = ↑(↑B (-x)) y
[PROOFSTEP]
rw [← (B x).neg_apply]
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ ↑(-↑B x) y = ↑(↑B (-x)) y
[PROOFSTEP]
congr
[GOAL]
case h.e_a
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ -↑B x = ↑B (-x)
[PROOFSTEP]
exact (map_neg B x).symm
