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
ε : ℝ
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, ENNReal.ofReal δ ∂μA < ENNReal.ofReal ε
have rwa : HMul.hMul (β := ENNReal) (ENNReal.ofReal δ) ((μA.restrict S : (a : Set A) → ENNReal) Set.univ : ENNReal) <
  ENNReal.ofReal ε
Tactic: rwa [lintegral_const, restrict_apply_univ]
-- 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 δ
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
⊢ y ∈ S
have 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)
Tactic: contrapose hy
Cleared hypotheses: hy
-- 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 δ
y : A
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)
have 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
Tactic: rw [Function.notMem_support, hS htb hy, hS (mem_of_mem_nhds hb) hy, edist_self]
-- 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 δ
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
⊢ 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)
have rw₁ : edist.{u_4} (α := E) (0 : E) ((H.pullback f b : (a : A) → E) y : E) = 0
Tactic: rw [Function.notMem_support, hS htb hy, hS (mem_of_mem_nhds hb) hy, edist_self]
-- 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 δ
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
⊢ 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)
have rw₂ : edist.{u_4} (α := E) 0 0 = 0
Tactic: rw [Function.notMem_support, hS htb hy, hS (mem_of_mem_nhds hb) hy, edist_self]
-- 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 δ
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
⊢ 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)
have rw₃ : Eq (α := ENNReal) 0 0
Tactic: rw [Function.notMem_support, hS htb hy, hS (mem_of_mem_nhds hb) hy, edist_self]
-- 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
⊢ 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
have 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
Tactic: obtain ⟨K, hK, hf⟩ := exists_compact_iff_hasCompactSupport.mpr f.hasCompactSupport
-- 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
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
have 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
Tactic: refine exists_compact_iff_hasCompactSupport.mp
        ⟨ψ '' K, hK.image H.isOpenQuotientMap.continuous, fun x hx ↦ ?_⟩
-- 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
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
⊢ Eq.{u_4 + 1} (α := E) (∫ (a : A), (H.pullback f (Function.invFun (⇑ψ : (a : B) → C) x) : (a : A) → E) a ∂μA) 0
have 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)
Tactic: suffices ∀ a : A, f (Function.invFun ψ x * φ a) = 0 by simp [this, pullback_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
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)
have refine : ∀ (a : A),
  ((ψ : (a : B) → C)
        (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
      C) ∉
    (⇑ψ : (a : B) → C) '' K
Tactic: refine fun a ↦ hf _ (mt (Set.mem_image_of_mem ψ) ?_)
-- 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
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
⊢ ((ψ : (a : B) → C)
        (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
      C) ∉
    (⇑ψ : (a : B) → C) '' K
have rwa : HMul.hMul (α := C) (β := C) ((ψ : (a : B) → C) (Function.invFun (⇑ψ : (a : B) → C) x) : C)
    ((ψ : (a : B) → C) ((φ : (a : A) → B) a : B) : C) ∉
  (⇑ψ : (a : B) → C) '' K
Tactic: rwa [map_mul, Function.rightInverse_invFun H.isOpenQuotientMap.surjective,
        H.mulExact.apply_apply_eq_one, mul_one]
-- 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
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
rwa :
  HMul.hMul (α := C) (β := C) ((ψ : (a : B) → C) (Function.invFun (⇑ψ : (a : B) → C) x) : C)
      ((ψ : (a : B) → C) ((φ : (a : A) → B) a : B) : C) ∉
    (⇑ψ : (a : B) → C) '' K
⊢ ((ψ : (a : B) → C)
        (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
      C) ∉
    (⇑ψ : (a : B) → C) '' K
have rwa₁ : HMul.hMul (β := C) x ((ψ : (a : B) → C) ((φ : (a : A) → B) a : B) : C) ∉ (⇑ψ : (a : B) → C) '' K
Tactic: rwa [map_mul, Function.rightInverse_invFun H.isOpenQuotientMap.surjective,
        H.mulExact.apply_apply_eq_one, mul_one]
-- 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
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
rwa :
  HMul.hMul (α := C) (β := C) ((ψ : (a : B) → C) (Function.invFun (⇑ψ : (a : B) → C) x) : C)
      ((ψ : (a : B) → C) ((φ : (a : A) → B) a : B) : C) ∉
    (⇑ψ : (a : B) → C) '' K
rwa₁ : HMul.hMul (β := C) x ((ψ : (a : B) → C) ((φ : (a : A) → B) a : B) : C) ∉ (⇑ψ : (a : B) → C) '' K
⊢ ((ψ : (a : B) → C)
        (HMul.hMul (α := B) (β := B) (Function.invFun (⇑ψ : (a : B) → C) x : B) ((φ : (a : A) → B) a : B)) :
      C) ∉
    (⇑ψ : (a : B) → C) '' K
have rwa₂ : x * 1 ∉ (⇑ψ : (a : B) → C) '' K
Tactic: rwa [map_mul, Function.rightInverse_invFun H.isOpenQuotientMap.surjective,
        H.mulExact.apply_apply_eq_one, mul_one]