awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
μ : ProbabilityMeasure E
hμ : μ ∈ S
n : ℕ
⊢ Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ x.le n) n

Tactic:
exact le_rfl (a := n)

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
μ : ProbabilityMeasure E
hμ : μ ∈ S
n : ℕ
⊢ (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst) {x : Measure E | ∃ μ ∈ S, (↑μ : Measure E) = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : (n : ℕ) → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
K' : (n : ℕ) → Set E := fun (n : ℕ) ↦ ⋃ i ∈ Iic n, K i
h'K :
  IsCompact.{u_1} (X := ProbabilityMeasure E)
    {μ : ProbabilityMeasure E | ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n}
μ : ProbabilityMeasure E
hμ : μ ∈ S
n : ℕ
calc : LE.le (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K' n)ᶜ : ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (K n)ᶜ : ℝ≥0)
calc₁ : (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ (μ : (a : Set E) → ℝ≥0) (K' n)ᶜ ≤ u n

Tactic:
calc μ (K' n)ᶜ
  _ ≤ μ (K n)ᶜ := by
    gcongr
    simp only [mem_Iic, K']
    apply subset_biUnion_of_mem
    exact le_rfl (a := n)
  _ ≤ u n := by grind

Premises used: Compl.compl, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
_m0 : MeasurableSpace α
μ : Measure α
⊢ QuasiMeasurePreserving id μ μ

Tactic:
⟨measurable_id, map_id.absolutelyContinuous⟩

Premises used: MeasureTheory.Measure.map_id, measurable_id, MeasureTheory.Measure.QuasiMeasurePreserving.mk, Eq.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
f : α → β
_m0 : MeasurableSpace α
hf : Measurable f
μ : Measure α
⊢ QuasiMeasurePreserving (mβ := mβ) f μ (map f μ)

Tactic:
⟨hf, AbsolutelyContinuous.rfl⟩

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa μa' : Measure α
μb : Measure β
f : α → β
h : QuasiMeasurePreserving f μa μb
ha : μa' ≪ μa
⊢ QuasiMeasurePreserving f μa' μb

Tactic:
⟨h.1, (ha.map h.1).trans h.2⟩

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.map, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb μb' : Measure β
f : α → β
h : QuasiMeasurePreserving f μa μb
ha : μb ≪ μb'
⊢ QuasiMeasurePreserving f μa μb'

Tactic:
⟨h.1, h.2.trans ha⟩

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa μa' : Measure α
μb μb' : Measure β
f : α → β
ha : μa' ≪ μa
hb : μb ≪ μb'
h : QuasiMeasurePreserving f μa μb
⊢ QuasiMeasurePreserving f μa' μb'

Tactic:
(h.mono_left ha).mono_right hb

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mono_right, MeasureTheory.Measure.QuasiMeasurePreserving.mono_left
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
rw : map g (map f μa) ≪ μc
⊢ map (g ∘ f) μa ≪ μc

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

Premises used: MeasureTheory.Measure.map_map, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
⊢ map g (map f μa) ≪ μc

Tactic:
(hf.2.map hg.1).trans hg.2

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.map, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : β → γ
f : α → β
hg : QuasiMeasurePreserving g μb μc
hf : QuasiMeasurePreserving f μa μb
⊢ map g (map f μa) ≪ μc

Tactic:
exact (hf.2.map hg.1).trans hg.2

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.map, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : QuasiMeasurePreserving f μa μb
⊢ AEMeasurable f μa

Tactic:
hf.1.aemeasurable

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

Tactic:
⟨hf', ?_⟩

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

Tactic:
refine ⟨hf', ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : QuasiMeasurePreserving f μa μb
f' : α → β
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.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : QuasiMeasurePreserving f μa μb
f' : α → β
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
⊢ map f μa ≪ μb

Tactic:
hf.absolutelyContinuous

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : QuasiMeasurePreserving f μa μb
f' : α → β
hf' : Measurable f'
h : f =ᶠ[ae μa] f'
⊢ map f μa ≪ μb

Tactic:
exact hf.absolutelyContinuous

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
rw : HSMul.hSMul (β := Measure β) c (map f μa) ≪ c • μb
⊢ map f (c • μa) ≪ c • μb

Tactic:
rw [Measure.map_smul]

Premises used: MeasureTheory.Measure.map_smul
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ HSMul.hSMul (β := Measure β) c (map f μa) ≪ c • μb

Tactic:
hf.2.smul c

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.smul
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ HSMul.hSMul (β := Measure β) c (map f μa) ≪ c • μb

Tactic:
exact hf.2.smul c

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.smul
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
h : QuasiMeasurePreserving f μa μb
⊢ ae (F := Measure β) (map f μa) ≤ ae μb

Tactic:
h.2.ae_le

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_le, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
h : QuasiMeasurePreserving f μa μb
⊢ Tendsto f (ae μa) (ae μb)

Tactic:
(tendsto_ae_map h.aemeasurable).mono_right h.ae_map_le

Premises used: MeasureTheory.Measure.tendsto_ae_map, MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le, MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable, Filter.Tendsto.mono_right
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
h : QuasiMeasurePreserving f μa μb
p : β → Prop
hg : ∀ᵐ (x : β) ∂μb, p x
⊢ ∀ᵐ (x : α) ∂μa, p (f x)

Tactic:
h.tendsto_ae hg

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
h : QuasiMeasurePreserving f μa μb
g₁ g₂ : β → δ
hg : g₁ =ᵐ[μb] g₂
⊢ g₁ ∘ f =ᵐ[μa] g₂ ∘ f

Tactic:
h.ae hg

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.ae, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
h : QuasiMeasurePreserving f μa μb
s : Set β
hs : Eq (α := ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
preimage_null_of_map_null h.aemeasurable (h.2 hs)

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.Measure.preimage_null_of_map_null
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
s t : Set β
hf : QuasiMeasurePreserving f μa μb
h : s ≤ᵐ[μb] t
⊢ f ⁻¹' s ≤ᵐ[μa] f ⁻¹' t

Tactic:
eventually_map.mp <|
    Eventually.filter_mono (tendsto_ae_map hf.aemeasurable) (Eventually.filter_mono hf.ae_map_le h)

Premises used: Filter.Eventually.filter_mono, Set.Mem, setOf, Filter.eventually_map, MeasureTheory.Measure.tendsto_ae_map, MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le, Set.preimage, MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable, Iff.mp, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
s t : Set β
hf : QuasiMeasurePreserving f μa μb
h : s =ᵐ[μb] t
⊢ f ⁻¹' s =ᵐ[μa] f ⁻¹' t

Tactic:
EventuallyLE.antisymm (hf.preimage_mono_ae h.le) (hf.preimage_mono_ae h.symm.le)

Premises used: Filter.EventuallyEq.le, Filter.EventuallyLE.antisymm, Filter.EventuallyEq.symm, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_mono_ae
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
s : Set β
hs : NullMeasurableSet s μb
hf : QuasiMeasurePreserving f μa μb
⊢ NullMeasurableSet (f ⁻¹' s) μa

Tactic:
let ⟨t, htm, hst⟩ := hs
  ⟨f ⁻¹' t, hf.measurable htm, hf.preimage_ae_eq hst⟩

Premises used: MeasureTheory.NullMeasurableSet, _private.0.MeasureTheory.NullMeasurableSet.preimage.match_1, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq, Set.preimage, And.intro, Exists.intro, MeasureTheory.Measure.QuasiMeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[0] ⁻¹' s =ᵐ[μ] f^[0] ⁻¹' s

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
succ : f ⁻¹' f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f^[k + 1] ⁻¹' s =ᵐ[μ] s

Tactic:
rw [iterate_succ, preimage_comp]

Premises used: Function.iterate_succ, Set.preimage_comp
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f ⁻¹' f^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
EventuallyEq.trans (hf.preimage_ae_eq ih) hs

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f ⁻¹' f^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
exact EventuallyEq.trans (hf.preimage_ae_eq ih) hs

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
k : ℕ
hs : f ⁻¹' s =ᵐ[μ] s
zero : f^[0] ⁻¹' s =ᵐ[μ] f^[0] ⁻¹' s
succ : ∀ (k : ℕ) (ih : f^[k] ⁻¹' s =ᵐ[μ] s), f^[k + 1] ⁻¹' s =ᵐ[μ] s
⊢ f^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
induction k with
  | zero => rfl
  | succ k ih =>
    rw [iterate_succ, preimage_comp]
    exact EventuallyEq.trans (hf.preimage_ae_eq ih) hs

Premises used: Function.iterate_succ, Set.preimage_comp
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
k : ℤ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
rw : (⇑(e ^ k).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
⊢ (⇑(e ^ k) : (a : α) → α) '' s =ᵐ[μ] s

Tactic:
rw [Equiv.image_eq_preimage_symm]

Premises used: Equiv.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
k : ℤ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
inl : ∀ (k : ℕ), (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
inr : ∀ (k : ℕ), (⇑(HPow.hPow (β := ℤ) e (-(↑k : ℤ))).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
⊢ (⇑(e ^ k).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s

Tactic:
obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
k : ℕ
rwa rwa₁ rwa₂ rwa₃ : ∀ (hs : (⇑e.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s) (k : ℕ), (⇑e⁻¹ : (a : α) → α) ⁻¹' s =ᵐ[μ] s
⊢ (⇑e⁻¹ : (a : α) → α) ⁻¹' s =ᵐ[μ] s

Tactic:
rwa [Equiv.image_eq_preimage_symm] at hs

Premises used: Equiv.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
k : ℕ
⊢ (⇑e⁻¹ : (a : α) → α) ⁻¹' s =ᵐ[μ] s

Tactic:
replace hs : (⇑e⁻¹) ⁻¹' s =ᵐ[μ] s := by rwa [Equiv.image_eq_preimage_symm] at hs
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
k : ℕ
hs : (⇑e⁻¹ : (a : α) → α) ⁻¹' s =ᵐ[μ] s
⊢ (⇑e⁻¹ : (a : α) → α)^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
replace he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s := he'.preimage_iterate_ae_eq k hs
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
k : ℕ
hs : (⇑e⁻¹ : (a : α) → α) ⁻¹' s =ᵐ[μ] s
he' : (⇑e⁻¹ : (a : α) → α)^[k] ⁻¹' s =ᵐ[μ] s
inl :
  ∀ (he' : (⇑(e⁻¹ ^ k) : (a : α) → α) ⁻¹' s =ᵐ[μ] s),
    (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
inl₁ inl₂ inl₃ inl₄ :
  ∀ (he' : (⇑(e ^ k)⁻¹ : (a : α) → α) ⁻¹' s =ᵐ[μ] s),
    (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
⊢ (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s

Tactic:
rwa [Equiv.Perm.iterate_eq_pow e⁻¹ k, inv_pow e k] at he'

Premises used: Equiv.Perm.iterate_eq_pow, inv_pow, Inv.inv
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
k : ℕ
inr : (⇑(e ^ k)⁻¹.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
⊢ (⇑(HPow.hPow (β := ℤ) e (-(↑k : ℤ))).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s

Tactic:
rw [zpow_neg, zpow_natCast]

Premises used: zpow_natCast, zpow_neg
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
k : ℕ
⊢ (⇑e : (a : α) → α) ⁻¹' s =ᵐ[μ] preimage (β := α) (⇑e : (a : α) → α) ((⇑e : (a : α) → α) '' s)

Tactic:
he.preimage_ae_eq hs.symm

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
k : ℕ
h : s = preimage (β := α) (⇑e : (a : α) → α) ((⇑e : (a : α) → α) '' s)
⊢ (⇑e : (a : α) → α) ⁻¹' s =ᵐ[μ] s

Tactic:
convert! he.preimage_ae_eq hs.symm

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
k : ℕ
h h₁ : s = s
⊢ s = preimage (β := α) (⇑e : (a : α) → α) ((⇑e : (a : α) → α) '' s)

Tactic:
rw [Equiv.preimage_image]

Premises used: Equiv.preimage_image
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
hs : (⇑e : (a : α) → α) '' s =ᵐ[μ] s
k : ℕ
⊢ (⇑e : (a : α) → α) ⁻¹' s =ᵐ[μ] s

Tactic:
replace hs : e ⁻¹' s =ᵐ[μ] s := by
      convert! he.preimage_ae_eq hs.symm
      rw [Equiv.preimage_image]
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e : (a : α) → α) μ μ
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
k : ℕ
hs : (⇑e : (a : α) → α) ⁻¹' s =ᵐ[μ] s
⊢ (⇑e : (a : α) → α)^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
replace he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s := he.preimage_iterate_ae_eq k hs
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he' : QuasiMeasurePreserving (⇑e.symm : (a : α) → α) μ μ
k : ℕ
hs : (⇑e : (a : α) → α) ⁻¹' s =ᵐ[μ] s
he : (⇑e : (a : α) → α)^[k] ⁻¹' s =ᵐ[μ] s
inr inr₁ inr₂ inr₃ : ∀ (he : (⇑(e ^ k) : (a : α) → α) ⁻¹' s =ᵐ[μ] s), (⇑(e ^ k)⁻¹.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
⊢ (⇑(e ^ k)⁻¹.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s

Tactic:
rwa [Equiv.Perm.iterate_eq_pow e k] at he

Premises used: Equiv.Perm.iterate_eq_pow
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
n : ℕ
⊢ (fun (n : ℕ) ↦ (preimage f)^[n] s) n =ᵐ[μ] s

Tactic:
simpa only [Set.preimage_iterate_eq] using hf.preimage_iterate_ae_eq n hs

Premises used: Set.preimage_iterate_eq, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s =ᵐ[μ] s
obtain :
  ∀ (t : Set α) (htm : MeasurableSet t) (ht : s =ᵐ[μ] t), ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t
⊢ ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t

Tactic:
obtain ⟨t, htm, ht⟩ := hs