α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
k : ℤ
hs : ↑e '' s =ᵐ[μ] s
⊢ ↑(e ^ k).symm ⁻¹' s =ᵐ[μ] s
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
k : ℤ
hs : ↑e '' s =ᵐ[μ] s
⊢ ↑(e ^ k) '' s =ᵐ[μ] s
rw [Equiv.image_eq_preimage]
case intro.inl
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s

case intro.inr
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑(e ^ (-↑k)).symm ⁻¹' s =ᵐ[μ] s
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
k : ℤ
hs : ↑e '' s =ᵐ[μ] s
⊢ ↑(e ^ k).symm ⁻¹' s =ᵐ[μ] s
obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
case hs
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑e⁻¹ ⁻¹' s =ᵐ[μ] s

case intro.inl
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
k : ℕ
hs : ↑e⁻¹ ⁻¹' s =ᵐ[μ] s
⊢ ↑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s
case intro.inl
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s
replace hs : (⇑e⁻¹) ⁻¹' s =ᵐ[μ] s
case intro.inl
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
k : ℕ
hs : ↑e⁻¹ ⁻¹' s =ᵐ[μ] s
he' : ↑e⁻¹^[k] ⁻¹' s =ᵐ[μ] s
⊢ ↑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s
case intro.inl
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
k : ℕ
hs : ↑e⁻¹ ⁻¹' s =ᵐ[μ] s
⊢ ↑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s
replace he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s := he'.preimage_iterate_ae_eq k hs
no goals
case intro.inl
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
k : ℕ
hs : ↑e⁻¹ ⁻¹' s =ᵐ[μ] s
he' : ↑e⁻¹^[k] ⁻¹' s =ᵐ[μ] s
⊢ ↑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s
rwa [Equiv.Perm.iterate_eq_pow e⁻¹ k, inv_pow e k] at he'
no goals
case hs
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑e⁻¹ ⁻¹' s =ᵐ[μ] s
rwa [Equiv.image_eq_preimage] at hs
case intro.inr
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
case intro.inr
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑(e ^ (-↑k)).symm ⁻¹' s =ᵐ[μ] s
rw [zpow_neg, zpow_ofNat]
case hs
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑e ⁻¹' s =ᵐ[μ] s

case intro.inr
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
k : ℕ
hs : ↑e ⁻¹' s =ᵐ[μ] s
⊢ ↑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
case intro.inr
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
replace hs : e ⁻¹' s =ᵐ[μ] s
case intro.inr
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he' : QuasiMeasurePreserving ↑e.symm
k : ℕ
hs : ↑e ⁻¹' s =ᵐ[μ] s
he : ↑e^[k] ⁻¹' s =ᵐ[μ] s
⊢ ↑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
case intro.inr
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
k : ℕ
hs : ↑e ⁻¹' s =ᵐ[μ] s
⊢ ↑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
replace he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s := he.preimage_iterate_ae_eq k hs
no goals
case intro.inr
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he' : QuasiMeasurePreserving ↑e.symm
k : ℕ
hs : ↑e ⁻¹' s =ᵐ[μ] s
he : ↑e^[k] ⁻¹' s =ᵐ[μ] s
⊢ ↑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
rwa [Equiv.Perm.iterate_eq_pow e k] at he
case h.e'_5
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ s = ↑e ⁻¹' (↑e '' s)
case hs
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ ↑e ⁻¹' s =ᵐ[μ] s
convert he.preimage_ae_eq hs.symm
no goals
case h.e'_5
α : Type u_1
β : Type ?u.412225
γ : Type ?u.412228
δ : Type ?u.412231
ι : Type ?u.412234
R : Type ?u.412237
R' : Type ?u.412240
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
μa μa' : Measure α
μb μb' : Measure β
μc : Measure γ
f : α → β
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
hs : ↑e '' s =ᵐ[μ] s
k : ℕ
⊢ s = ↑e ⁻¹' (↑e '' s)
rw [Equiv.preimage_image]