-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem preimage_of_equiv {ν : Measure β} (h : IsFundamentalDomain G s μ) {f : β → α}
    (hf : QuasiMeasurePreserving f ν μ) {e : G → H} (he : Bijective e)
    (hef : ∀ g, Semiconj f (e g • ·) (g • ·)) : IsFundamentalDomain H (f ⁻¹' s) ν where
  nullMeasurableSet := h.nullMeasurableSet.preimage hf
  ae_covers := (hf.ae h.ae_covers).mono fun x ⟨g, hg⟩ => ⟨e g, by rwa [mem_preimage, hef g x]⟩
  aedisjoint a b hab

Proof state:
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G) (x : β), f (e g • x) = g • f x
this✝ : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹
this : AEDisjoint ν (f ⁻¹' (fun g => g • s) (e.symm a⁻¹)⁻¹) (f ⁻¹' (fun g => g • s) (e.symm b⁻¹)⁻¹)
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Tactic:
simpa only [onFun, ← preimage_smul_inv, preimage_preimage, ← hef, e.apply_symm_apply, inv_inv]
  using this

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
e : G → H
he : Bijective e
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
a b : H
hab : a ≠ b
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Tactic:
lift e to G ≃ H using he

Result:
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Proof state:
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
this✝ : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹
this : AEDisjoint ν (f ⁻¹' (fun g => g • s) (e.symm a⁻¹)⁻¹) (f ⁻¹' (fun g => g • s) (e.symm b⁻¹)⁻¹)
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Tactic:
simp only [Semiconj] at hef

Result:
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G) (x : β), f (e g • x) = g • f x
this✝ : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹
this : AEDisjoint ν (f ⁻¹' (fun g => g • s) (e.symm a⁻¹)⁻¹) (f ⁻¹' (fun g => g • s) (e.symm b⁻¹)⁻¹)
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Proof state:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
e : G → H
he : Bijective e
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
x : β
x✝ : ∃ g, g • f x ∈ s
g : G
hg : g • f x ∈ s
⊢ e g • x ∈ f ⁻¹' s

Tactic:
rwa [mem_preimage, hef g x]

Result:
no goals

Proof state:
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
this : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Tactic:
have := (h.aedisjoint this).preimage hf

Result:
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
this✝ : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹
this : AEDisjoint ν (f ⁻¹' (fun g => g • s) (e.symm a⁻¹)⁻¹) (f ⁻¹' (fun g => g • s) (e.symm b⁻¹)⁻¹)
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Proof state:
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Tactic:
have : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹ := by simp [hab]

Result:
case intro
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
this : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹
⊢ (AEDisjoint ν on fun g => g • f ⁻¹' s) a b

Proof state:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef : ∀ (g : G), Semiconj f (fun x => e g • x) fun x => g • x
⊢ (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹

Tactic:
simp [hab]

Result:
no goals