awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℝ)
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) :
      ℝ)
have ha₁ : Ne (α := ℝ)
  ((f : (a : B) → ℝ)
      (HMul.hMul (α := B) (β := B)
        (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C) : B)
        ((φ : (a : A) → B) a : B)) :
    ℝ)
  (0 : ℝ)
Tactic: replace ha : f (Function.invFun ψ (ψ b) * φ a) ≠ 0 := by simp [ha, hf1 (interior_subset hb)]
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
⊢ ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U ≤
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
have contrapose! : ∀
  (h :
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
        ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
      ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U),
  ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
⊢ ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
have ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
Tactic: have ho : 0 < μA {1} := (isOpen_discrete {1}).measure_pos _ (Set.singleton_nonempty 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
⊢ ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
have ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
Tactic: have ht : μA {1} < ⊤ := isCompact_singleton.measure_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
⊢ ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
have obtain : ∀ (K : Set B) (hKU : K ⊆ U) (hK : IsCompact K)
  (h :
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
        ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
      ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) K),
  ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
Tactic: obtain ⟨K, hKU, hK, h⟩ := Regular.innerRegular hU _ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) K
⊢ ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
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 : ℝ)),
  ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
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 (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) K
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 : ℝ)
⊢ ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
have h₁ : HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
    ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
  ENNReal.ofReal
    (∫ (c : 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 ℝ) :
          (a : C) → ℝ)
        c ∂μC)
Tactic: replace h : μC Set.univ * μA {1} < ENNReal.ofReal (∫ c : C, pushforward H μA ⟨f, hf2⟩ c ∂μC) :=
    lt_of_lt_of_le h ((RealRMK.rieszMeasure_le_of_eq_one (f := ⟨f, hf2⟩) _ (fun x ↦ (hf4 x).1)
      hK (fun x hx ↦ hf1 hx)))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
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 :
  ∀ (c : 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 ℝ) :
          (a : C) → ℝ)
        c ≤
      ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1})
hC : LT.lt (α := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal) (⊤ : ENNReal)
⊢ ENNReal.ofReal
      (∫ (c : 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 B ℝ } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC) ≤
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
have this : IsFiniteMeasure μC
Tactic: have : IsFiniteMeasure μC := ⟨hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
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 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : 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 ℝ) :
            (a : C) → ℝ)
          c ∂μC)
⊢ ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
have obtain : ∀ (c : C)
  (hc :
    ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1}) <
      ((((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) → ℝ)
        c),
  ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
Tactic: obtain ⟨c, hc⟩ : ∃ c : C, (μA {1}).toReal < pushforward H μA ⟨f, hf2⟩ c := by
    contrapose! h
    rcases eq_top_or_lt_top (μC Set.univ) with hC | hC
    · simp [hC, ENNReal.top_mul ho.ne']
    · have : IsFiniteMeasure μC := ⟨hC⟩
      rw [ENNReal.ofReal_le_iff_le_toReal (ENNReal.mul_lt_top hC ht).ne, ENNReal.toReal_mul,
        ← Measure.real_def, ← smul_eq_mul, ← integral_const]
      exact integral_mono (H.pushforward μA ⟨f, hf2⟩).integrable (integrable_const _) h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
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 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : 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 ℝ) :
            (a : C) → ℝ)
          c ∂μC)
c : C
hc :
  ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1}) <
    ((((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) → ℝ)
      c
⊢ ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
have contrapose! : ∀ (hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U),
  ((((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) → ℝ)
      c ≤
    ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1})
Tactic: contrapose! hc
Cleared hypotheses: hc