no goals
G : Type u_1
H : Type ?u.119421
α : Type u_2
β : Type ?u.119427
E : Type ?u.119430
inst✝⁹ : Group G
inst✝⁸ : Group H
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MulAction H β
inst✝⁴ : MeasurableSpace β
inst✝³ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
h : IsFundamentalDomain G s
g g' : G
⊢ (fun g' => g * g' * g⁻¹) ((fun g' => g⁻¹ * g' * g) g') = g'
simp [mul_assoc]
no goals
G : Type u_1
H : Type ?u.119421
α : Type u_2
β : Type ?u.119427
E : Type ?u.119430
inst✝⁹ : Group G
inst✝⁸ : Group H
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MulAction H β
inst✝⁴ : MeasurableSpace β
inst✝³ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
h : IsFundamentalDomain G s
g g' : G
⊢ (fun g' => g⁻¹ * g' * g) ((fun g' => g * g' * g⁻¹) g') = g'
simp [mul_assoc]
no goals
G : Type u_1
H : Type ?u.119421
α : Type u_2
β : Type ?u.119427
E : Type ?u.119430
inst✝⁹ : Group G
inst✝⁸ : Group H
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MulAction H β
inst✝⁴ : MeasurableSpace β
inst✝³ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
inst✝ : SMulInvariantMeasure G α μ
h : IsFundamentalDomain G s
g g' : G
x : α
⊢ ↑(MulAction.toPerm g)
      ((fun x =>
          ↑{ toFun := fun g' => g⁻¹ * g' * g, invFun := fun g' => g * g' * g⁻¹,
                  left_inv := (_ : ∀ (g' : G), g * (g⁻¹ * g' * g) * g⁻¹ = g'),
                  right_inv := (_ : ∀ (g' : G), g⁻¹ * (g * g' * g⁻¹) * g = g') }
              g' •
            x)
        x) =
    (fun x => g' • x) (↑(MulAction.toPerm g) x)
simp [smul_smul, mul_assoc]