awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
x : ℝ
f : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C),
      (HSMul.hSMul (β := CompactlySupportedContinuousMap C E) x
            ((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) f :
              CompactlySupportedContinuousMap C E) :
          (a : C) → E)
        c ∂μC =
    HSMul.hSMul (α := ℝ) (β := E) ((RingHom.id ℝ : (a : ℝ) → ℝ) x : ℝ)
      (∫ (c : C),
        (((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) f :
              CompactlySupportedContinuousMap C E) :
            (a : C) → E)
          c ∂μC)

Tactic:
exact integral_smul x (H.pushforward μA f)

Premises used: MeasureTheory.integral_smul, TopologicalGroup.IsSES.pushforward, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
f : CompactlySupportedContinuousMap B E
⊢ Eq.{u_4 + 1} (α := E) ((H.integrate μA μC : (a : CompactlySupportedContinuousMap B E) → E) f : E)
    (∫ (c : C),
        (((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) f :
              CompactlySupportedContinuousMap C E) :
            (a : C) → E)
          c ∂μC :
      E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
f g : CompactlySupportedContinuousMap B ℝ
h : f ≤ g
⊢ LE.le (α := ℝ) ((H.integrate μA μC : (a : CompactlySupportedContinuousMap B ℝ) → ℝ) f : ℝ)
    ((H.integrate μA μC : (a : CompactlySupportedContinuousMap B ℝ) → ℝ) g : ℝ)

Tactic:
integral_mono (pushforward H μA f).integrable (pushforward H μA g).integrable
    (pushforward_mono H μA h)

Premises used: MeasureTheory.integral_mono, CompactlySupportedContinuousMap.integrable, TopologicalGroup.IsSES.pushforward, TopologicalGroup.IsSES.pushforward_mono, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
⊢ Regular (H.inducedMeasure μA μC)

Tactic:
RealRMK.regular_rieszMeasure _

Premises used: RealRMK.regular_rieszMeasure, TopologicalGroup.IsSES.inducedMeasure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
f : CompactlySupportedContinuousMap B ℝ
⊢ Eq (α := ℝ) (@integral _ _ _ _ inst_15 (H.inducedMeasure μA μC) fun (b : B) ↦ (f : (a : B) → ℝ) b : ℝ)
    ((H.integrate μA μC : (a : CompactlySupportedContinuousMap B ℝ) → ℝ) f : ℝ)

Tactic:
apply RealRMK.integral_rieszMeasure

Premises used: RealRMK.integral_rieszMeasure
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
K : Set B
hK : IsCompact K
obtain :
  ∀ (f : C(B, ℝ)) (hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K)
    (hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ)))
    (hf3 : Subset (α := Set B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ)) Set.univ)
    (hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)),
    LT.lt (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) K : ENNReal) (⊤ : ENNReal)
⊢ LT.lt (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) K : ENNReal) (⊤ : ENNReal)

Tactic:
obtain ⟨f, hf1, hf2, hf3, hf4⟩ :=
      exists_continuousMap_one_of_isCompact_subset_isOpen hK isOpen_univ K.subset_univ

Premises used: Set.subset_univ, isOpen_univ, exists_continuousMap_one_of_isCompact_subset_isOpen
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
K : Set B
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : Subset (α := Set B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ)) Set.univ
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
⊢ LT.lt (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) K : ENNReal) (⊤ : ENNReal)

Tactic:
lt_of_le_of_lt (RealRMK.rieszMeasure_le_of_eq_one (f := ⟨f, hf2⟩) _
      (fun x ↦ (hf4 x).1) hK (fun x hx ↦ hf1 hx)) ENNReal.ofReal_lt_top

Premises used: lt_of_le_of_lt, ENNReal.ofReal_lt_top, RealRMK.rieszMeasure_le_of_eq_one, And.left
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
K : Set B
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : Subset (α := Set B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ)) Set.univ
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
⊢ LT.lt (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) K : ENNReal) (⊤ : ENNReal)

Tactic:
exact lt_of_le_of_lt (RealRMK.rieszMeasure_le_of_eq_one (f := ⟨f, hf2⟩) _
      (fun x ↦ (hf4 x).1) hK (fun x hx ↦ hf1 hx)) ENNReal.ofReal_lt_top

Premises used: lt_of_le_of_lt, ENNReal.ofReal_lt_top, RealRMK.rieszMeasure_le_of_eq_one, And.left
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
⊢ Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))

Tactic:
have : ((inducedMeasure H μA μC).map (b * ·)).Regular := Regular.map (Homeomorph.mulLeft b)
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
this : Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))
⊢ Eq (α := Measure B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC)) (H.inducedMeasure μA μC)

Tactic:
ext_of_integral_eq_on_compactlySupported fun f ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
this : Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))
refine :
  ∀ (f : CompactlySupportedContinuousMap B ℝ),
    Eq (α := ℝ)
      (@integral _ _ _ _ inst_17 (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC)) fun (x : B) ↦ (f : (a : B) → ℝ) x)
      (@integral _ _ _ _ inst_17 (H.inducedMeasure μA μC) fun (x : B) ↦ (f : (a : B) → ℝ) x)
⊢ Eq (α := Measure B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC)) (H.inducedMeasure μA μC)

Tactic:
refine ext_of_integral_eq_on_compactlySupported fun f ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
this : Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))
f : CompactlySupportedContinuousMap B ℝ
⊢ AEMeasurable (β := B) (_m := inst_17) (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
this : Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))
f : CompactlySupportedContinuousMap B ℝ
⊢ AEStronglyMeasurable (α := B) (β := ℝ) (m₀ := inst_17) (⇑f : (a : B) → ℝ)
    (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
this : Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))
f : CompactlySupportedContinuousMap B ℝ
rw :
  Eq (α := ℝ) (@integral _ _ _ _ inst_17 (H.inducedMeasure μA μC) fun (x : B) ↦ (f : (a : B) → ℝ) (b * x))
    (@integral _ _ _ _ inst_17 (H.inducedMeasure μA μC) fun (x : B) ↦ (f : (a : B) → ℝ) x)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_17 (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC)) fun (x : B) ↦ (f : (a : B) → ℝ) x)
    (@integral _ _ _ _ inst_17 (H.inducedMeasure μA μC) fun (x : B) ↦ (f : (a : B) → ℝ) x)

Tactic:
rw [integral_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
this : Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))
f : CompactlySupportedContinuousMap B ℝ
⊢ ∀ (x : B),
    Eq (α := ℝ) ((f : (a : B) → ℝ) (b * x) : ℝ)
      ((f.comp (Homeomorph.toCocompactMap (Homeomorph.mulLeft b)) : (a : B) → ℝ) x : ℝ)

Tactic:
have h (x : B) : f (b * x) = f.comp (Homeomorph.mulLeft b).toCocompactMap x := rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
this : Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))
f : CompactlySupportedContinuousMap B ℝ
h :
  ∀ (x : B),
    Eq (α := ℝ) ((f : (a : B) → ℝ) (b * x) : ℝ)
      ((f.comp (Homeomorph.toCocompactMap (Homeomorph.mulLeft b)) : (a : B) → ℝ) x : ℝ)
simp_rw :
  Eq (α := ℝ)
    (∫ (c : C),
      ((((H.pushforward μA :
                  LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                    (CompactlySupportedContinuousMap C ℝ)) :
                (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
              (f.comp (Homeomorph.toCocompactMap (Homeomorph.mulLeft b))) :
            CompactlySupportedContinuousMap C ℝ) :
          (a : C) → ℝ)
        c ∂μC)
    (∫ (c : C),
      ((((H.pushforward μA :
                  LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                    (CompactlySupportedContinuousMap C ℝ)) :
                (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
              f :
            CompactlySupportedContinuousMap C ℝ) :
          (a : C) → ℝ)
        c ∂μC)
⊢ Eq (α := ℝ) (@integral _ _ _ _ inst_17 (H.inducedMeasure μA μC) fun (x : B) ↦ (f : (a : B) → ℝ) (b * x))
    (@integral _ _ _ _ inst_17 (H.inducedMeasure μA μC) fun (x : B) ↦ (f : (a : B) → ℝ) x)

Tactic:
simp_rw [h, integral_inducedMeasure, integrate_apply]

Premises used: TopologicalGroup.IsSES.integral_inducedMeasure, TopologicalGroup.IsSES.integrate_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
inst_14 : MeasurableSpace C
inst_15 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_16 : T2Space B
inst_17 : MeasurableSpace B
inst_18 : BorelSpace B
b : B
this : Regular (α := B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC))
f : CompactlySupportedContinuousMap B ℝ
h :
  ∀ (x : B),
    Eq (α := ℝ) ((f : (a : B) → ℝ) (b * x) : ℝ)
      ((f.comp (Homeomorph.toCocompactMap (Homeomorph.mulLeft b)) : (a : B) → ℝ) x : ℝ)
rw :
  Eq (α := ℝ)
    (∫ (x : C),
      ((((H.pushforward μA :
                  LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                    (CompactlySupportedContinuousMap C ℝ)) :
                (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
              (f.comp (Homeomorph.toCocompactMap (Homeomorph.mulLeft b))) :
            CompactlySupportedContinuousMap C ℝ) :
          (a : C) → ℝ)
        (HMul.hMul (α := C) (((ψ : (a : B) → C) b)⁻¹ : C) x) ∂μC)
    (∫ (c : C),
      ((((H.pushforward μA :
                  LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                    (CompactlySupportedContinuousMap C ℝ)) :
                (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
              f :
            CompactlySupportedContinuousMap C ℝ) :
          (a : C) → ℝ)
        c ∂μC)
⊢ Eq (α := ℝ)
    (∫ (c : C),
      ((((H.pushforward μA :
                  LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                    (CompactlySupportedContinuousMap C ℝ)) :
                (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
              (f.comp (Homeomorph.toCocompactMap (Homeomorph.mulLeft b))) :
            CompactlySupportedContinuousMap C ℝ) :
          (a : C) → ℝ)
        c ∂μC)
    (∫ (c : C),
      ((((H.pushforward μA :
                  LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                    (CompactlySupportedContinuousMap C ℝ)) :
                (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
              f :
            CompactlySupportedContinuousMap C ℝ) :
          (a : C) → ℝ)
        c ∂μC)

Tactic:
rw [← integral_mul_left_eq_self _ (ψ b)⁻¹]

Premises used: Inv.inv, MeasureTheory.integral_mul_left_eq_self, DFunLike.coe