𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
h : H
⊢ Measure.map (fun x => h * x) (Measure.map (↑f) μ) = Measure.map (↑f) μ
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
⊢ IsMulLeftInvariant (Measure.map (↑f) μ)
refine' ⟨fun h => _⟩
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
h : H
⊢ Measure.map ((fun x => h * x) ∘ ↑f) μ = Measure.map (↑f) μ
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
h : H
⊢ Measure.map (fun x => h * x) (Measure.map (↑f) μ) = Measure.map (↑f) μ
rw [map_map (measurable_const_mul _) hf]
case intro
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g : G
⊢ Measure.map ((fun x => ↑f g * x) ∘ ↑f) μ = Measure.map (↑f) μ
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
h : H
⊢ Measure.map ((fun x => h * x) ∘ ↑f) μ = Measure.map (↑f) μ
obtain ⟨g, rfl⟩ := h_surj h
case intro
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g : G
⊢ Measure.map ((fun x => ↑f g * x) ∘ ↑f) μ = Measure.map (↑f) (Measure.map (fun x => g * x) μ)
case intro
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g : G
⊢ Measure.map ((fun x => ↑f g * x) ∘ ↑f) μ = Measure.map (↑f) μ
conv_rhs => rw [← map_mul_left_eq_self μ g]
case intro
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g : G
⊢ Measure.map ((fun x => ↑f g * x) ∘ ↑f) μ = Measure.map (↑f ∘ fun x => g * x) μ
case intro
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g : G
⊢ Measure.map ((fun x => ↑f g * x) ∘ ↑f) μ = Measure.map (↑f) (Measure.map (fun x => g * x) μ)
rw [map_map hf (measurable_const_mul _)]
case intro.e_f
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g : G
⊢ (fun x => ↑f g * x) ∘ ↑f = ↑f ∘ fun x => g * x
case intro
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g : G
⊢ Measure.map ((fun x => ↑f g * x) ∘ ↑f) μ = Measure.map (↑f ∘ fun x => g * x) μ
congr 2
case intro.e_f.h
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g y : G
⊢ ((fun x => ↑f g * x) ∘ ↑f) y = (↑f ∘ fun x => g * x) y
case intro.e_f
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g : G
⊢ (fun x => ↑f g * x) ∘ ↑f = ↑f ∘ fun x => g * x
ext y
no goals
case intro.e_f.h
𝕜 : Type ?u.240117
G : Type u_2
H✝ : Type ?u.240123
inst✝⁷ : MeasurableSpace G
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_1
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : IsMulLeftInvariant μ
f : G →ₙ* H
hf : Measurable ↑f
h_surj : Surjective ↑f
g y : G
⊢ ((fun x => ↑f g * x) ∘ ↑f) y = (↑f ∘ fun x => g * x) y
simp only [comp_apply, map_mul]