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
f : CompactlySupportedContinuousMap B E
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
x : C
hx : x ∉ (⇑ψ : (a : B) → C) '' K
refine :
  ∀ (a : A),
    ((ψ : (a : B) → C)
          (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
        C) ∉
      (⇑ψ : (a : B) → C) '' K
⊢ ∀ (a : A),
    Eq.{u_4 + 1} (α := E)
      ((f : (a : B) → E)
          (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
        E)
      (0 : E)

Tactic:
refine fun a ↦ hf _ (mt (Set.mem_image_of_mem ψ) ?_)

Premises used: mt, Set.mem_image_of_mem, 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
f : CompactlySupportedContinuousMap B E
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
x : C
hx : x ∉ (⇑ψ : (a : B) → C) '' K
a : A
rwa :
  HMul.hMul (α := C) (β := C) ((ψ : (a : B) → C) (Function.invFun (⇑ψ : (a : B) → C) x) : C)
      ((ψ : (a : B) → C) ((φ : (a : A) → B) a : B) : C) ∉
    (⇑ψ : (a : B) → C) '' K
rwa₁ : HMul.hMul (β := C) x ((ψ : (a : B) → C) ((φ : (a : A) → B) a : B) : C) ∉ (⇑ψ : (a : B) → C) '' K
rwa₂ : x * 1 ∉ (⇑ψ : (a : B) → C) '' K
rwa₃ rwa₄ rwa₅ rwa₆ : x ∉ (⇑ψ : (a : B) → C) '' K
⊢ ((ψ : (a : B) → C)
        (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
      C) ∉
    (⇑ψ : (a : B) → C) '' K

Tactic:
rwa [map_mul, Function.rightInverse_invFun H.isOpenQuotientMap.surjective,
        H.mulExact.apply_apply_eq_one, mul_one]

Premises used: Function.rightInverse_invFun, IsOpenQuotientMap.surjective, map_mul, TopologicalGroup.IsSES.isOpenQuotientMap, TopologicalGroup.IsSES.mulExact, mul_one, Function.MulExact.apply_apply_eq_one
-- 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
f g : CompactlySupportedContinuousMap B E
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 := ⋯, hasCompactSupport' := ⋯ : 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 := ⋯, 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 } :
            (a : C) → E)
          c :
        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 }

Tactic:
ext c
-- 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
f g : CompactlySupportedContinuousMap B E
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 := ⋯, hasCompactSupport' := ⋯ : 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 := ⋯, 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 } :
          (a : C) → E)
        c :
      E)

Tactic:
integral_add (pullback H f _).integrable (pullback H g _).integrable

Premises used: CompactlySupportedContinuousMap.integrable, TopologicalGroup.IsSES.pullback, MeasureTheory.integral_add
-- 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
f g : CompactlySupportedContinuousMap B E
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 := ⋯, hasCompactSupport' := ⋯ : 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 := ⋯, 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 } :
          (a : C) → E)
        c :
      E)

Tactic:
exact integral_add (pullback H f _).integrable (pullback H g _).integrable

Premises used: CompactlySupportedContinuousMap.integrable, TopologicalGroup.IsSES.pullback, MeasureTheory.integral_add
-- 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
x : ℝ
f : CompactlySupportedContinuousMap B E
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 := ⋯, hasCompactSupport' := ⋯ : 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 := ⋯, hasCompactSupport' := ⋯ : CompactlySupportedContinuousMap C E } :
            (a : C) → E)
          c :
        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 }

Tactic:
ext c
-- 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
x : ℝ
f : CompactlySupportedContinuousMap B E
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 := ⋯, hasCompactSupport' := ⋯ : 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 := ⋯, hasCompactSupport' := ⋯ : CompactlySupportedContinuousMap C E } :
          (a : C) → E)
        c :
      E)

Tactic:
apply integral_smul

Premises used: MeasureTheory.integral_smul
-- 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
f : CompactlySupportedContinuousMap B E
c : C
⊢ Eq.{u_4 + 1} (α := E)
    ((((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) f :
            CompactlySupportedContinuousMap C E) :
          (a : C) → E)
        c :
      E)
    (∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA : 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
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 : CompactlySupportedContinuousMap B E
b : B
⊢ Eq.{u_4 + 1} (α := E)
    ((((H.pushforward μA : (a : CompactlySupportedContinuousMap B E) → CompactlySupportedContinuousMap C E) f :
            CompactlySupportedContinuousMap C E) :
          (a : C) → E)
        ((ψ : (a : B) → C) b : C) :
      E)
    (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA : E)

Tactic:
integral_pullback_invFun_apply H μA f b

Premises used: TopologicalGroup.IsSES.integral_pullback_invFun_apply
-- 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
f g : CompactlySupportedContinuousMap B ℝ
h : f ≤ g
⊢ LE.le.{u_3} (α := CompactlySupportedContinuousMap 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 ℝ)
    (((H.pushforward μA :
            LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
              (CompactlySupportedContinuousMap C ℝ)) :
          (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
        g :
      CompactlySupportedContinuousMap C ℝ)

Tactic:
fun _ ↦ integral_mono (pullback H f _).integrable (pullback H g _).integrable (fun _ ↦ h _)

Premises used: Function.invFun, HMul.hMul, MeasureTheory.integral_mono, CompactlySupportedContinuousMap.integrable, TopologicalGroup.IsSES.pullback, 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 g : CompactlySupportedContinuousMap B E
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)
⊢ ∫ (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)

Tactic:
rw [map_add]

Premises used: map_add
-- 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 g : CompactlySupportedContinuousMap B E
⊢ ∫ (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:
integral_add (pushforward H μA f).integrable (pushforward H μA g).integrable

Premises used: CompactlySupportedContinuousMap.integrable, TopologicalGroup.IsSES.pushforward, DFunLike.coe, MeasureTheory.integral_add
-- 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 g : CompactlySupportedContinuousMap B E
⊢ ∫ (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:
exact integral_add (pushforward H μA f).integrable (pushforward H μA g).integrable

Premises used: CompactlySupportedContinuousMap.integrable, TopologicalGroup.IsSES.pushforward, DFunLike.coe, MeasureTheory.integral_add
-- 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
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)
⊢ ∫ (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)

Tactic:
rw [map_smul]

Premises used: map_smul
-- 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:
integral_smul x (H.pushforward μA f)

Premises used: MeasureTheory.integral_smul, TopologicalGroup.IsSES.pushforward, DFunLike.coe