-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
theorem toLp_inj {f g : α →ᵇ E} [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E] :
    toLp (E := E) p μ 𝕜 f = toLp (E := E) p μ 𝕜 g ↔ f = g

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✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ (toLp p μ 𝕜) f = (toLp p μ 𝕜) g ↔ f = g

Tactic:
refine ⟨fun h => ?_, by tauto⟩

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ f = g

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✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ f = g

Tactic:
rw [← DFunLike.coe_fn_eq, ← (map_continuous f).ae_eq_iff_eq μ (map_continuous g)]

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ ⇑f =ᶠ[ae μ] ⇑g

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✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ ↑↑((toLp p μ 𝕜) f) =ᶠ[ae μ] ↑↑((toLp p μ 𝕜) g)

Tactic:
rw [h]

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✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
⊢ f = g → (toLp p μ 𝕜) f = (toLp p μ 𝕜) g

Tactic:
tauto

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✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ ⇑f =ᶠ[ae μ] ⇑g

Tactic:
refine (coeFn_toLp p μ 𝕜 f).symm.trans (EventuallyEq.trans ?_ <| coeFn_toLp p μ 𝕜 g)

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : TopologicalSpace α
inst✝⁷ : BorelSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopologyEither α E
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
f g : α →ᵇ E
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g
⊢ ↑↑((toLp p μ 𝕜) f) =ᶠ[ae μ] ↑↑((toLp p μ 𝕜) g)