awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g : G
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
s : Set A
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0
hμgs : (μ : (a : Set A) → ℝ≥0∞) (g • s) = HMul.hMul (β := ℝ≥0∞) (↑r : ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
refine : (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞) = (↑r : ℝ≥0∞)
⊢ ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g = r

Tactic:
refine ENNReal.coe_injective ?_

Premises used: ENNReal.coe_injective
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g : G
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
s : Set A
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0
hμgs : (μ : (a : Set A) → ℝ≥0∞) (g • s) = HMul.hMul (β := ℝ≥0∞) (↑r : ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
hb₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞) = (↑r : ℝ≥0∞)

Tactic:
rw [distribHaarChar_eq_div hs₀ hs, hμgs, ENNReal.mul_div_cancel_right]

Premises used: ENNReal.mul_div_cancel_right, MeasureTheory.distribHaarChar_eq_div
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g : G
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
s : Set A
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0
hμgs : (μ : (a : Set A) → ℝ≥0∞) (g • s) = HMul.hMul (β := ℝ≥0∞) (↑r : ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g : G
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
s : Set A
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0
hμgs : (μ : (a : Set A) → ℝ≥0∞) (g • s) = HMul.hMul (β := ℝ≥0∞) (↑r : ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [*]
-- 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
f : CompactlySupportedContinuousMap B E
b : B
a : A
⊢ Eq.{u_4 + 1} (α := E) ((H.pullback f b : (a : A) → E) a : E)
    ((f : (a : B) → E) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)) : E)

Tactic:
f.pullback_monoidHom_def H.isClosedEmbedding b a

Premises used: TopologicalGroup.IsSES.isClosedEmbedding, CompactlySupportedContinuousMap.pullback_monoidHom_def
-- 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
f : CompactlySupportedContinuousMap B E
b : B
⊢ Eq.{u_3 + 1} (α := C)
    ((ψ : (a : B) → C)
        ((Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ *
          b) :
      C)
    (1 : C)

Tactic:
simp [Function.apply_invFun_apply]

Premises used: 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
f : CompactlySupportedContinuousMap B E
b : B
⊢ Eq.{u_3 + 1} (α := C)
    ((ψ : (a : B) → C)
        ((Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ *
          b) :
      C)
    (1 : C)

Tactic:
have h : ψ ((Function.invFun ψ (ψ b))⁻¹ * b) = 1 := by simp [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
f : CompactlySupportedContinuousMap B E
b : B
h :
  Eq.{u_3 + 1} (α := C)
    ((ψ : (a : B) → C)
        ((Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ *
          b) :
      C)
    (1 : C)
⊢ (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C))⁻¹ * b ∈
    φ.range

Tactic:
rw [← ψ.mem_ker, H.mulExact.monoidHom_ker_eq] at h

Premises used: Function.MulExact.monoidHom_ker_eq, MonoidHom.mem_ker, 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
f : CompactlySupportedContinuousMap B E
b : B
h :
  (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),
    Eq.{u_4 + 1} (α := E)
      (∫ (a : A),
        (H.pullback f
              (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C)
                ((ψ : (a : B) → C) b : C)) :
            (a : A) → E)
          a ∂μA)
      (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA)
⊢ Eq.{u_4 + 1} (α := E)
    (∫ (a : A),
      (H.pullback f
            (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C)) :
          (a : A) → E)
        a ∂μA)
    (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA)

Tactic:
obtain ⟨a, ha⟩ := h
-- 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
f : CompactlySupportedContinuousMap B E
b : B
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
rw :
  Eq.{u_4 + 1} (α := E)
    (∫ (x : A),
      (H.pullback f
            (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C)) :
          (a : A) → E)
        (a * x) ∂μA)
    (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA)
⊢ Eq.{u_4 + 1} (α := E)
    (∫ (a : A),
      (H.pullback f
            (Function.invFun.{u_2 + 1, u_3 + 1} (β := C) ((⇑ψ : (a : B) → C) : (a : B) → C) ((ψ : (a : B) → C) b : C)) :
          (a : A) → E)
        a ∂μA)
    (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA)

Tactic:
rw [← integral_mul_left_eq_self _ a]

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

Tactic:
simp [pullback_def, ha, 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
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
simp_rw :
  ∀ (a : B),
    ∀ ε > 0,
      ∀ᶠ (x : B) in nhds a,
        dist.{u_4} (α := E) (∫ (a : A), (H.pullback f x : (a : A) → E) a ∂μA)
            (∫ (a_2 : A), (H.pullback f a : (a : A) → E) a_2 ∂μA) <
          ε
⊢ Continuous.{u_3, u_4} (Y := E) fun (c : C) ↦
    ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA

Tactic:
simp_rw [← H.isOpenQuotientMap.continuous_comp_iff, Function.comp_def,
        integral_pullback_invFun_apply, Metric.continuous_iff']

Premises used: TopologicalGroup.IsSES.integral_pullback_invFun_apply, IsOpenQuotientMap.continuous_comp_iff, Metric.continuous_iff', Function.comp_def, TopologicalGroup.IsSES.isOpenQuotientMap
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
obtain :
  ∀ (U₀ : Set B) (hU₀ : IsCompact U₀) (hb : U₀ ∈ nhds b),
    ∀ᶠ (x : B) in nhds b,
      dist.{u_4} (α := E) (∫ (a : A), (H.pullback f x : (a : A) → E) a ∂μA)
          (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA) <
        ε
⊢ ∀ᶠ (x : B) in nhds b,
    dist.{u_4} (α := E) (∫ (a : A), (H.pullback f x : (a : A) → E) a ∂μA)
        (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA) <
      ε

Tactic:
obtain ⟨U₀, hU₀, hb⟩ := exists_compact_mem_nhds b

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
obtain :
  ∀ (K : Set B) (hK : IsCompact K) (hf₀ : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)),
    ∀ᶠ (x : B) in nhds b,
      dist.{u_4} (α := E) (∫ (a : A), (H.pullback f x : (a : A) → E) a ∂μA)
          (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA) <
        ε
⊢ ∀ᶠ (x : B) in nhds b,
    dist.{u_4} (α := E) (∫ (a : A), (H.pullback f x : (a : A) → E) a ∂μA)
        (∫ (a : A), (H.pullback f b : (a : A) → E) a ∂μA) <
      ε

Tactic:
obtain ⟨K, hK, hf₀⟩ := exists_compact_iff_hasCompactSupport.mpr f.hasCompactSupport

Premises used: Iff.mpr, CompactlySupportedContinuousMap.hasCompactSupport, exists_compact_iff_hasCompactSupport
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
S : Set A := (⇑φ : (a : A) → B) ⁻¹' (U₀⁻¹ * K)
⊢ IsCompact S

Tactic:
have hSc : IsCompact S := H.isClosedEmbedding.isCompact_preimage (hU₀.inv.mul hK)
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
S : Set A := (⇑φ : (a : A) → B) ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
rw : ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
⊢ ∃ δ > 0, HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε

Tactic:
rw [← ENNReal.ofReal_toReal hSc.measure_ne_top, ← measureReal_def]

Premises used: ENNReal.ofReal_toReal, MeasureTheory.measureReal_def, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
S : Set A := (⇑φ : (a : A) → B) ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
pos : ∀ (hS' : μA.real S = 0), ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
neg : ∀ (hS' : ¬μA.real S = 0), ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
⊢ ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε

Tactic:
by_cases hS' : μA.real S = 0

Premises used: MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
S : Set A := (⇑φ : (a : A) → B) ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : μA.real S = 0
⊢ ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε

Tactic:
simp [hS', hε, exists_gt]

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
S : Set A := (⇑φ : (a : A) → B) ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : ¬μA.real S = 0
⊢ ε / 2 / μA.real S > 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
S : Set A := (⇑φ : (a : A) → B) ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : ¬μA.real S = 0
neg : ENNReal.ofReal (ε / 2 / μA.real S) * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
⊢ ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε

Tactic:
refine ⟨ε / 2 / μA.real S, by positivity, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
S : Set A := (⇑φ : (a : A) → B) ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : ¬μA.real S = 0
neg : ENNReal.ofReal (ε / 2 / μA.real S * μA.real S) < ENNReal.ofReal ε
neg₁ : ε / 2 / μA.real S * μA.real S < ε
neg₂ : ε / 2 < ε
neg₃ neg₄ neg₅ neg₆ : 0 < ε
⊢ ENNReal.ofReal (ε / 2 / μA.real S) * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε

Tactic:
rwa [← ENNReal.ofReal_mul' measureReal_nonneg, ENNReal.ofReal_lt_ofReal_iff hε,
            div_mul_cancel₀ _ hS', half_lt_self_iff]

Premises used: div_mul_cancel₀, MeasureTheory.measureReal_nonneg, half_lt_self_iff, ENNReal.ofReal_lt_ofReal_iff, ENNReal.ofReal_mul'