-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integrable_comp_smul_iff {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ]
    (f : E → F) {R : ℝ} (hR : R ≠ 0) : Integrable (fun x => f (R • x)) μ ↔ Integrable f μ

Proof state:
case h.e'_6.h.h.e'_1
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable (fun x => g (S • x)) μ
hf : Integrable (fun x => f (R • x)) μ
x✝ : E
⊢ x✝ = R • R⁻¹ • x✝

Tactic:
rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]

Result:
no goals

Proof state:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable (fun x => g (S • x)) μ
⊢ Integrable (fun x => f (R • x)) μ ↔ Integrable f μ

Tactic:
refine ⟨fun hf => ?_, fun hf => this hf hR⟩

Result:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable (fun x => g (S • x)) μ
hf : Integrable (fun x => f (R • x)) μ
⊢ Integrable f μ

Proof state:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable (fun x => g (S • x)) μ
hf : Integrable (fun x => f (R • x)) μ
⊢ Integrable f μ

Tactic:
convert this hf (inv_ne_zero hR)

Result:
case h.e'_6.h.h.e'_1
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable (fun x => g (S • x)) μ
hf : Integrable (fun x => f (R • x)) μ
x✝ : E
⊢ x✝ = R • R⁻¹ • x✝

Proof state:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
⊢ Integrable (fun x => f (R • x)) μ ↔ Integrable f μ

Tactic:
suffices
  ∀ {g : E → F} (_ : Integrable g μ) {S : ℝ} (_ : S ≠ 0), Integrable (fun x => g (S • x)) μ by
  refine ⟨fun hf => ?_, fun hf => this hf hR⟩
  convert this hf (inv_ne_zero hR)
  rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]

Result:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
⊢ ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable (fun x => g (S • x)) μ

Proof state:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv
⊢ ENNReal.ofReal |(S ^ finrank ℝ E)⁻¹| ≠ 0

Tactic:
simpa only [Ne, ENNReal.ofReal_eq_zero, not_le, abs_pos] using inv_ne_zero (pow_ne_zero _ hS)

Result:
no goals

Proof state:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv
⊢ Integrable g (Measure.map (fun x => S • x) μ)

Tactic:
rwa [map_addHaar_smul μ hS, integrable_smul_measure _ ENNReal.ofReal_ne_top]

Result:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv
⊢ ENNReal.ofReal |(S ^ finrank ℝ E)⁻¹| ≠ 0

Proof state:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
⊢ ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable (fun x => g (S • x)) μ

Tactic:
intro g hg S hS

Result:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
⊢ Integrable (fun x => g (S • x)) μ

Proof state:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
⊢ Integrable (fun x => g (S • x)) μ

Tactic:
let t := ((Homeomorph.smul (isUnit_iff_ne_zero.2 hS).unit).toMeasurableEquiv : E ≃ᵐ E)

Result:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv
⊢ Integrable (fun x => g (S • x)) μ