awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
inst_3 : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c

Tactic:
h.ae_eq_const_of_ae_eq_comp_of_ae_range₀ (s := univ) univ_mem hgm hg_eq

Premises used: QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀, Filter.univ_mem
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : Nonempty X
inst_2 : MeasurableSpace X
inst_3 : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : Ergodic f μ
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c

Tactic:
h.quasiErgodic.ae_eq_const_of_ae_eq_comp₀ hgm hg_eq

Premises used: Ergodic.quasiErgodic, QuasiErgodic.ae_eq_const_of_ae_eq_comp₀
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ let this := borel X;
  BorelSpace X

Tactic:
borelize X
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
rcases : ∀ (t : Set X) (ht : IsSeparable t) (hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t), ∃ (c : X), g =ᶠ[ae μ] const α c
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c

Tactic:
rcases hgm.isSeparable_ae_range with ⟨t, ht, hgt⟩

Premises used: MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this : MeasurableSpace X := borel X
this_1 : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ SecondCountableTopology.{u_2} (↑t : Type u_2)

Tactic:
haveI := ht.secondCountableTopology
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
this : SecondCountableTopology.{u_2} (↑t : Type u_2)
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c

Tactic:
h.ae_eq_const_of_ae_eq_comp_of_ae_range₀ hgt hgm.aemeasurable.nullMeasurable hg_eq

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.nullMeasurable, QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
this_1 : MeasurableSpace X := borel X
this_2 : BorelSpace X
t : Set X
ht : IsSeparable t
hgt : ∀ᵐ (x : α) ∂μ, g x ∈ t
this : SecondCountableTopology.{u_2} (↑t : Type u_2)
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c

Tactic:
exact h.ae_eq_const_of_ae_eq_comp_of_ae_range₀ hgt hgm.aemeasurable.nullMeasurable hg_eq

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.nullMeasurable, QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
h : QuasiErgodic f μ
g : α →ₘ[μ] X
hg_eq : g.compQuasiMeasurePreserving f ⋯ = g
⊢ ∃ (c : X), g = AEEqFun.const α c

Tactic:
have : g ∘ f =ᵐ[μ] g := (g.coeFn_compQuasiMeasurePreserving h.1).symm.trans
    (hg_eq.symm ▸ .refl _ _)
  let ⟨c, hc⟩ := h.ae_eq_const_of_ae_eq_comp_ae g.aestronglyMeasurable this
  ⟨c, AEEqFun.ext <| hc.trans (AEEqFun.coeFn_const _ _).symm⟩

Premises used: MeasureTheory.ae, Filter.EventuallyEq.trans, MeasureTheory.AEEqFun.cast, QuasiErgodic.toQuasiMeasurePreserving, MeasureTheory.AEEqFun.coeFn_const, Exists, MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving, Eq.rec, QuasiErgodic.ae_eq_const_of_ae_eq_comp_ae, _private.0.QuasiErgodic.eq_const_of_compQuasiMeasurePreserving_eq.match_1, Filter.EventuallyEq.refl, Exists.intro, MeasureTheory.AEEqFun.aestronglyMeasurable, MeasureTheory.AEEqFun.ext, Eq.symm, Eq, Filter.EventuallyEq.symm, MeasureTheory.AEEqFun.const
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
g : α → X
h : Ergodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᶠ[ae μ] g
⊢ ∃ (c : X), g =ᶠ[ae μ] const α c

Tactic:
h.quasiErgodic.ae_eq_const_of_ae_eq_comp_ae hgm hg_eq

Premises used: QuasiErgodic.ae_eq_const_of_ae_eq_comp_ae, Ergodic.quasiErgodic
-- Module: Mathlib.Dynamics.Ergodic.Function
Goal:
α : Type u_1
X : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace X
inst_2 : MetrizableSpace X
inst_3 : Nonempty X
f : α → α
h : Ergodic f μ
g : α →ₘ[μ] X
hg_eq : g.compMeasurePreserving f ⋯ = g
⊢ ∃ (c : X), g = AEEqFun.const α c

Tactic:
h.quasiErgodic.eq_const_of_compQuasiMeasurePreserving_eq hg_eq

Premises used: QuasiErgodic.eq_const_of_compQuasiMeasurePreserving_eq, Ergodic.quasiErgodic
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
h : Measurable f
μa : Measure α
⊢ MeasurePreserving f μa (map f μa)

Tactic:
⟨h, rfl⟩

Premises used: MeasureTheory.MeasurePreserving.mk, rfl
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
⊢ MeasurePreserving id μ μ

Tactic:
⟨measurable_id, map_id⟩

Premises used: MeasureTheory.Measure.map_id, measurable_id, MeasureTheory.MeasurePreserving.mk
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
⊢ AEMeasurable f μa

Tactic:
hf.1.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
⊢ MeasurePreserving f' μa μb

Tactic:
⟨hf', ?_⟩

Premises used: MeasureTheory.MeasurePreserving.mk
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
refine : map f' μa = μb
⊢ MeasurePreserving f' μa μb

Tactic:
refine ⟨hf', ?_⟩
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
rw : map f μa = μb
⊢ map f' μa = μb

Tactic:
rw [Measure.map_congr h.symm]

Premises used: MeasureTheory.Measure.map_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
⊢ map f μa = μb

Tactic:
hf.map_eq

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
⊢ map f μa = μb

Tactic:
exact hf.map_eq

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : IsEmpty β
f : α → β
μa : Measure α
μb : Measure β
⊢ MeasurePreserving f μa μb

Tactic:
⟨measurable_of_subsingleton_codomain _, Subsingleton.elim _ _⟩

Premises used: MeasureTheory.MeasurePreserving.mk, measurable_of_subsingleton_codomain, Subsingleton.elim
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e : (a : α) → β) μa μb
rw : map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) μa) = μa
rw₁ : map (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) μa = μa
rw₂ : map id μa = μa
rw₃ rw₄ : μa = μa
⊢ map (⇑e.symm : (a : β) → α) μb = μa

Tactic:
rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]

Premises used: MeasureTheory.Measure.map_id, MeasurableEquiv.symm, MeasureTheory.MeasurePreserving.map_eq, MeasurableEquiv.symm_comp_self, MeasurableEquiv.measurable, MeasureTheory.Measure.map_map
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : MeasurableSet s
rw : Eq (α := Measure β) (map f (μa.restrict (f ⁻¹' s))) (Measure.restrict (map f μa) s)
rw₁ rw₂ : Eq (α := Measure β) (map f (μa.restrict (f ⁻¹' s))) (map f (μa.restrict (f ⁻¹' s)))
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s

Tactic:
rw [← hf.map_eq, restrict_map hf.measurable hs]

Premises used: MeasureTheory.Measure.restrict_map, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
s : Set β
rw : Eq (α := Measure β) (map f (μa.restrict (f ⁻¹' s))) (Measure.restrict (map f μa) s)
rw₁ rw₂ : Eq (α := Measure β) (map f (μa.restrict (f ⁻¹' s))) (map f (μa.restrict (f ⁻¹' s)))
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s

Tactic:
rw [← hf.map_eq, h₂.restrict_map]

Premises used: MeasurableEmbedding.restrict_map, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
s : Set α
⊢ MeasurePreserving f (μa.restrict s) (μb.restrict (f '' s))

Tactic:
simpa only [Set.preimage_image_eq _ h₂.injective] using hf.restrict_preimage_emb h₂ (f '' s)

Premises used: MeasurableEmbedding.injective, Set.preimage_image_eq, Set.image, MeasureTheory.MeasurePreserving.restrict_preimage_emb
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
rw : AEMeasurable (g ∘ f) μa ↔ AEMeasurable (_m := inst_1) g (map f μa)
rw₁ rw₂ : AEMeasurable (g ∘ f) μa ↔ AEMeasurable (g ∘ f) μa
⊢ AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb

Tactic:
rw [← hf.map_eq, h₂.aemeasurable_map_iff]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasurableEmbedding.aemeasurable_map_iff
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
⊢ QuasiMeasurePreserving f μa μb

Tactic:
⟨hf.1, hf.2.absolutelyContinuous⟩

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasureTheory.MeasurePreserving.map_eq, Eq.absolutelyContinuous, MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : MeasurePreserving g μb μc
hf : MeasurePreserving f μa μb
rw : map g (map f μa) = μc
rw₁ : map g μb = μc
rw₂ rw₃ : μc = μc
⊢ map (g ∘ f) μa = μc

Tactic:
rw [← map_map hg.1 hf.1, hf.2, hg.2]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.MeasurePreserving.measurable, MeasureTheory.Measure.map_map
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μc : Measure γ
f : α → β
g : β → γ
hgf : MeasurePreserving (g ∘ f) μa μc
hg : Measurable g
hf : Measurable f
⊢ MeasurePreserving g (map f μa) μc

Tactic:
⟨hg, (map_map hg hf).trans hgf.map_eq⟩

Premises used: MeasureTheory.MeasurePreserving.mk, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.Measure.map_map, Eq.trans
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
ga : α → α
gb : β → β
hfm : MeasurePreserving f μa μb
hga : MeasurePreserving ga μa μa
hf : Semiconj f ga gb
hgb : Measurable gb
⊢ MeasurePreserving gb (map f μa) μb

Tactic:
have := hf.comp_eq ▸ hfm.comp hga |>.map_of_comp hgb hfm.measurable
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
ga : α → α
gb : β → β
hfm : MeasurePreserving f μa μb
hga : MeasurePreserving ga μa μa
hf : Semiconj f ga gb
hgb : Measurable gb
this : MeasurePreserving gb (map f μa) μb
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : MeasurePreserving gb μb μb), MeasurePreserving gb μb μb
⊢ MeasurePreserving gb μb μb

Tactic:
rwa [hfm.map_eq] at this

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
e : α ≃ᵐ β
e' : β ≃ᵐ γ
μa : Measure α
μb : Measure β
μc : Measure γ
h : MeasurePreserving (⇑e : (a : α) → β) μa μb
h' : MeasurePreserving (⇑e' : (a : β) → γ) μb μc
⊢ MeasurePreserving (⇑(e.trans e') : (a : α) → γ) μa μc

Tactic:
h'.comp h

Premises used: MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e : (a : β) → γ) μb μc
⊢ MeasurePreserving ((⇑e : (a : β) → γ) ∘ g) μa μc ↔ MeasurePreserving g μa μb

Tactic:
⟨fun hg => ?_, fun hg => h.comp hg⟩

Premises used: Iff.intro, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e : (a : β) → γ) μb μc
refine : ∀ (hg : MeasurePreserving ((⇑e : (a : β) → γ) ∘ g) μa μc), MeasurePreserving g μa μb
⊢ MeasurePreserving ((⇑e : (a : β) → γ) ∘ g) μa μc ↔ MeasurePreserving g μa μb

Tactic:
refine ⟨fun hg => ?_, fun hg => h.comp hg⟩
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e : (a : β) → γ) μb μc
hg : MeasurePreserving ((⇑e : (a : β) → γ) ∘ g) μa μc
⊢ MeasurePreserving (comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := γ) (⇑e.symm : (a : γ) → β) ((⇑e : (a : β) → γ) ∘ g)) μa μb

Tactic:
(MeasurePreserving.symm e h).comp hg

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e : (a : β) → γ) μb μc
hg : MeasurePreserving ((⇑e : (a : β) → γ) ∘ g) μa μc
h₁ : g = comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := γ) (⇑e.symm : (a : γ) → β) ((⇑e : (a : β) → γ) ∘ g)
⊢ MeasurePreserving g μa μb

Tactic:
convert! (MeasurePreserving.symm e h).comp hg

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e : (a : β) → γ) μb μc
hg : MeasurePreserving ((⇑e : (a : β) → γ) ∘ g) μa μc
⊢ g = comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := γ) (⇑e.symm : (a : γ) → β) ((⇑e : (a : β) → γ) ∘ g)

Tactic:
simp [← Function.comp_assoc e.symm e g]

Premises used: MeasurableEquiv.symm, DFunLike.coe, Function.comp_assoc
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e : (a : γ) → α) μc μa
⊢ MeasurePreserving (g ∘ (⇑e : (a : γ) → α)) μc μb ↔ MeasurePreserving g μa μb

Tactic:
⟨fun hg => ?_, fun hg => hg.comp h⟩

Premises used: Iff.intro, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e : (a : γ) → α) μc μa
refine : ∀ (hg : MeasurePreserving (g ∘ (⇑e : (a : γ) → α)) μc μb), MeasurePreserving g μa μb
⊢ MeasurePreserving (g ∘ (⇑e : (a : γ) → α)) μc μb ↔ MeasurePreserving g μa μb

Tactic:
refine ⟨fun hg => ?_, fun hg => hg.comp h⟩
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e : (a : γ) → α) μc μa
hg : MeasurePreserving (g ∘ (⇑e : (a : γ) → α)) μc μb
⊢ MeasurePreserving (comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := γ) (g ∘ (⇑e : (a : γ) → α)) (⇑e.symm : (a : α) → γ)) μa μb

Tactic:
hg.comp (MeasurePreserving.symm e h)

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e : (a : γ) → α) μc μa
hg : MeasurePreserving (g ∘ (⇑e : (a : γ) → α)) μc μb
h₁ : g = comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := γ) (g ∘ (⇑e : (a : γ) → α)) (⇑e.symm : (a : α) → γ)
⊢ MeasurePreserving g μa μb

Tactic:
convert! hg.comp (MeasurePreserving.symm e h)

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e : (a : γ) → α) μc μa
hg : MeasurePreserving (g ∘ (⇑e : (a : γ) → α)) μc μb
⊢ g = comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := γ) (g ∘ (⇑e : (a : γ) → α)) (⇑e.symm : (a : α) → γ)

Tactic:
simp [Function.comp_assoc g e e.symm]

Premises used: MeasurableEquiv.symm, DFunLike.coe, Function.comp_assoc
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst_2 rwa rwa₁ rwa₂ rwa₃ : SigmaFinite μb
⊢ SigmaFinite (m0 := inst_1) (map f μa)

Tactic:
rwa [hf.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst_2 : SFinite μa
rw : SFinite (m0 := inst_1) (map f μa)
⊢ SFinite μb

Tactic:
rw [← hf.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst_2 : SFinite μa
⊢ SFinite (m0 := inst_1) (map f μa)

Tactic:
infer_instance
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s μb
rw :
  ∀ (hs : NullMeasurableSet s (map f μa)),
    Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← hf.map_eq] at hs ⊢

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s (map f μa)
rw rw₁ : Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply₀ hf.1.aemeasurable hs]

Premises used: Measurable.aemeasurable, MeasureTheory.MeasurePreserving.measurable, MeasureTheory.Measure.map_apply₀
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s μb
⊢ μa.real (f ⁻¹' s) = μb.real s

Tactic:
simp [measureReal_def, measure_preimage hf hs]

Premises used: MeasureTheory.measureReal_def, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
hfe : MeasurableEmbedding f
s : Set β
rw :
  Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← hf.map_eq, hfe.map_apply]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasurableEmbedding.map_apply