-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essSup_map_measure (hg : AEMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
h_eq : (fun x => g (f x)) =ᶠ[ae μ] fun x => AEMeasurable.mk g hg (f x)
⊢ AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f

Tactic:
exact h_eq.symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
rw [essSup_congr_ae hg.ae_eq_mk, essSup_map_measure_of_measurable hg.measurable_mk hf]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ

Tactic:
refine essSup_congr_ae ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f

Tactic:
have h_eq := ae_of_ae_map hf hg.ae_eq_mk

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
h_eq : ∀ᵐ (x : α) ∂μ, g (f x) = AEMeasurable.mk g hg (f x)
⊢ AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
h_eq : ∀ᵐ (x : α) ∂μ, g (f x) = AEMeasurable.mk g hg (f x)
⊢ AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f

Tactic:
rw [← EventuallyEq] at h_eq

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
h_eq : (fun x => g (f x)) =ᶠ[ae μ] fun x => AEMeasurable.mk g hg (f x)
⊢ AEMeasurable.mk g hg ∘ f =ᶠ[ae μ] g ∘ f