-- Mathlib/Topology/Algebra/Module/Basic.lean
theorem LinearMap.continuous_on_pi {ι : Type*} {R : Type*} {M : Type*} [Finite ι] [Semiring R]
    [TopologicalSpace R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M]
    [ContinuousSMul R M] (f : (ι → R) →ₗ[R] M) : Continuous f

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
⊢ Continuous ⇑f

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
⊢ Continuous ⇑f

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
x : ι → R
⊢ f x = ∑ i : ι, x i • f fun j => if i = j then 1 else 0

Tactic:
exact f.pi_apply_eq_sum_univ x

Result:
no goals

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
⊢ Continuous ⇑f

Tactic:
classical
  have : (f : (ι → R) → M) = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0 := by
    ext x
    exact f.pi_apply_eq_sum_univ x
  rw [this]
  refine continuous_finset_sum _ fun i _ => ?_
  exact (continuous_apply i).smul continuous_const

Result:
no goals

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
this : ⇑f = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0
i : ι
x✝ : i ∈ Finset.univ
⊢ Continuous fun x => x i • f fun j => if i = j then 1 else 0

Tactic:
exact (continuous_apply i).smul continuous_const

Result:
no goals

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
this : ⇑f = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0
⊢ Continuous ⇑f

Tactic:
rw [this]

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
this : ⇑f = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0
⊢ Continuous fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
this : ⇑f = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0
⊢ Continuous fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0

Tactic:
refine continuous_finset_sum _ fun i _ => ?_

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
this : ⇑f = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0
i : ι
x✝ : i ∈ Finset.univ
⊢ Continuous fun x => x i • f fun j => if i = j then 1 else 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
⊢ ⇑f = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0

Tactic:
ext x

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
x : ι → R
⊢ f x = ∑ i : ι, x i • f fun j => if i = j then 1 else 0

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
⊢ Continuous ⇑f

Tactic:
have : (f : (ι → R) → M) = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0 := by
  ext x
  exact f.pi_apply_eq_sum_univ x

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
this : ⇑f = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0
⊢ Continuous ⇑f