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
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
⊢ 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 :
      ℝ)
have 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) :
      ℝ)
Tactic: obtain ⟨b', rfl⟩ := H.isOpenQuotientMap.surjective c
Cleared hypotheses: 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
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 (α := ℝ)
    (((((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) :
      ℝ)
have 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)
Tactic: rw [← map_inv, ← map_mul, pushforward_apply_apply, pushforward_apply_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
U : Set B
hU : IsOpen U
b : B
hb : b ∈ U
⊢ Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)
have 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)
Tactic: obtain ⟨K, hK, hb, hKU⟩ := exists_compact_subset hU hb
-- 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
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
⊢ Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)
have 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)
Tactic: obtain ⟨f, hf1, hf2, hf3, hf4⟩ := exists_continuousMap_one_of_isCompact_subset_isOpen hK hU hKU
-- 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
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 ℝ)
have 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 ℝ)
Tactic: rw [← map_zero (H.pushforward μA)]
-- 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
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 ℝ)
    (((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 ℝ)
have h : 0 ≤ { toContinuousMap := f, hasCompactSupport' := hf2 : CompactlySupportedContinuousMap B ℝ }
Tactic: apply pushforward_mono
-- 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
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 : ℝ)
⊢ Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)
have 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 ℝ)
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
-- 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
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 ℝ)
⊢ Ne (α := ENNReal) (((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U : ENNReal) (0 : ENNReal)
have grw : LT.lt (α := ℝ) (0 : ℝ)
  (({ toLinearMap := H.integrate μA μC, monotone' := sorry } : (a : CompactlySupportedContinuousMap B ℝ) → ℝ)
      { toContinuousMap := f, hasCompactSupport' := hf2 : CompactlySupportedContinuousMap B ℝ } :
    ℝ)
Tactic: grw [← pos_iff_ne_zero, inducedMeasure,
      ← RealRMK.le_rieszMeasure_tsupport_subset (f := ⟨f, hf2⟩) _ hf4 hf3, ENNReal.ofReal_pos]
-- 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
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 ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ)
    (({ toLinearMap := H.integrate μA μC, monotone' := ⋯ } : (a : CompactlySupportedContinuousMap B ℝ) → ℝ)
        { toContinuousMap := f, hasCompactSupport' := hf2 : CompactlySupportedContinuousMap B ℝ } :
      ℝ)
have suffices : LT.lt (α := ℝ) (0 : ℝ)
  (((((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 ℝ) :
        (a : C) → ℝ)
      ((ψ : (a : B) → C) b : C) :
    ℝ)
Tactic: suffices (0 : ℝ) < pushforward H μA ⟨f, hf2⟩ (ψ b) from
      (pushforward H μA ⟨f, hf2⟩).continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero
        (pushforward H μA ⟨f, hf2⟩).hasCompactSupport hf0 this.ne'
-- 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
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 ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ)
    (((((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 ℝ) :
          (a : C) → ℝ)
        ((ψ : (a : B) → C) b : C) :
      ℝ)
have this : (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ * b ∈
  φ.range
Tactic: have : (Function.invFun ψ (ψ b))⁻¹ * b ∈ φ.range := by
      simp [← H.mulExact.monoidHom_ker_eq, Function.apply_invFun_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
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 ℝ)
this :
  (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ * b ∈
    φ.range
⊢ LT.lt (α := ℝ) (0 : ℝ)
    (((((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 ℝ) :
          (a : C) → ℝ)
        ((ψ : (a : B) → C) b : C) :
      ℝ)
have obtain : ∀ (a : A)
  (ha :
    (φ : (a : A) → B) a =
      (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ * b),
  LT.lt (α := ℝ) (0 : ℝ)
    (((((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 ℝ) :
          (a : C) → ℝ)
        ((ψ : (a : B) → C) b : C) :
      ℝ)
Tactic: obtain ⟨a, ha⟩ := this
Cleared hypotheses: this