awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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 ∘ f) μa ≪ μc
have rw : map g (map f μa) ≪ μc
Tactic: rw [← map_map hg.1 hf.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
have refine : map f' μa ≪ μb
Tactic: refine ⟨hf', ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
have rw : map f μa ≪ μb
Tactic: rw [Measure.map_congr h.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
⊢ map f (c • μa) ≪ c • μb
have rw : HSMul.hSMul (β := Measure β) c (map f μa) ≪ c • μb
Tactic: rw [Measure.map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f^[k + 1] ⁻¹' s =ᵐ[μ] s
have succ : f ⁻¹' f^[k] ⁻¹' s =ᵐ[μ] s
Tactic: rw [iterate_succ, preimage_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
k : ℕ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[k] ⁻¹' s =ᵐ[μ] s
have zero : f^[0] ⁻¹' s =ᵐ[μ] f^[0] ⁻¹' s
Tactic: induction k with
  | zero => rfl
  | succ k ih =>
    rw [iterate_succ, preimage_comp]
    exact EventuallyEq.trans (hf.preimage_ae_eq ih) hs
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
⊢ f^[k] ⁻¹' s =ᵐ[μ] s
have succ : ∀ (k : ℕ) (ih : f^[k] ⁻¹' s =ᵐ[μ] s), f^[k + 1] ⁻¹' 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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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 ^ k) : (a : α) → α) '' s =ᵐ[μ] s
have rw : (⇑(e ^ k).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
Tactic: rw [Equiv.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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 ^ k).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have inl : ∀ (k : ℕ), (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
Tactic: obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
⊢ (⇑(e ^ k).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have inr : ∀ (k : ℕ), (⇑(HPow.hPow (β := ℤ) e (-(↑k : ℤ))).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
Tactic: obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
have rwa : ∀ (hs : (⇑e.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s) (k : ℕ), (⇑e⁻¹ : (a : α) → α) ⁻¹' s =ᵐ[μ] s
Tactic: rwa [Equiv.image_eq_preimage_symm] at hs
Cleared hypotheses: hs, k
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (hypothesis)
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 : ℕ
⊢ (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have hs₁ : (⇑e⁻¹ : (a : α) → α) ⁻¹' s =ᵐ[μ] s
Tactic: replace hs : (⇑e⁻¹) ⁻¹' s =ᵐ[μ] s := by rwa [Equiv.image_eq_preimage_symm] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (hypothesis)
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
⊢ (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have he'₁ : (⇑e⁻¹ : (a : α) → α)^[k] ⁻¹' s =ᵐ[μ] s
Tactic: replace he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s := he'.preimage_iterate_ae_eq k hs
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
⊢ (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have inl : ∀ (he' : (⇑(e⁻¹ ^ k) : (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'
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
⊢ (⇑(HPow.hPow (β := ℤ) e (↑k : ℤ)).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have inl₁ : ∀ (he' : (⇑(e ^ k)⁻¹ : (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'
Cleared hypotheses: he'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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 : ℕ
⊢ (⇑(HPow.hPow (β := ℤ) e (-(↑k : ℤ))).symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have inr : (⇑(e ^ k)⁻¹.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
Tactic: rw [zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
have h : s = preimage (β := α) (⇑e : (a : α) → α) ((⇑e : (a : α) → α) '' s)
Tactic: convert! he.preimage_ae_eq hs.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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 : ℕ
⊢ s = preimage (β := α) (⇑e : (a : α) → α) ((⇑e : (a : α) → α) '' s)
have h : s = s
Tactic: rw [Equiv.preimage_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (hypothesis)
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 ^ k)⁻¹.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have hs₁ : (⇑e : (a : α) → α) ⁻¹' s =ᵐ[μ] s
Tactic: replace hs : e ⁻¹' s =ᵐ[μ] s := by
      convert! he.preimage_ae_eq hs.symm
      rw [Equiv.preimage_image]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (hypothesis)
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 ^ k)⁻¹.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have he₁ : (⇑e : (a : α) → α)^[k] ⁻¹' s =ᵐ[μ] s
Tactic: replace he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s := he.preimage_iterate_ae_eq k hs
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
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
⊢ (⇑(e ^ k)⁻¹.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
have inr : ∀ (he : (⇑(e ^ k) : (a : α) → α) ⁻¹' s =ᵐ[μ] s), (⇑(e ^ k)⁻¹.symm : (a : α) → α) ⁻¹' s =ᵐ[μ] s
Tactic: rwa [Equiv.Perm.iterate_eq_pow e k] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : f ⁻¹' s =ᵐ[μ] s
⊢ ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t
have obtain : ∀ (t : Set α) (htm : MeasurableSet t) (ht : s =ᵐ[μ] t), ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t
Tactic: obtain ⟨t, htm, ht⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t
have refine_1 : MeasurableSet.{u_1} (α := α) (limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop)
Tactic: refine ⟨limsup (f^[·] ⁻¹' t) atTop, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
refine_1 : MeasurableSet.{u_1} (α := α) (limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop)
⊢ ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t
have refine_2 : limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop =ᵐ[μ] s
Tactic: refine ⟨limsup (f^[·] ⁻¹' t) atTop, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
refine_1 : MeasurableSet.{u_1} (α := α) (limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop)
refine_2 : limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop =ᵐ[μ] s
⊢ ∃ (t : Set α), MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t
have refine_3 : f ⁻¹' limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop = limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop
Tactic: refine ⟨limsup (f^[·] ⁻¹' t) atTop, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop =ᵐ[μ] s
have this : f ⁻¹' t =ᵐ[μ] t
Tactic: have : f ⁻¹' t =ᵐ[μ] t := (h.preimage_ae_eq ht.symm).trans (hs'.trans ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
h : QuasiMeasurePreserving f μ μ
hs' : f ⁻¹' s =ᵐ[μ] s
t : Set α
htm : MeasurableSet t
ht : s =ᵐ[μ] t
⊢ f ⁻¹' limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop = limsup (fun (x : ℕ) ↦ f^[x] ⁻¹' t) atTop
have refine_3 : f ⁻¹' limsup (fun (x : ℕ) ↦ (preimage f)^[x] t) atTop = limsup (fun (x : ℕ) ↦ (preimage f)^[x] t) atTop
Tactic: simp only [Set.preimage_iterate_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ g ≠ 1
have rw : ¬g₂ = g₁
Tactic: rw [Ne, inv_mul_eq_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (hypothesis)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ (AEDisjoint μ on fun (g : G) ↦ g • s) g₁ g₂
have hg₁ : g ≠ 1
Tactic: replace hg : g ≠ 1 := by
    rw [Ne, inv_mul_eq_one]
    exact hg.symm
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
have rw : g • s ∩ s = (fun (x : α) ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
Tactic: rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
rw : g • s ∩ s = (fun (x : α) ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
have rw₁ : g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)
Tactic: rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
rw : g • s ∩ s = (fun (x : α) ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
rw₁ : g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
have rw₂ : g • s ∩ s = g₂⁻¹ • g₁ • s ∩ g₂⁻¹ • g₂ • s
Tactic: rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
rw : g • s ∩ s = (fun (x : α) ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
rw₁ : g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)
rw₂ : g • s ∩ s = g₂⁻¹ • g₁ • s ∩ g₂⁻¹ • g₂ • s
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
have rw₃ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ g₂⁻¹ • g₂ • s
Tactic: rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
rw : g • s ∩ s = (fun (x : α) ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
rw₁ : g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)
rw₂ : g • s ∩ s = g₂⁻¹ • g₁ • s ∩ g₂⁻¹ • g₂ • s
rw₃ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ g₂⁻¹ • g₂ • s
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
have rw₄ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ (g₂⁻¹ * g₂) • s
Tactic: rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
rw : g • s ∩ s = (fun (x : α) ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
rw₁ : g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)
rw₂ : g • s ∩ s = g₂⁻¹ • g₁ • s ∩ g₂⁻¹ • g₂ • s
rw₃ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ g₂⁻¹ • g₂ • s
rw₄ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ (g₂⁻¹ * g₂) • s
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
have rw₅ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ HSMul.hSMul.{u_5, u_6, u_6} (α := G) 1 s
Tactic: rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
rw : g • s ∩ s = (fun (x : α) ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)
rw₁ : g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)
rw₂ : g • s ∩ s = g₂⁻¹ • g₁ • s ∩ g₂⁻¹ • g₂ • s
rw₃ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ g₂⁻¹ • g₂ • s
rw₄ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ (g₂⁻¹ * g₂) • s
rw₅ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ HSMul.hSMul.{u_5, u_6, u_6} (α := G) 1 s
⊢ (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
have rw₆ : g • s ∩ s = (g₂⁻¹ * g₁) • s ∩ s
Tactic: rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (hypothesis)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ (AEDisjoint μ on fun (g : G) ↦ g • s) g₁ g₂
have this : (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
Tactic: have : (g₂⁻¹ • ·) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s := by
    rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
      smul_smul, inv_mul_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
G : Type u_5
α : Type u_6
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
this : (fun (x : α) ↦ g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
⊢ (AEDisjoint μ on fun (g : G) ↦ g • s) g₁ g₂
have change : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (g₁ • s ∩ g₂ • s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: change μ (g₁ • s ∩ g₂ • s) = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measure.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (Measure.map (⇑e : (a : α) → β) μ) ≪ μ
have hg : Measurable.{u_2, u_1} (α := β) (β := α) (⇑e.symm : (a : β) → α)
Tactic: rw [Measure.map_map, e.symm_comp_self, Measure.map_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
hg : Measurable.{u_2, u_1} (α := β) (β := α) (⇑e.symm : (a : β) → α)
⊢ Measure.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (Measure.map (⇑e : (a : α) → β) μ) ≪ μ
have hf : Measurable.{u_1, u_2} (α := α) (β := β) (⇑e : (a : α) → β)
Tactic: rw [Measure.map_map, e.symm_comp_self, Measure.map_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s = 0 ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.real, ENNReal.toReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (hypothesis)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₁ ⊆ s₂
h₂ : μ.real s₂ = 0
h'₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₁ = 0
have h₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [measureReal_eq_zero_iff h'₂] at h₂
Cleared hypotheses: h₂, h'₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s ≤ μ.real (s ∪ t)
have inl : ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real s ≤ μ.real (s ∪ t)
Tactic: rcases eq_top_or_lt_top (μ s) with hs | hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real s ≤ μ.real (s ∪ t)
⊢ μ.real s ≤ μ.real (s ∪ t)
have inr : ∀ (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real s ≤ μ.real (s ∪ t)
Tactic: rcases eq_top_or_lt_top (μ s) with hs | hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real t ≤ μ.real (s ∪ t)
have rw : μ.real t ≤ μ.real (t ∪ s)
Tactic: rw [union_comm]