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
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 ℝ)
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) :
      ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ)
    (({ toLinearMap := H.integrate μA μC, monotone' := ⋯ } : (a : CompactlySupportedContinuousMap B ℝ) → ℝ)
        { toContinuousMap := f, hasCompactSupport' := hf2 : CompactlySupportedContinuousMap B ℝ } :
      ℝ)

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'
-- 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 ℝ)
⊢ (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ * b ∈
    φ.range

Tactic:
simp [← H.mulExact.monoidHom_ker_eq, Function.apply_invFun_apply]

Premises used: Function.MulExact.monoidHom_ker_eq, Function.apply_invFun_apply, TopologicalGroup.IsSES.mulExact
-- 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 ℝ)
⊢ (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]
-- 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 ℝ)
this :
  (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ * b ∈
    φ.range
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) :
        ℝ)
⊢ 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
-- 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 ℝ)
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
⊢ 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:
simp [ha, hf1 (interior_subset hb)]

Premises used: interior_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
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
⊢ 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)]
-- 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 ℝ)
a : A
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 : ℝ)
⊢ 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:
(pullback H ⟨f, hf2⟩ _).continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero
      (pullback H ⟨f, hf2⟩ _).hasCompactSupport (fun x ↦ (hf4 _).1) ha

Premises used: Function.invFun, ContinuousMap.continuous, HMul.hMul, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero, CompactlySupportedContinuousMap.toContinuousMap, And.left, TopologicalGroup.IsSES.pullback, DFunLike.coe, CompactlySupportedContinuousMap.mk
-- 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 ℝ)
a : A
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 : ℝ)
⊢ 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:
exact (pullback H ⟨f, hf2⟩ _).continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero
      (pullback H ⟨f, hf2⟩ _).hasCompactSupport (fun x ↦ (hf4 _).1) ha

Premises used: ContinuousMap.continuous, HMul.hMul, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero, CompactlySupportedContinuousMap.toContinuousMap, And.left, TopologicalGroup.IsSES.pullback, DFunLike.coe, CompactlySupportedContinuousMap.mk
-- 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
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
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
⊢ ((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)

Tactic:
contrapose! h
-- 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
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
⊢ 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)
-- 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
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)
⊢ LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)

Tactic:
have ht : μA {1} < ⊤ := isCompact_singleton.measure_lt_top
-- 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
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)
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
⊢ ¬Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U

Tactic:
obtain ⟨K, hKU, hK, h⟩ := Regular.innerRegular hU _ h

Premises used: MeasureTheory.Measure.Regular.innerRegular