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
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
obtain :
  ∀ (δ : ℝ) (hδ0 : δ > 0)
    (hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε),
    ∀ᶠ (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 ⟨δ, hδ0, hδ⟩ : ∃ δ > 0, ENNReal.ofReal δ * μA S < ENNReal.ofReal ε := by
        rw [← ENNReal.ofReal_toReal hSc.measure_ne_top, ← measureReal_def]
        by_cases hS' : μA.real S = 0
        · simp [hS', hε, exists_gt]
        · refine ⟨ε / 2 / μA.real S, by positivity, ?_⟩
          rwa [← ENNReal.ofReal_mul' measureReal_nonneg, ENNReal.ofReal_lt_ofReal_iff hε,
            div_mul_cancel₀ _ hS', half_lt_self_iff]

Premises used: ENNReal.ofReal, DFunLike.coe
-- 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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
x : B
hx : x ∈ U₀
y : A
hy : y ∉ S
contrapose! : ∀ (hy : Ne.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)), y ∈ S
⊢ Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)

Tactic:
contrapose! hy
-- 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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
x : B
hx : x ∈ U₀
y : A
hy : Ne.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
⊢ y ∈ S

Tactic:
Set.mem_mul.mpr ⟨x⁻¹, Set.inv_mem_inv.mpr hx, x * φ y,
          not_imp_comm.mp (hf₀ (x * φ y)) hy, inv_mul_cancel_left x (φ y)⟩

Premises used: Iff.mpr, HMul.hMul, inv_mul_cancel_left, Set.Mem, not_imp_comm, setOf, Set.inv_mem_inv, Inv.inv, Set.preimage, And.intro, Exists.intro, Iff.mp, DFunLike.coe, Set.mem_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
x : B
hx : x ∈ U₀
y : A
hy : Ne.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
⊢ y ∈ S

Tactic:
exact Set.mem_mul.mpr ⟨x⁻¹, Set.inv_mem_inv.mpr hx, x * φ y,
          not_imp_comm.mp (hf₀ (x * φ y)) hy, inv_mul_cancel_left x (φ y)⟩

Premises used: Iff.mpr, HMul.hMul, inv_mul_cancel_left, not_imp_comm, Set.inv_mem_inv, Inv.inv, And.intro, Exists.intro, Iff.mp, DFunLike.coe, Set.mem_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
⊢ ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)

Tactic:
have hS {x} (hx : x ∈ U₀) {y} (hy : y ∉ S) : H.pullback f x y = 0 := by
        contrapose! hy
        exact Set.mem_mul.mpr ⟨x⁻¹, Set.inv_mem_inv.mpr hx, x * φ y,
          not_imp_comm.mp (hf₀ (x * φ y)) hy, inv_mul_cancel_left x (φ y)⟩
-- 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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
hS : ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
⊢ UniformContinuous.{u_2, u_4} (α := B) (β := E) (⇑f : (a : B) → E)

Tactic:
have ha := f.hasCompactSupport.uniformContinuous_of_continuous f.continuous
-- 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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
hS : ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
ha : UniformContinuous.{u_2, u_4} (α := B) (β := E) (⇑f : (a : B) → E)
⊢ ∀ r ∈ uniformity E,
    ∀ᶠ (x : B × B) in uniformity B,
      Membership.mem (α := E × E) r (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E)

Tactic:
rw [uniformContinuous_iff_eventually] at ha

Premises used: uniformContinuous_iff_eventually
-- 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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
hS : ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
ha :
  ∀ r ∈ uniformity E,
    ∀ᶠ (x : B × B) in uniformity B,
      Membership.mem (α := E × E) r (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E)
obtain :
  ∀ (U : Set B) (hU : Membership.mem (γ := Filter B) (nhds 1) U)
    (hf :
      Subset (α := Set (B × B)) ((fun (p : B × B) ↦ p.2 * p.1⁻¹) ⁻¹' U)
        {x : B × B |
          (fun (x : B × B) ↦
              Membership.mem.{u_4, u_4} (α := E × E) (γ := Set (E × E)) {p : E × E | dist p.1 p.2 < δ}
                (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E))
            x}),
    ∀ᶠ (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, hf⟩ := ha _ (Metric.dist_mem_uniformity hδ0)

Premises used: Metric.dist_mem_uniformity
-- 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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
hS : ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
ha :
  ∀ r ∈ uniformity E,
    ∀ᶠ (x : B × B) in uniformity B,
      Membership.mem (α := E × E) r (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E)
U : Set B
hU : Membership.mem (γ := Filter B) (nhds 1) U
hf :
  Subset (α := Set (B × B)) ((fun (p : B × B) ↦ p.2 * p.1⁻¹) ⁻¹' U)
    {x : B × B |
      (fun (x : B × B) ↦
          Membership.mem.{u_4, u_4} (α := E × E) (γ := Set (E × E)) {p : E × E | dist p.1 p.2 < δ}
            (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E))
        x}
⊢ ∀ᶠ (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:
Filter.mem_of_superset (Filter.inter_mem
        (mul_singleton_mem_nhds_of_nhds_one b (inv_mem_nhds_one B hU)) hb) ?_

Premises used: Filter.Eventually, Filter.inter_mem, inv_mem_nhds_one, mul_singleton_mem_nhds_of_nhds_one, Filter.mem_of_superset
-- 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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
hS : ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
ha :
  ∀ r ∈ uniformity E,
    ∀ᶠ (x : B × B) in uniformity B,
      Membership.mem (α := E × E) r (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E)
U : Set B
hU : Membership.mem (γ := Filter B) (nhds 1) U
hf :
  Subset (α := Set (B × B)) ((fun (p : B × B) ↦ p.2 * p.1⁻¹) ⁻¹' U)
    {x : B × B |
      (fun (x : B × B) ↦
          Membership.mem.{u_4, u_4} (α := E × E) (γ := Set (E × E)) {p : E × E | dist p.1 p.2 < δ}
            (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E))
        x}
refine :
  U⁻¹ * {b} ∩ U₀ ⊆
    {x : B |
      (fun (x : 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}
⊢ ∀ᶠ (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:
refine Filter.mem_of_superset (Filter.inter_mem
        (mul_singleton_mem_nhds_of_nhds_one b (inv_mem_nhds_one B hU)) hb) ?_

Premises used: Filter.inter_mem, inv_mem_nhds_one, mul_singleton_mem_nhds_of_nhds_one, Filter.mem_of_superset
-- 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
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
hS : ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
ha_1 :
  ∀ r ∈ uniformity E,
    ∀ᶠ (x : B × B) in uniformity B,
      Membership.mem (α := E × E) r (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E)
U : Set B
hU : Membership.mem (γ := Filter B) (nhds 1) U
hf :
  Subset (α := Set (B × B)) ((fun (p : B × B) ↦ p.2 * p.1⁻¹) ⁻¹' U)
    {x : B × B |
      (fun (x : B × B) ↦
          Membership.mem.{u_4, u_4} (α := E × E) (γ := Set (E × E)) {p : E × E | dist p.1 p.2 < δ}
            (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E))
        x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun (x1 x2 : B) ↦ x1 * x2) t b ∈ U₀
a : A
ha : a ∈ S
rw :
  ENNReal.ofReal
      (dist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) a : E) ((H.pullback f b : (a : A) → E) a : E)) ≤
    ENNReal.ofReal δ
⊢ edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) a : E) ((H.pullback f b : (a : A) → E) a : E) ≤
    ENNReal.ofReal δ

Tactic:
rw [edist_dist]

Premises used: edist_dist
-- 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
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
hS : ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
ha_1 :
  ∀ r ∈ uniformity E,
    ∀ᶠ (x : B × B) in uniformity B,
      Membership.mem (α := E × E) r (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E)
U : Set B
hU : Membership.mem (γ := Filter B) (nhds 1) U
hf :
  Subset (α := Set (B × B)) ((fun (p : B × B) ↦ p.2 * p.1⁻¹) ⁻¹' U)
    {x : B × B |
      (fun (x : B × B) ↦
          Membership.mem.{u_4, u_4} (α := E × E) (γ := Set (E × E)) {p : E × E | dist p.1 p.2 < δ}
            (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E))
        x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun (x1 x2 : B) ↦ x1 * x2) t b ∈ U₀
a : A
ha : a ∈ S
⊢ Membership.mem (γ := Set (B × B)) ((fun (p : B × B) ↦ p.2 * p.1⁻¹) ⁻¹' U)
    (HMul.hMul (β := B) (t * b) ((φ : (a : A) → B) a : B), HMul.hMul (β := B) b ((φ : (a : A) → B) a : B))

Tactic:
simpa
-- 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
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
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
δ : ℝ
hδ0 : δ > 0
hδ : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
hS : ∀ {x : B} (hx : x ∈ U₀) {y : A} (hy : y ∉ S), Eq.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)
ha_1 :
  ∀ r ∈ uniformity E,
    ∀ᶠ (x : B × B) in uniformity B,
      Membership.mem (α := E × E) r (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E)
U : Set B
hU : Membership.mem (γ := Filter B) (nhds 1) U
hf :
  Subset (α := Set (B × B)) ((fun (p : B × B) ↦ p.2 * p.1⁻¹) ⁻¹' U)
    {x : B × B |
      (fun (x : B × B) ↦
          Membership.mem.{u_4, u_4} (α := E × E) (γ := Set (E × E)) {p : E × E | dist p.1 p.2 < δ}
            (((f : (a : B) → E) x.1, (f : (a : B) → E) x.2) : E × E))
        x}
t : B
ht : t ∈ U⁻¹
b : B
hb : U₀ ∈ nhds b
htb : (fun (x1 x2 : B) ↦ x1 * x2) t b ∈ U₀
a : A
ha : a ∈ S
⊢ ENNReal.ofReal
      (dist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) a : E) ((H.pullback f b : (a : A) → E) a : E)) ≤
    ENNReal.ofReal δ

Tactic:
exact ENNReal.ofReal_le_ofReal (@hf ⟨t * b * φ a, b * φ a⟩ (by simpa)).le

Premises used: ENNReal.ofReal_le_ofReal, LT.lt.le