-- Mathlib/Topology/Algebra/Module/ModuleTopology.lean
theorem continuous_bilinear_of_pi_fintype (ι : Type*) [Finite ι]
    (bil : (ι → R) →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : ((ι → R) × B → C))

Proof state:
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
⊢ (fun fb => (bil fb.1) fb.2) = fun fb => ∑ i : ι, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2

Tactic:
ext ⟨f, b⟩

Result:
case h.mk
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
⊢ (bil (f, b).1) (f, b).2 = ∑ i : ι, (f, b).1 i • (bil ⇑(Finsupp.single i 1)) (f, b).2

Proof state:
case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
h : (fun fb => (bil fb.1) fb.2) = fun fb => ∑ i : ι, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2
⊢ Continuous fun fb => ∑ i : ι, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2

Tactic:
haveI : ContinuousAdd C := toContinuousAdd R C

Result:
case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
h : (fun fb => (bil fb.1) fb.2) = fun fb => ∑ i : ι, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2
this : ContinuousAdd C
⊢ Continuous fun fb => ∑ i : ι, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2

Proof state:
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
⊢ Continuous fun ab => (bil ab.1) ab.2

Tactic:
classical
cases nonempty_fintype ι
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.coeFn_sum, Finset.sum_apply]
  refine Finset.sum_congr rfl (fun x _ ↦ ?_)
  rw [← Finsupp.smul_single_one]
  push_cast
  simp
rw [h]
haveI : ContinuousAdd C := toContinuousAdd R C
fun_prop

Result:
no goals

Proof state:
case h.mk
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
⊢ ∑ c : ι, (bil ⇑(Finsupp.single c (f c))) b = ∑ x : ι, f x • (bil ⇑(Finsupp.single x 1)) b

Tactic:
refine Finset.sum_congr rfl (fun x _ ↦ ?_)

Result:
case h.mk
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil ⇑(Finsupp.single x (f x))) b = f x • (bil ⇑(Finsupp.single x 1)) b

Proof state:
case h.mk
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil ⇑(f x • Finsupp.single x 1)) b = f x • (bil ⇑(Finsupp.single x 1)) b

Tactic:
push_cast

Result:
case h.mk
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil (f x • ⇑(Finsupp.single x 1))) b = f x • (bil ⇑(Finsupp.single x 1)) b

Proof state:
case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
h : (fun fb => (bil fb.1) fb.2) = fun fb => ∑ i : ι, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2
this : ContinuousAdd C
⊢ Continuous fun fb => ∑ i : ι, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2

Tactic:
fun_prop

Result:
no goals

Proof state:
case h.mk
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
⊢ (bil (f, b).1) (f, b).2 = ∑ i : ι, (f, b).1 i • (bil ⇑(Finsupp.single i 1)) (f, b).2

Tactic:
nth_rw 1 [← Finset.univ_sum_single f]

Result:
case h.mk
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
⊢ (bil (∑ i : ι, Pi.single i (f i), b).1) (f, b).2 = ∑ i : ι, (f, b).1 i • (bil ⇑(Finsupp.single i 1)) (f, b).2