𝕜 : Type ?u.68496
M : Type ?u.68499
α : Type ?u.68502
G : Type u_1
E : Type ?u.68508
F : Type u_2
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
h : Integrable fun t => f (g / t)
⊢ Integrable f
𝕜 : Type ?u.68496
M : Type ?u.68499
α : Type ?u.68502
G : Type u_1
E : Type ?u.68508
F : Type u_2
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
⊢ (Integrable fun t => f (g / t)) ↔ Integrable f
refine' ⟨fun h => _, fun h => h.comp_div_left g⟩
case h.e'_5.h.h.e'_1
𝕜 : Type ?u.68496
M : Type ?u.68499
α : Type ?u.68502
G : Type u_1
E : Type ?u.68508
F : Type u_2
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
h : Integrable fun t => f (g / t)
x✝ : G
⊢ x✝ = g / (g⁻¹ * x✝)⁻¹
𝕜 : Type ?u.68496
M : Type ?u.68499
α : Type ?u.68502
G : Type u_1
E : Type ?u.68508
F : Type u_2
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
h : Integrable fun t => f (g / t)
⊢ Integrable f
convert h.comp_inv.comp_mul_left g⁻¹
no goals
case h.e'_5.h.h.e'_1
𝕜 : Type ?u.68496
M : Type ?u.68499
α : Type ?u.68502
G : Type u_1
E : Type ?u.68508
F : Type u_2
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
h : Integrable fun t => f (g / t)
x✝ : G
⊢ x✝ = g / (g⁻¹ * x✝)⁻¹
simp_rw [div_inv_eq_mul, mul_inv_cancel_left]