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
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 : ℝ)
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 :
        ℝ)
⊢ 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:
congr with 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
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 : ℝ)
c : C
e_f :
  ∀ (b' : B),
    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) (β := C) (((ψ : (a : B) → C) b)⁻¹ : C) ((ψ : (a : B) → C) b' : 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) → ℝ)
          ((ψ : (a : B) → C) b' : 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:
obtain ⟨b', rfl⟩ := H.isOpenQuotientMap.surjective c

Premises used: IsOpenQuotientMap.surjective, TopologicalGroup.IsSES.isOpenQuotientMap, 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 : ℝ)
b' : B
e_f :
  Eq (α := ℝ)
    (∫ (a : A), (H.pullback (f.comp (Homeomorph.toCocompactMap (Homeomorph.mulLeft b))) (b⁻¹ * b') : (a : A) → ℝ) a ∂μA)
    (∫ (a : A), (H.pullback f b' : (a : A) → ℝ) a ∂μA)
⊢ 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) (β := C) (((ψ : (a : B) → C) b)⁻¹ : C) ((ψ : (a : B) → C) b' : 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) → ℝ)
        ((ψ : (a : B) → C) b' : C) :
      ℝ)

Tactic:
rw [← map_inv, ← map_mul, pushforward_apply_apply, pushforward_apply_apply]

Premises used: map_inv, TopologicalGroup.IsSES.pushforward_apply_apply, map_mul
-- 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 : ℝ)
b' : B
⊢ Eq (α := ℝ)
    (∫ (a : A), (H.pullback (f.comp (Homeomorph.toCocompactMap (Homeomorph.mulLeft b))) (b⁻¹ * b') : (a : A) → ℝ) a ∂μA)
    (∫ (a : A), (H.pullback f b' : (a : A) → ℝ) a ∂μA)

Tactic:
simp [pullback_def, mul_assoc]

Premises used: TopologicalGroup.IsSES.pullback_def, mul_assoc
-- 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
U : Set B
hU : IsOpen U
b : B
hb : b ∈ U
obtain :
  ∀ (K : Set B) (hK : IsCompact K) (hb : b ∈ interior K) (hKU : K ⊆ U),
    Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)
⊢ Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)

Tactic:
obtain ⟨K, hK, hb, hKU⟩ := exists_compact_subset hU hb

Premises used: exists_compact_subset
-- 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
U : Set B
hU : IsOpen U
b : B
hb_1 : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
obtain :
  ∀ (f : C(B, ℝ)) (hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K)
    (hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))) (hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U)
    (hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)),
    Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)
⊢ Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)

Tactic:
obtain ⟨f, hf1, hf2, hf3, hf4⟩ := exists_continuousMap_one_of_isCompact_subset_isOpen hK hU hKU

Premises used: 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
U : Set B
hU : IsOpen U
b : B
hb_1 : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
rw :
  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 ℝ)
        0 :
      CompactlySupportedContinuousMap C ℝ)
    (((H.pushforward μA :
            LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
              (CompactlySupportedContinuousMap C ℝ)) :
          (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
        { toContinuousMap := f, hasCompactSupport' := hf2 } :
      CompactlySupportedContinuousMap C ℝ)
⊢ LE.le.{u_3} (α := CompactlySupportedContinuousMap C ℝ) (0 : CompactlySupportedContinuousMap C ℝ)
    (((H.pushforward μA :
            LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
              (CompactlySupportedContinuousMap C ℝ)) :
          (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
        { toContinuousMap := f, hasCompactSupport' := hf2 } :
      CompactlySupportedContinuousMap C ℝ)

Tactic:
rw [← map_zero (H.pushforward μA)]

Premises used: map_zero, TopologicalGroup.IsSES.pushforward
-- 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
U : Set B
hU : IsOpen U
b : B
hb_1 : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h : 0 ≤ { toContinuousMap := f, hasCompactSupport' := hf2 : CompactlySupportedContinuousMap B ℝ }
⊢ 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 ℝ)
        0 :
      CompactlySupportedContinuousMap C ℝ)
    (((H.pushforward μA :
            LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
              (CompactlySupportedContinuousMap C ℝ)) :
          (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
        { toContinuousMap := f, hasCompactSupport' := hf2 } :
      CompactlySupportedContinuousMap C ℝ)

Tactic:
apply pushforward_mono

Premises used: TopologicalGroup.IsSES.pushforward_mono
-- 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
U : Set B
hU : IsOpen U
b : B
hb_1 : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
⊢ 0 ≤ { toContinuousMap := f, hasCompactSupport' := hf2 : CompactlySupportedContinuousMap B ℝ }

Tactic:
fun x ↦ (hf4 x).1

Premises used: 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
U : Set B
hU : IsOpen U
b : B
hb_1 : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
⊢ 0 ≤ { toContinuousMap := f, hasCompactSupport' := hf2 : CompactlySupportedContinuousMap B ℝ }

Tactic:
exact fun x ↦ (hf4 x).1

Premises used: 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
U : Set B
hU : IsOpen U
b : B
hb_1 : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
⊢ LE.le.{u_3} (α := CompactlySupportedContinuousMap C ℝ) (0 : CompactlySupportedContinuousMap C ℝ)
    (((H.pushforward μA :
            LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
              (CompactlySupportedContinuousMap C ℝ)) :
          (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
        { toContinuousMap := f, hasCompactSupport' := hf2 } :
      CompactlySupportedContinuousMap C ℝ)

Tactic:
have hf0 : 0 ≤ H.pushforward μA ⟨f, hf2⟩ := by
      rw [← map_zero (H.pushforward μA)]
      apply pushforward_mono
      exact fun x ↦ (hf4 x).1
-- 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
U : Set B
hU : IsOpen U
b : B
hb_1 : b ∈ U
K : Set B
hK : IsCompact K
hb : b ∈ interior K
hKU : K ⊆ U
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
hf0 :
  LE.le.{u_3} (α := CompactlySupportedContinuousMap C ℝ) (0 : CompactlySupportedContinuousMap C ℝ)
    (((H.pushforward μA :
            LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
              (CompactlySupportedContinuousMap C ℝ)) :
          (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
        { toContinuousMap := f, hasCompactSupport' := hf2 } :
      CompactlySupportedContinuousMap C ℝ)
grw :
  LT.lt (α := ℝ) (0 : ℝ)
    (({ toLinearMap := H.integrate μA μC, monotone' := ⋯ } : (a : CompactlySupportedContinuousMap B ℝ) → ℝ)
        { toContinuousMap := f, hasCompactSupport' := hf2 : CompactlySupportedContinuousMap B ℝ } :
      ℝ)
⊢ Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)

Tactic:
grw [← pos_iff_ne_zero, inducedMeasure,
      ← RealRMK.le_rieszMeasure_tsupport_subset (f := ⟨f, hf2⟩) _ hf4 hf3, ENNReal.ofReal_pos]

Premises used: TopologicalGroup.IsSES.inducedMeasure, ENNReal.ofReal_pos, RealRMK.le_rieszMeasure_tsupport_subset, pos_iff_ne_zero