-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- In a group with a left invariant measure `μ` and a right invariant measure `ν`, one can express
integrals with respect to `μ` as integrals with respect to `ν` up to a constant scaling factor
(given in the statement as `∫ x, g x ∂μ` where `g` is a fixed reference function) and an
explicit density `y ↦ 1/∫ z, g (z⁻¹ * y) ∂ν`. -/
@[to_additive]
lemma integral_isMulLeftInvariant_isMulRightInvariant_combo
    {μ ν : Measure G} [IsFiniteMeasureOnCompacts μ] [IsFiniteMeasureOnCompacts ν]
    [IsMulLeftInvariant μ] [IsMulRightInvariant ν] [IsOpenPosMeasure ν]
    {f g : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f)
    (hg : Continuous g) (h'g : HasCompactSupport g) (g_nonneg : 0 ≤ g) {x₀ : G} (g_pos : g x₀ ≠ 0) :
    ∫ x, f x ∂μ = (∫ y, f y * (∫ z, g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ x, g x ∂μ

Proof state:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p => p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure M)
⊢ ∀ p ∉ L ×ˢ closure M, f (p.2 * p.1) * (D (p.2 * p.1))⁻¹ * g p.1 = 0

Tactic:
rintro ⟨x, y⟩ hxy

Result:
case mk
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p => p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure M)
x y : G
hxy : (x, y) ∉ L ×ˢ closure M
⊢ f ((x, y).2 * (x, y).1) * (D ((x, y).2 * (x, y).1))⁻¹ * g (x, y).1 = 0

Proof state:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous D
D_pos : ∀ (x : G), 0 < D x
⊢ ∫ (y : G), ∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ ∂ν = ∫ (y : G), ∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ ∂ν

Tactic:
congr with y

Result:
case e_f.h
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous D
D_pos : ∀ (x : G), 0 < D x
y : G
⊢ ∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ = ∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ

Proof state:
case e_f.h
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous D
D_pos : ∀ (x : G), 0 < D x
y : G
⊢ ∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ = ∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ

Tactic:
rw [← integral_mul_left_eq_self _ y]

Result:
case e_f.h
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous D
D_pos : ∀ (x : G), 0 < D x
y : G
⊢ ∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g (y⁻¹ * (y * x)) ∂μ = ∫ (x : G), f (y * x) * (D (y * x))⁻¹ * g x ∂μ

Proof state:
case inl
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : f = 0
⊢ ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ

Tactic:
simp [Hf]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p => p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure M)
⊢ ∀ p ∉ K ×ˢ closure M, f p.1 * (D p.1)⁻¹ * g (p.2⁻¹ * p.1) = 0

Tactic:
rintro ⟨x, y⟩ hxy

Result:
case mk
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
hg : Continuous g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p => p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure M)
x y : G
hxy : (x, y) ∉ K ×ˢ closure M
⊢ f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0