-- Lean 4 proof step from Mathlib.Analysis.Distribution.TestFunction (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n : ℕ∞
V : Type u_6
inst_6 : AddCommGroup V
inst_7 : Module ℝ V
t : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul ℝ V
inst_10 : LocallyConvexSpace ℝ V
inst_11 : Algebra ℝ 𝕜
inst_12 : IsScalarTower ℝ 𝕜 F
inst_13 : Module 𝕜 V
inst_14 : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this_1 : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this_2 : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
this : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
simp_rw :
  LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (originalTop Ω F n)
      (induced
        (⇑((↑ℝ :
                {S : Type u_1} →
                  {M : Type (max u_3 u_4)} →
                    {M₂ : Type u_6} →
                      [inst : Semiring ℝ] →
                        [inst_15 : Semiring S] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module ℝ M] →
                                [inst_19 : Module ℝ M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              f) :
          (a : 𝓓^{n}(Ω, F)) → V)
        t) ↔
    ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
      Continuous[_, t]
        ((⇑((↑ℝ :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_4)} →
                      {M₂ : Type u_6} →
                        [inst : Semiring ℝ] →
                          [inst_15 : Semiring S] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module ℝ M] →
                                  [inst_19 : Module ℝ M₂] →
                                    [inst_20 : Module S M] →
                                      [inst_21 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                f) :
            (a : 𝓓^{n}(Ω, F)) → V) ∘
          ofSupportedIn K_sub_Ω)
simp_rw₁ :
  LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F))
      (⨆ (K : Compacts E),
        ⨆ (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
          coinduced (ofSupportedIn K_sub_Ω) ContDiffMapSupportedIn.topologicalSpace)
      (induced
        (⇑((↑ℝ :
                {S : Type u_1} →
                  {M : Type (max u_3 u_4)} →
                    {M₂ : Type u_6} →
                      [inst : Semiring ℝ] →
                        [inst_15 : Semiring S] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module ℝ M] →
                                [inst_19 : Module ℝ M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              f) :
          (a : 𝓓^{n}(Ω, F)) → V)
        t) ↔
    ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
      Continuous[_, t]
        ((⇑((↑ℝ :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_4)} →
                      {M₂ : Type u_6} →
                        [inst : Semiring ℝ] →
                          [inst_15 : Semiring S] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module ℝ M] →
                                  [inst_19 : Module ℝ M₂] →
                                    [inst_20 : Module S M] →
                                      [inst_21 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                f) :
            (a : 𝓓^{n}(Ω, F)) → V) ∘
          ofSupportedIn K_sub_Ω)
simp_rw₂ :
  (∀ (i : Compacts E) (j : (↑i : Set E) ⊆ (↑Ω : Set E)),
      LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (coinduced (ofSupportedIn j) ContDiffMapSupportedIn.topologicalSpace)
        (induced
          (⇑((↑ℝ :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_4)} →
                      {M₂ : Type u_6} →
                        [inst : Semiring ℝ] →
                          [inst_15 : Semiring S] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module ℝ M] →
                                  [inst_19 : Module ℝ M₂] →
                                    [inst_20 : Module S M] →
                                      [inst_21 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                f) :
            (a : 𝓓^{n}(Ω, F)) → V)
          t)) ↔
    ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
      Continuous[_, t]
        ((⇑((↑ℝ :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_4)} →
                      {M₂ : Type u_6} →
                        [inst : Semiring ℝ] →
                          [inst_15 : Semiring S] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module ℝ M] →
                                  [inst_19 : Module ℝ M₂] →
                                    [inst_20 : Module S M] →
                                      [inst_21 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                f) :
            (a : 𝓓^{n}(Ω, F)) → V) ∘
          ofSupportedIn K_sub_Ω)
⊢ LE.le (α := TopologicalSpace 𝓓^{n}(Ω, F)) (topologicalSpace Ω F n)
      (induced
        (⇑((↑ℝ :
                {S : Type u_1} →
                  {M : Type (max u_3 u_4)} →
                    {M₂ : Type u_6} →
                      [inst : Semiring ℝ] →
                        [inst_15 : Semiring S] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module ℝ M] →
                                [inst_19 : Module ℝ M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              f) :
          (a : 𝓓^{n}(Ω, F)) → V)
        t) ↔
    ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
      Continuous[_, t]
        ((⇑((↑ℝ :
                  {S : Type u_1} →
                    {M : Type (max u_3 u_4)} →
                      {M₂ : Type u_6} →
                        [inst : Semiring ℝ] →
                          [inst_15 : Semiring S] →
                            [inst_16 : AddCommMonoid M] →
                              [inst_17 : AddCommMonoid M₂] →
                                [inst_18 : Module ℝ M] →
                                  [inst_19 : Module ℝ M₂] →
                                    [inst_20 : Module S M] →
                                      [inst_21 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                f) :
            (a : 𝓓^{n}(Ω, F)) → V) ∘
          ofSupportedIn K_sub_Ω)
have simp_rw₃ : (∀ (i : Compacts E) (j : (↑i : Set E) ⊆ (↑Ω : Set E)),
    Continuous[coinduced (ofSupportedIn j) ContDiffMapSupportedIn.topologicalSpace, t]
      (⇑((↑ℝ :
              {S : Type u_1} →
                {M : Type (max u_3 u_4)} →
                  {M₂ : Type u_6} →
                    [inst : Semiring ℝ] →
                      [inst_15 : Semiring S] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module ℝ M] →
                              [inst_19 : Module ℝ M₂] →
                                [inst_20 : Module S M] →
                                  [inst_21 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
            f) :
        (a : 𝓓^{n}(Ω, F)) → V)) ↔
  ∀ (K : Compacts E) (K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)),
    Continuous[_, t]
      ((⇑((↑ℝ :
                {S : Type u_1} →
                  {M : Type (max u_3 u_4)} →
                    {M₂ : Type u_6} →
                      [inst : Semiring ℝ] →
                        [inst_15 : Semiring S] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module ℝ M] →
                                [inst_19 : Module ℝ M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              f) :
          (a : 𝓓^{n}(Ω, F)) → V) ∘
        ofSupportedIn K_sub_Ω)
Tactic: simp_rw [topologicalSpace_le_iff, originalTop, iSup₂_le_iff, ← continuous_iff_le_induced,
    continuous_coinduced_dom]