mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst✝⁸, _] g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ 0 < ν (support ((fun f ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }))

pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst✝⁸, _] g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ Integrable ((fun f ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }) ν

Tactic:
·

Goal state after:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst✝⁸, _] g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ 0 < ν (support ((fun f ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }))
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst✝⁸, _] g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ Integrable ((fun f ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }) ν

Tactic:
·

Goal state after:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
μ' μ ν : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : ν.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst✝⁸, _] g
g_comp : HasCompactSupport ⇑{ toFun := g, continuous_toFun := g_cont }
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont }
g_one : { toFun := g, continuous_toFun := g_cont } 1 ≠ 0
Z : μ'.haarScalarFactor ν • ∫ (x : G), g x ∂ν = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ∫ (x : G), g x ∂ν
⊢ Integrable ((fun f ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }) ν
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ ∀ (x : E), (fun x ↦ (f x + f (-x)) / 2) (-x) = (fun x ↦ (f x + f (-x)) / 2) x

Tactic:
·

Goal state after:
case refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
⊢ ∀ (x : E), (fun x ↦ (f x + f (-x)) / 2) (-x) = (fun x ↦ (f x + f (-x)) / 2) x
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case neg
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : ¬LocallyCompactSpace G
⊢ (map (⇑φ) μ').haarScalarFactor (map (⇑φ) μ) = μ'.haarScalarFactor μ

pp: case pos
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
⊢ (map (⇑φ) μ').haarScalarFactor (map (⇑φ) μ) = μ'.haarScalarFactor μ

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : ¬LocallyCompactSpace G
⊢ (map (⇑φ) μ').haarScalarFactor (map (⇑φ) μ) = μ'.haarScalarFactor μ
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ Integrable u μ

pp: case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (support u)

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ Integrable u μ
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (support u)

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (support u)
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
p : P
x : G
hp : p ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
M1 : s ∈ 𝓝 p
⊢ uncurry g =ᶠ[𝓝 p ×ˢ 𝓝 x] fun x ↦ 0

Tactic:
filter_upwards [prod_mem_prod M1 M2]

Goal state after:
𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
p : P
x : G
hp : p ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
M1 : s ∈ 𝓝 p
⊢ ∀ a ∈ s ×ˢ kᶜ, uncurry g a = 0
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i : Ordinal.{u}
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
g : ℕ → Ordinal.{u}
n : ℕ
hN : IsEmpty (SatelliteConfig α n p.τ)
IH : ∀ y < i, y < p.lastStep → p.color y < n
N_mem : n ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = n
hg :
  ∀ k < n,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n_1 ↦ if n_1 = n then i else g n_1
color_G : ∀ n_1 ≤ n, p.color (G n_1) = n_1
hn : n ≤ n
⊢ G n < p.lastStep

pp: case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
n : ℕ
hn : n ≤ N
H : n < N
⊢ G n < p.lastStep

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i : Ordinal.{u}
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
g : ℕ → Ordinal.{u}
n : ℕ
hN : IsEmpty (SatelliteConfig α n p.τ)
IH : ∀ y < i, y < p.lastStep → p.color y < n
N_mem : n ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = n
hg :
  ∀ k < n,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n_1 ↦ if n_1 = n then i else g n_1
color_G : ∀ n_1 ≤ n, p.color (G n_1) = n_1
hn : n ≤ n
⊢ G n < p.lastStep
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
p✝ : P
x : G
hp✝ : p✝ ∈ s
hx : x ∉ k
M2 : kᶜ ∈ 𝓝 x
M1 : s ∈ 𝓝 p✝
p : P
y : G
hp : (p, y).1 ∈ s
hy : (p, y).2 ∈ kᶜ
⊢ uncurry g (p, y) = 0

Tactic:
exact hgs p y hp hy

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
n : ℕ
hn : n ≤ N
H : n < N
⊢ G n < p.lastStep

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
n : ℕ
hn : n ≤ N
H : n < N
⊢ G n < p.lastStep
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case h1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, w D (-x) = w D x

pp: case h2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, φ (-x) = φ x

Tactic:
·

Goal state after:
case h1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, w D (-x) = w D x
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case h2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, φ (-x) = φ x

Tactic:
·

Goal state after:
case h2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ ∀ᵐ (x : E) ∂μ, φ (-x) = φ x
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case pos
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ (∫ (x : G), { toFun := f, continuous_toFun := f_cont } (φ x) ∂μ') /
      ∫ (x : G), { toFun := f, continuous_toFun := f_cont } (φ x) ∂μ =
    (∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ') / ∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ

pp: case pos.h'f
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ HasCompactSupport (f ∘ ⇑φ.toHomeomorph)

pp: case pos.int_nonzero
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ ∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ ≠ 0

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ (∫ (x : G), { toFun := f, continuous_toFun := f_cont } (φ x) ∂μ') /
      ∫ (x : G), { toFun := f, continuous_toFun := f_cont } (φ x) ∂μ =
    (∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ') / ∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case pos.h'f
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ HasCompactSupport (f ∘ ⇑φ.toHomeomorph)

pp: case pos.int_nonzero
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ ∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ ≠ 0

Tactic:
·

Goal state after:
case pos.h'f
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ HasCompactSupport (f ∘ ⇑φ.toHomeomorph)
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case pos.int_nonzero
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ ∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ ≠ 0

Tactic:
·

Goal state after:
case pos.int_nonzero
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ ∫ (x : G), (f ∘ ⇑φ.toHomeomorph) x ∂μ ≠ 0