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
ε : ℝ
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 :
  ∀ 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),
    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:
have h (a) (ha : a ∈ S) : edist (H.pullback f (t * b) a) (H.pullback f b a) ≤ .ofReal δ := by
        rw [edist_dist]
        exact ENNReal.ofReal_le_ofReal (@hf ⟨t * b * φ a, b * φ a⟩ (by simpa)).le
-- 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 :
  ∀ 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₀
h :
  ∀ (a : A) (ha : a ∈ S),
    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 δ
grw :
  (∫⁻ (x : A) in S,
        edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) x : E)
          ((H.pullback f b : (a : A) → E) x : E) ∂μA).toReal <
    ε
grw₁ :
  (Function.support (M := ENNReal) fun (a : A) ↦
      edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) a : E) ((H.pullback f b : (a : A) → E) a : E)) ⊆
    S
grw₂ : Set A
⊢ Membership.mem (γ := Set B)
    {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}
    ((fun (x1 x2 : B) ↦ x1 * x2) t b)

Tactic:
grw [Set.mem_setOf_eq, dist_integral_le_lintegral_edist (H.pullback f (t * b)).integrable
        (H.pullback f b).integrable, ← setLIntegral_eq_of_support_subset]

Premises used: HMul.hMul, CompactlySupportedContinuousMap.integrable, Set.mem_setOf_eq, MeasureTheory.setLIntegral_eq_of_support_subset, TopologicalGroup.IsSES.pullback, MeasureTheory.dist_integral_le_lintegral_edist
-- 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 :
  ∀ 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₀
h :
  ∀ (a : A) (ha : a ∈ S),
    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 δ
⊢ (∫⁻ (x : A) in S,
        edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) x : E)
          ((H.pullback f b : (a : A) → E) x : E) ∂μA).toReal <
    ε

Tactic:
ENNReal.toReal_lt_of_lt_ofReal ((setLIntegral_mono measurable_const h).trans_lt ?_)

Premises used: ENNReal.toReal_lt_of_lt_ofReal, MeasureTheory.setLIntegral_mono, measurable_const, LE.le.trans_lt
-- 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 :
  ∀ 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₀
h :
  ∀ (a : A) (ha : a ∈ S),
    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 δ
refine : ∫⁻ (x : A) in S, ENNReal.ofReal δ ∂μA < ENNReal.ofReal ε
⊢ (∫⁻ (x : A) in S,
        edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) x : E)
          ((H.pullback f b : (a : A) → E) x : E) ∂μA).toReal <
    ε

Tactic:
refine ENNReal.toReal_lt_of_lt_ofReal ((setLIntegral_mono measurable_const h).trans_lt ?_)

Premises used: ENNReal.toReal_lt_of_lt_ofReal, MeasureTheory.setLIntegral_mono, measurable_const, LE.le.trans_lt
-- 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 :
  ∀ 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₀
h :
  ∀ (a : A) (ha : a ∈ S),
    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 δ
rwa :
  HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA.restrict S : (a : Set A) → ENNReal) Set.univ : ENNReal) <
    ENNReal.ofReal ε
rwa₁ rwa₂ rwa₃ rwa₄ :
  HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
⊢ ∫⁻ (x : A) in S, ENNReal.ofReal δ ∂μA < ENNReal.ofReal ε

Tactic:
rwa [lintegral_const, restrict_apply_univ]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply_univ
-- 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 :
  ∀ 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₀
h :
  ∀ (a : A) (ha : a ∈ S),
    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 δ
y : A
hy :
  Membership.mem (γ := Set A)
    (Function.support (M := ENNReal) fun (a : A) ↦
      edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) a : E) ((H.pullback f b : (a : A) → E) a : E))
    y
contrapose :
  ∀ (hy : y ∉ S),
    y ∉
      Function.support (M := ENNReal) fun (a : A) ↦
        edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) a : E) ((H.pullback f b : (a : A) → E) a : E)
⊢ y ∈ S

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
ε : ℝ
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 :
  ∀ 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₀
h :
  ∀ (a : A) (ha : a ∈ S),
    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 δ
y : A
hy : y ∉ S
rw : edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) y : E) ((H.pullback f b : (a : A) → E) y : E) = 0
rw₁ : edist.{u_4} (α := E) (0 : E) ((H.pullback f b : (a : A) → E) y : E) = 0
rw₂ : edist.{u_4} (α := E) 0 0 = 0
rw₃ rw₄ : Eq (α := ENNReal) 0 0
⊢ y ∉
    Function.support (M := ENNReal) fun (a : A) ↦
      edist.{u_4} (α := E) ((H.pullback f (t * b) : (a : A) → E) a : E) ((H.pullback f b : (a : A) → E) a : E)

Tactic:
rw [Function.notMem_support, hS htb hy, hS (mem_of_mem_nhds hb) hy, edist_self]

Premises used: mem_of_mem_nhds, PseudoEMetricSpace.edist_self, Function.notMem_support
-- 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
obtain :
  ∀ (K : Set B) (hK : IsCompact K) (hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)),
    HasCompactSupport.{u_3, u_4} (β := E) fun (c : C) ↦
      ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA
⊢ HasCompactSupport.{u_3, u_4} (β := E) fun (c : C) ↦
    ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (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
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
⊢ HasCompactSupport.{u_3, u_4} (β := E) fun (c : C) ↦
    ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA

Tactic:
exists_compact_iff_hasCompactSupport.mp
        ⟨ψ '' K, hK.image H.isOpenQuotientMap.continuous, fun x hx ↦ ?_⟩

Premises used: IsOpenQuotientMap.continuous, exists_compact_iff_hasCompactSupport, TopologicalGroup.IsSES.isOpenQuotientMap, And.intro, Exists.intro, Iff.mp, Set.image, IsCompact.image, 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
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
refine :
  ∀ (x : C) (hx : x ∉ (⇑ψ : (a : B) → C) '' K),
    Eq.{u_4 + 1} (α := E) (∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) x) : (a : A) → E) a ∂μA) 0
⊢ HasCompactSupport.{u_3, u_4} (β := E) fun (c : C) ↦
    ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) c) : (a : A) → E) a ∂μA

Tactic:
refine exists_compact_iff_hasCompactSupport.mp
        ⟨ψ '' K, hK.image H.isOpenQuotientMap.continuous, fun x hx ↦ ?_⟩

Premises used: IsOpenQuotientMap.continuous, exists_compact_iff_hasCompactSupport, TopologicalGroup.IsSES.isOpenQuotientMap, And.intro, Exists.intro, Iff.mp, Set.image, IsCompact.image, 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
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
x : C
hx : x ∉ (⇑ψ : (a : B) → C) '' K
this :
  ∀ (a : A),
    Eq.{u_4 + 1} (α := E)
      ((f : (a : B) → E)
          (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
        E)
      (0 : E)
⊢ Eq.{u_4 + 1} (α := E) (∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) x) : (a : A) → E) a ∂μA) 0

Tactic:
simp [this, pullback_def]

Premises used: TopologicalGroup.IsSES.pullback_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
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
x : C
hx : x ∉ (⇑ψ : (a : B) → C) '' K
suffices :
  ∀ (a : A),
    Eq.{u_4 + 1} (α := E)
      ((f : (a : B) → E)
          (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
        E)
      (0 : E)
⊢ Eq.{u_4 + 1} (α := E) (∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) x) : (a : A) → E) a ∂μA) 0

Tactic:
suffices ∀ a : A, f (Function.invFun ψ x * φ a) = 0 by simp [this, pullback_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
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
K : Set B
hK : IsCompact K
hf : ∀ x ∉ K, Eq.{u_4 + 1} (α := E) ((f : (a : B) → E) x : E) (0 : E)
x : C
hx : x ∉ (⇑ψ : (a : B) → C) '' K
⊢ ∀ (a : A),
    Eq.{u_4 + 1} (α := E)
      ((f : (a : B) → E)
          (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
        E)
      (0 : E)

Tactic:
fun a ↦ hf _ (mt (Set.mem_image_of_mem ψ) ?_)

Premises used: Function.invFun, HMul.hMul, mt, Set.mem_image_of_mem, DFunLike.coe