awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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
⊢ ∀ᶠ (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) <
      ε
have 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) <
      ε
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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)
have contrapose! : ∀ (hy : Ne.{u_4 + 1} (α := E) ((H.pullback f x : (a : A) → E) y : E) (0 : E)), y ∈ S
Tactic: contrapose! hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
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) 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) <
      ε
have 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)
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)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
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)
⊢ ∀ᶠ (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) <
      ε
have ha : UniformContinuous.{u_2, u_4} (α := B) (β := E) (⇑f : (a : B) → E)
Tactic: have ha := f.hasCompactSupport.uniformContinuous_of_continuous f.continuous
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
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)
⊢ ∀ᶠ (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) <
      ε
have 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)
Tactic: rw [uniformContinuous_iff_eventually] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
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)
⊢ ∀ᶠ (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) <
      ε
have 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) <
      ε
Tactic: obtain ⟨U, hU, hf⟩ := ha _ (Metric.dist_mem_uniformity hδ0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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) <
      ε
have 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}
Tactic: refine Filter.mem_of_superset (Filter.inter_mem
        (mul_singleton_mem_nhds_of_nhds_one b (inv_mem_nhds_one B hU)) hb) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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
⊢ 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 δ
have 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 δ
Tactic: rw [edist_dist]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : NormedAddCommGroup E
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_11 : NormedSpace ℝ E
inst_12 : IsTopologicalGroup C
inst_13 : LocallyCompactSpace B
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₀
⊢ 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)
have 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 δ
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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 δ
⊢ 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)
have 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 <
  ε
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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 <
    ε
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Extension (goal)
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 <
    ε
have refine : ∫⁻ (x : A) in S, ENNReal.ofReal δ ∂μA < ENNReal.ofReal ε
Tactic: refine ENNReal.toReal_lt_of_lt_ofReal ((setLIntegral_mono measurable_const h).trans_lt ?_)