G : Type u_2
H : Type u_4
α : Type u_3
β : Type u_1
E : Type ?u.74797
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
⊢ IsFundamentalDomain H (↑f.symm ⁻¹' s)
G : Type u_2
H : Type u_4
α : Type u_3
β : Type u_1
E : Type ?u.74797
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
⊢ IsFundamentalDomain H (↑f '' s)
rw [f.image_eq_preimage]
G : Type u_2
H : Type u_4
α : Type u_3
β : Type u_1
E : Type ?u.74797
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
g : G
x : β
⊢ ↑f.symm ((fun x => ↑e.symm g • x) x) = (fun x => g • x) (↑f.symm x)
G : Type u_2
H : Type u_4
α : Type u_3
β : Type u_1
E : Type ?u.74797
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
⊢ IsFundamentalDomain H (↑f.symm ⁻¹' s)
refine' h.preimage_of_equiv hf e.symm.bijective fun g x => _
case intro
G : Type u_2
H : Type u_4
α : Type u_3
β : Type u_1
E : Type ?u.74797
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
g : G
x : α
⊢ ↑f.symm ((fun x => ↑e.symm g • x) (↑f x)) = (fun x => g • x) (↑f.symm (↑f x))
G : Type u_2
H : Type u_4
α : Type u_3
β : Type u_1
E : Type ?u.74797
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
g : G
x : β
⊢ ↑f.symm ((fun x => ↑e.symm g • x) x) = (fun x => g • x) (↑f.symm x)
rcases f.surjective x with ⟨x, rfl⟩
no goals
case intro
G : Type u_2
H : Type u_4
α : Type u_3
β : Type u_1
E : Type ?u.74797
inst✝⁶ : Group G
inst✝⁵ : Group H
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
inst✝² : MulAction H β
inst✝¹ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
s t : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s
f : α ≃ β
hf : QuasiMeasurePreserving ↑f.symm
e : H ≃ G
hef : ∀ (g : H), Semiconj (↑f) (fun x => ↑e g • x) fun x => g • x
g : G
x : α
⊢ ↑f.symm ((fun x => ↑e.symm g • x) (↑f x)) = (fun x => g • x) (↑f.symm (↑f x))
rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]