-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
theorem range_toLp [NormedField 𝕜] [NormedSpace 𝕜 E] :
    (LinearMap.range (toLp p μ 𝕜 : C(α, E) →L[𝕜] Lp E p μ)).toAddSubgroup =
      MeasureTheory.Lp.boundedContinuousFunction E p μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ ↑(LinearMap.range (toLp p μ 𝕜)).toAddSubgroup = ↑(Lp.boundedContinuousFunction E p μ)

Tactic:
have := (linearIsometryBoundedOfCompact α E 𝕜).surjective

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
this : Function.Surjective ⇑(linearIsometryBoundedOfCompact α E 𝕜)
⊢ ↑(LinearMap.range (toLp p μ 𝕜)).toAddSubgroup = ↑(Lp.boundedContinuousFunction E p μ)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
this : Function.Surjective ⇑(linearIsometryBoundedOfCompact α E 𝕜)
⊢ ↑(LinearMap.range (toLp p μ 𝕜)).toAddSubgroup = ↑(Lp.boundedContinuousFunction E p μ)

Tactic:
convert Function.Surjective.range_comp this (BoundedContinuousFunction.toLp (E := E) p μ 𝕜)

Result:
case h.e'_3
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
this : Function.Surjective ⇑(linearIsometryBoundedOfCompact α E 𝕜)
⊢ ↑(Lp.boundedContinuousFunction E p μ) = Set.range ⇑(BoundedContinuousFunction.toLp p μ 𝕜)

Proof state:
case h.e'_3
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
this : Function.Surjective ⇑(linearIsometryBoundedOfCompact α E 𝕜)
⊢ ↑(Lp.boundedContinuousFunction E p μ) = Set.range ⇑(BoundedContinuousFunction.toLp p μ 𝕜)

Tactic:
rw [← BoundedContinuousFunction.range_toLp p μ (𝕜 := 𝕜), Submodule.coe_toAddSubgroup,
  LinearMap.range_coe]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ (LinearMap.range (toLp p μ 𝕜)).toAddSubgroup = Lp.boundedContinuousFunction E p μ

Tactic:
refine SetLike.ext' ?_

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : CompactSpace α
inst✝³ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝² : Fact (1 ≤ p)
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ ↑(LinearMap.range (toLp p μ 𝕜)).toAddSubgroup = ↑(Lp.boundedContinuousFunction E p μ)