awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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
f g : CompactlySupportedContinuousMap B E
⊢ { toFun := fun (c : C) ↦ ∫ (a : A), (H.pullback (f + g) (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
      continuous_toFun := ⋯, hasCompactSupport' := ⋯ : CompactlySupportedContinuousMap C E } =
    { toFun := fun (c : C) ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
        continuous_toFun := ⋯, hasCompactSupport' := ⋯ : CompactlySupportedContinuousMap C E } +
      { toFun := fun (c : C) ↦ ∫ (a : A), (H.pullback g (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
        continuous_toFun := ⋯, hasCompactSupport' := ⋯ : CompactlySupportedContinuousMap C E }
have h : ∀ (c : C),
  Eq.{u_4 + 1} (α := E)
    (({
            toFun := fun (c : C) ↦
              ∫ (a : A), (H.pullback (f + g) (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
            continuous_toFun := sorry, hasCompactSupport' := sorry : CompactlySupportedContinuousMap C E } :
          (a : C) → E)
        c :
      E)
    (({ toFun := fun (c : C) ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
              continuous_toFun := sorry, hasCompactSupport' := sorry : CompactlySupportedContinuousMap C E } +
            {
              toFun := fun (c : C) ↦
                ∫ (a : A), (H.pullback g (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
              continuous_toFun := sorry, hasCompactSupport' := sorry : CompactlySupportedContinuousMap C E } :
          (a : C) → E)
        c :
      E)
Tactic: ext c
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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
x : ℝ
f : CompactlySupportedContinuousMap B E
⊢ { toFun := fun (c : C) ↦ ∫ (a : A), (H.pullback (x • f) (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
      continuous_toFun := ⋯, hasCompactSupport' := ⋯ : CompactlySupportedContinuousMap C E } =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) x : ℝ)
      { toFun := fun (c : C) ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
        continuous_toFun := ⋯, hasCompactSupport' := ⋯ : CompactlySupportedContinuousMap C E }
have h : ∀ (c : C),
  Eq.{u_4 + 1} (α := E)
    (({
            toFun := fun (c : C) ↦
              ∫ (a : A), (H.pullback (x • f) (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
            continuous_toFun := sorry, hasCompactSupport' := sorry : CompactlySupportedContinuousMap C E } :
          (a : C) → E)
        c :
      E)
    ((HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) x : ℝ)
            {
              toFun := fun (c : C) ↦
                ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA,
              continuous_toFun := sorry, hasCompactSupport' := sorry : CompactlySupportedContinuousMap C E } :
          (a : C) → E)
        c :
      E)
Tactic: ext c
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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 g : CompactlySupportedContinuousMap B E
⊢ ∫ (c : C),
      (((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) (f + g) :
            CompactlySupportedContinuousMap C E) :
          (a : C) → E)
        c ∂μC =
    HAdd.hAdd (α := E)
      (∫ (c : C),
        (((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) f :
              CompactlySupportedContinuousMap C E) :
            (a : C) → E)
          c ∂μC)
      (∫ (c : C),
        (((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) g :
              CompactlySupportedContinuousMap C E) :
            (a : C) → E)
          c ∂μC)
have rw : ∫ (c : C),
    (HAdd.hAdd (α := CompactlySupportedContinuousMap C E) (β := CompactlySupportedContinuousMap C E)
          ((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) f :
            CompactlySupportedContinuousMap C E)
          ((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) g :
            CompactlySupportedContinuousMap C E) :
        (a : C) → E)
      c ∂μC =
  HAdd.hAdd (α := E)
    (∫ (c : C),
      (((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) f :
            CompactlySupportedContinuousMap C E) :
          (a : C) → E)
        c ∂μC)
    (∫ (c : C),
      (((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) g :
            CompactlySupportedContinuousMap C E) :
          (a : C) → E)
        c ∂μC)
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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),
      (((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) (x • 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)
have rw : ∫ (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: rw [map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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
⊢ LT.lt (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) K : ENNReal) (⊤ : ENNReal)
have 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)
Tactic: obtain ⟨f, hf1, hf2, hf3, hf4⟩ :=
      exists_continuousMap_one_of_isCompact_subset_isOpen hK isOpen_univ K.subset_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
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
⊢ Eq (α := Measure B) (map (fun (x : B) ↦ b * x) (H.inducedMeasure μA μC)) (H.inducedMeasure μA μC)
have this : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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)
have 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)
Tactic: refine ext_of_integral_eq_on_compactlySupported fun f ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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 ℝ
⊢ 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)
have 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)
Tactic: rw [integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
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 ℝ
⊢ 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)
have h : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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 : ℝ)
⊢ 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)
have 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)
Tactic: simp_rw [h, integral_inducedMeasure, integrate_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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 : ℝ)
⊢ 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)
have 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)
Tactic: rw [← integral_mul_left_eq_self _ (ψ b)⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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 : ℝ)
⊢ 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)
have e_f : ∀ (c : C),
  Eq (α := ℝ)
    (((((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) 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 :
      ℝ)
Tactic: congr with c