awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
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
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
g : G
s : Set A
this :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set A) → ℝ≥0∞) (g • s) : ℝ≥0∞)
rw :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HSMul.hSMul (α := ℝ≥0) (β := ℝ≥0∞) (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g : ℝ≥0)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HSMul.hSMul (β := ℝ≥0∞)
      ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₃ :
  (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s =
    HSMul.hSMul (β := ℝ≥0∞)
      ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₄ :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
    (((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ • μ :
          (a : Set A) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set A) → ℝ≥0∞) (g • s)
have rw₅ : Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
  ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
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∞)
⊢ ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g = r
have refine : (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞) = (↑r : ℝ≥0∞)
Tactic: refine ENNReal.coe_injective ?_
-- 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
f : CompactlySupportedContinuousMap B E
b : 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)
have 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)
Tactic: have h : ψ ((Function.invFun ψ (ψ b))⁻¹ * b) = 1 := by simp [Function.apply_invFun_apply]
-- 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
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)
⊢ 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)
have h₁ : (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
Cleared hypotheses: h
-- 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
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
⊢ 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)
have 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)
Tactic: obtain ⟨a, ha⟩ := h
Cleared hypotheses: h
-- 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
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)
    (∫ (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)
have 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)
Tactic: rw [← integral_mul_left_eq_self _ a]
-- 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
⊢ 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
have 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) <
        ε
Tactic: simp_rw [← H.isOpenQuotientMap.continuous_comp_iff, Function.comp_def,
        integral_pullback_invFun_apply, Metric.continuous_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
⊢ ∀ᶠ (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₀ : 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) <
      ε
Tactic: obtain ⟨U₀, hU₀, hb⟩ := exists_compact_mem_nhds b
-- 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
⊢ ∀ᶠ (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 : ∀ (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) <
      ε
Tactic: obtain ⟨K, hK, hf₀⟩ := exists_compact_iff_hasCompactSupport.mpr f.hasCompactSupport
-- 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)
⊢ ∀ᶠ (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 hSc : IsCompact S
Tactic: have hSc : IsCompact S := H.isClosedEmbedding.isCompact_preimage (hU₀.inv.mul hK)
-- 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
⊢ ∃ δ > 0, HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA : (a : Set A) → ENNReal) S : ENNReal) < ENNReal.ofReal ε
have rw : ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
Tactic: rw [← ENNReal.ofReal_toReal hSc.measure_ne_top, ← measureReal_def]
-- 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
⊢ ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
have pos : ∀ (hS' : μA.real S = 0), ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
Tactic: by_cases hS' : μA.real S = 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
pos : ∀ (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 ε
have neg : ∀ (hS' : ¬μA.real S = 0), ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
Tactic: by_cases hS' : μA.real S = 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
hS' : ¬μA.real S = 0
⊢ ∃ δ > 0, ENNReal.ofReal δ * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
have neg : ENNReal.ofReal (ε / 2 / μA.real S) * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
Tactic: refine ⟨ε / 2 / μA.real S, by positivity, ?_⟩
-- 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
hS' : ¬μA.real S = 0
⊢ ENNReal.ofReal (ε / 2 / μA.real S) * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
have neg : ENNReal.ofReal (ε / 2 / μA.real S * μ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]
-- 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
hS' : ¬μA.real S = 0
neg : ENNReal.ofReal (ε / 2 / μA.real S * μA.real S) < ENNReal.ofReal ε
⊢ ENNReal.ofReal (ε / 2 / μA.real S) * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
have neg₁ : ε / 2 / μA.real S * μA.real S < ε
Tactic: 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
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 < ε
⊢ ENNReal.ofReal (ε / 2 / μA.real S) * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
have neg₂ : ε / 2 < ε
Tactic: 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
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 < ε
⊢ ENNReal.ofReal (ε / 2 / μA.real S) * ENNReal.ofReal (μA.real S) < ENNReal.ofReal ε
have neg₃ : 0 < ε
Tactic: rwa [← ENNReal.ofReal_mul' measureReal_nonneg, ENNReal.ofReal_lt_ofReal_iff hε,
            div_mul_cancel₀ _ hS', half_lt_self_iff]