awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e : (a : α) → β) μa μb
⊢ map (⇑e.symm : (a : β) → α) μb = μa
have rw : map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) μa) = μa
Tactic: rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ map (⇑e.symm : (a : β) → α) μb = μa
have rw₁ : map (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) μa = μa
Tactic: rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ map (⇑e.symm : (a : β) → α) μb = μa
have rw₂ : map id μa = μa
Tactic: rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ map (⇑e.symm : (a : β) → α) μb = μa
have rw₃ : μa = μa
Tactic: rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s
have rw : Eq (α := Measure β) (map f (μa.restrict (f ⁻¹' s))) (Measure.restrict (map f μa) s)
Tactic: rw [← hf.map_eq, restrict_map hf.measurable hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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)
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s
have rw₁ : Eq (α := Measure β) (map f (μa.restrict (f ⁻¹' s))) (map f (μa.restrict (f ⁻¹' s)))
Tactic: rw [← hf.map_eq, restrict_map hf.measurable hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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 β
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s
have rw : Eq (α := Measure β) (map f (μa.restrict (f ⁻¹' s))) (Measure.restrict (map f μa) s)
Tactic: rw [← hf.map_eq, h₂.restrict_map]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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)
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s
have rw₁ : Eq (α := Measure β) (map f (μa.restrict (f ⁻¹' s))) (map f (μa.restrict (f ⁻¹' s)))
Tactic: rw [← hf.map_eq, h₂.restrict_map]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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 : β → γ
⊢ AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb
have rw : AEMeasurable (g ∘ f) μa ↔ AEMeasurable (_m := inst_1) g (map f μa)
Tactic: rw [← hf.map_eq, h₂.aemeasurable_map_iff]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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)
⊢ AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb
have rw₁ : AEMeasurable (g ∘ f) μa ↔ AEMeasurable (g ∘ f) μa
Tactic: rw [← hf.map_eq, h₂.aemeasurable_map_iff]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ map (g ∘ f) μa = μc
have rw : map g (map f μa) = μc
Tactic: rw [← map_map hg.1 hf.1, hf.2, hg.2]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ map (g ∘ f) μa = μc
have rw₁ : map g μb = μc
Tactic: rw [← map_map hg.1 hf.1, hf.2, hg.2]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ map (g ∘ f) μa = μc
have rw₂ : μc = μc
Tactic: rw [← map_map hg.1 hf.1, hf.2, hg.2]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (hypothesis)
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 μb μb
have this : MeasurePreserving gb (map f μa) μb
Tactic: have := hf.comp_eq ▸ hfm.comp hga |>.map_of_comp hgb hfm.measurable
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ MeasurePreserving gb μb μb
have rwa : ∀ (this : MeasurePreserving gb μb μb), MeasurePreserving gb μb μb
Tactic: rwa [hfm.map_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
have refine : ∀ (hg : MeasurePreserving ((⇑e : (a : β) → γ) ∘ g) μa μc), MeasurePreserving g μa μb
Tactic: refine ⟨fun hg => ?_, fun hg => h.comp hg⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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 g μa μb
have h₁ : g = comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := γ) (⇑e.symm : (a : γ) → β) ((⇑e : (a : β) → γ) ∘ g)
Tactic: convert! (MeasurePreserving.symm e h).comp hg
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
have refine : ∀ (hg : MeasurePreserving (g ∘ (⇑e : (a : γ) → α)) μc μb), MeasurePreserving g μa μb
Tactic: refine ⟨fun hg => ?_, fun hg => hg.comp h⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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 g μa μb
have h₁ : g = comp.{u_1 + 1, u_3 + 1, u_2 + 1} (β := γ) (g ∘ (⇑e : (a : γ) → α)) (⇑e.symm : (a : α) → γ)
Tactic: convert! hg.comp (MeasurePreserving.symm e h)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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 μb
have rw : SFinite (m0 := inst_1) (map f μa)
Tactic: rw [← hf.map_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rw [← hf.map_eq] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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)
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply₀ hf.1.aemeasurable hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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 β
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← hf.map_eq, hfe.map_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [← hf.map_eq, hfe.map_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ LE.le (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← hf.map_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
μa' : Measure α
μb' : Measure β
hf : MeasurePreserving f μa μb
hf' : MeasurePreserving f μa' μb'
⊢ map f (μa + μa') = μb + μb'
have rw : HAdd.hAdd (α := Measure β) (map f μa) (map f μa') = μb + μb'
Tactic: rw [Measure.map_add _ _ hf.measurable, hf.map_eq, hf'.map_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
μa' : Measure α
μb' : Measure β
hf : MeasurePreserving f μa μb
hf' : MeasurePreserving f μa' μb'
rw : HAdd.hAdd (α := Measure β) (map f μa) (map f μa') = μb + μb'
⊢ map f (μa + μa') = μb + μb'
have rw₁ : μb + map f μa' = μb + μb'
Tactic: rw [Measure.map_add _ _ hf.measurable, hf.map_eq, hf'.map_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
μa' : Measure α
μb' : Measure β
hf : MeasurePreserving f μa μb
hf' : MeasurePreserving f μa' μb'
rw : HAdd.hAdd (α := Measure β) (map f μa) (map f μa') = μb + μb'
rw₁ : μb + map f μa' = μb + μb'
⊢ map f (μa + μa') = μb + μb'
have rw₂ : μb + μb' = μb + μb'
Tactic: rw [Measure.map_add _ _ hf.measurable, hf.map_eq, hf'.map_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
R : Type u_5
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : α → β
hf : MeasurePreserving f μa μb
c : R
⊢ map f (c • μa) = c • μb
have rw : HSMul.hSMul (β := Measure β) c (map f μa) = c • μb
Tactic: rw [Measure.map_smul, hf.map_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
R : Type u_5
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : α → β
hf : MeasurePreserving f μa μb
c : R
rw : HSMul.hSMul (β := Measure β) c (map f μa) = c • μb
⊢ map f (c • μa) = c • μb
have rw₁ : c • μb = c • μb
Tactic: rw [Measure.map_smul, hf.map_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n + 1] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) (n + 1) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have succ : (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n + 1] ⁻¹' s)) ≤
  HAdd.hAdd (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
Tactic: simp only [add_smul, one_smul]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n + 1] ⁻¹' s)) ≤
    HAdd.hAdd (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have succ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
Tactic: grw [← ih, measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n + 1] ⁻¹' s)]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have hs₁ : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
Tactic: replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ :=
      hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have succ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f ∘ f^[n] ⁻¹' s)) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
Tactic: rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
succ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f ∘ f^[n] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have succ₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n] ⁻¹' f ⁻¹' s)) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
Tactic: rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
succ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f ∘ f^[n] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n] ⁻¹' f ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have succ₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f^[n] ⁻¹' s ∆ (f ⁻¹' s)) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
Tactic: rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.MeasurePreserving (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
succ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f ∘ f^[n] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n] ⁻¹' f ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (f^[n] ⁻¹' s ∆ (f ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
have succ₃ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
Tactic: rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]