-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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
intro :
  ∀ (val : Fintype ι),
    Continuous (Y := C) fun (ab : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
intro₁ :
  ∀ (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)),
    Continuous (Y := C) fun (ab : (ι → R) × B) ↦ (((bil : (a : ι → R) → B →ₗ[R] C) ab.1 : B →ₗ[R] C) : (a : B) → C) ab.2
intro₂ :
  ∀ (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)),
    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
have intro₃ : ∀ (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: classical
  cases nonempty_fintype ι
  -- The map in question, `(f, b) ↦ bil f b`, is easily checked to be equal to
  -- `(f, b) ↦ ∑ᵢ f i • bil (single i 1) b` where `single i 1 : ι → R` sends `i` to `1` and
  -- everything else to `0`.
  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
  rw [h]
  -- But this map is obviously continuous, because for a fixed `i`, `bil (single i 1)` is
  -- linear and thus continuous, and scalar multiplication and finite sums are continuous
  haveI : ContinuousAdd C := toContinuousAdd R C
  fun_prop