-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem image_zpow_ae_eq {s : Set α} {e : α ≃ α} (he : QuasiMeasurePreserving e μ μ)
    (he' : QuasiMeasurePreserving e.symm μ μ) (k : ℤ) (hs : e '' s =ᵐ[μ] s) :
    (⇑(e ^ k)) '' s =ᵐ[μ] s

Proof state:
case intro.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s

Tactic:
replace hs : e ⁻¹' s =ᵐ[μ] s := by
  convert he.preimage_ae_eq hs.symm
  rw [Equiv.preimage_image]

Result:
case intro.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℤ
hs : ⇑e '' s =ᵐ[μ] s
⊢ ⇑(e ^ k).symm ⁻¹' s =ᵐ[μ] s

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

Result:
case intro.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
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
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ (-↑k)).symm ⁻¹' s =ᵐ[μ] s

Proof state:
case intro.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
k : ℕ
hs : ⇑e⁻¹ ⁻¹' s =ᵐ[μ] s
he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s

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

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑e⁻¹ ⁻¹' s =ᵐ[μ] s

Tactic:
rwa [Equiv.image_eq_preimage] at hs

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e ⁻¹' s =ᵐ[μ] s
he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s

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

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ (-↑k)).symm ⁻¹' s =ᵐ[μ] s

Tactic:
rw [zpow_neg, zpow_natCast]

Result:
case intro.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s

Proof state:
case intro.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s

Tactic:
replace he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s := he.preimage_iterate_ae_eq k hs

Result:
case intro.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e ⁻¹' s =ᵐ[μ] s
he : (⇑e)^[k] ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s

Proof state:
case intro.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s

Tactic:
replace hs : (⇑e⁻¹) ⁻¹' s =ᵐ[μ] s := by rwa [Equiv.image_eq_preimage] at hs

Result:
case intro.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e⁻¹ ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s

Proof state:
case h.e'_5
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ s = ⇑e ⁻¹' (⇑e '' s)

Tactic:
rw [Equiv.preimage_image]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑e ⁻¹' s =ᵐ[μ] s

Tactic:
convert he.preimage_ae_eq hs.symm

Result:
case h.e'_5
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ s = ⇑e ⁻¹' (⇑e '' s)

Proof state:
case intro.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e⁻¹ ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s

Tactic:
replace he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s := he'.preimage_iterate_ae_eq k hs

Result:
case intro.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
k : ℕ
hs : ⇑e⁻¹ ⁻¹' s =ᵐ[μ] s
he' : (⇑e⁻¹)^[k] ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ ↑k).symm ⁻¹' s =ᵐ[μ] s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℤ
hs : ⇑e '' s =ᵐ[μ] s
⊢ ⇑(e ^ k) '' s =ᵐ[μ] s

Tactic:
rw [Equiv.image_eq_preimage]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℤ
hs : ⇑e '' s =ᵐ[μ] s
⊢ ⇑(e ^ k).symm ⁻¹' s =ᵐ[μ] s