mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
⊢ ∃ c, ∀ (f : G → ℝ), Continuous[inst✝⁷, _] f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
⊢ ∃ c, ∀ (f : G → ℝ), Continuous[inst✝⁷, _] f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : LocallyCompactSpace G
⊢ ∃ c, ∀ (f : G → ℝ), Continuous[inst✝⁷, _] f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
⊢ ∃ c, ∀ (f : G → ℝ), Continuous[inst✝⁷, _] f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : 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
int_g_pos : 0 < ∫ (x : G), g x ∂μ
c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous[inst✝⁷, _] f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂NNReal.mk c c_nonneg • μ

Tactic:
rw [← mul_inv_eq_iff_eq_mul₀ int_g_pos.ne'] at A

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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : 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
int_g_pos : 0 < ∫ (x : G), g x ∂μ
c : ℝ := (∫ (x : G), g x ∂μ)⁻¹ * ∫ (x : G), g x ∂μ'
c_nonneg : 0 ≤ c
f : G → ℝ
f_cont : Continuous[inst✝⁷, _] f
f_comp : HasCompactSupport f
ν : Measure G := μ.inv
A : (∫ (x : G), f x ∂μ) * (∫ (x : G), g x ∂μ)⁻¹ = ∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂NNReal.mk c c_nonneg • μ
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
hG : LocallyCompactSpace G
⊢ μ.haarScalarFactor μ = 1

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
hG : ¬LocallyCompactSpace G
⊢ μ.haarScalarFactor μ = 1

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
hG : LocallyCompactSpace G
⊢ μ.haarScalarFactor μ = 1

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
hG : ¬LocallyCompactSpace G
⊢ μ.haarScalarFactor μ = 1
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
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

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
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : ¬LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

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
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν

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
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
hG : ¬LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
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
hn : n ≤ n
⊢ p.color (if True then i else g n) = n

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
hn : n ≤ n
⊢ p.color (if True then i else g n) = n
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
n : ℕ
hn : n ≤ N
H : n < N
⊢ p.color (if n = N then i else g n) = n

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
n : ℕ
hn : n ≤ N
H : n < N
⊢ p.color (if n = N then i else g n) = n
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 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 μ

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 μ

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
⊢ (map (⇑φ) μ').haarScalarFactor (map (⇑φ) μ) = μ'.haarScalarFactor μ

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_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (ball 0 1)

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 < μ (ball 0 1)
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ w D x = ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)

Tactic:
;

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
⊢ w D x = ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)
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
⊢ (if True then i else 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
⊢ (if True then i else g n) < p.lastStep
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
⊢ (if n = N then i else 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
⊢ (if n = N then i else g n) < p.lastStep
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ ∀ y ∈ ball x D, φ y = 1

Tactic:
;

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ ∀ y ∈ ball x D, φ y = 1
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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
G_lt_last : ∀ n ≤ N, G n < p.lastStep
n : ℕ
hn : n ≤ N
⊢ (Classical.epsilon fun b ↦ p.c b ∉ ⋃ j, ball (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∧ ⨆ b, p.r ↑b ≤ p.τ * p.r b) =
    Classical.epsilon fun t ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t

Tactic:
;

Goal state after:
α : 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
G_lt_last : ∀ n ≤ N, G n < p.lastStep
n : ℕ
hn : n ≤ N
⊢ (Classical.epsilon fun b ↦ p.c b ∉ ⋃ j, ball (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∧ ⨆ b, p.r ↑b ≤ p.τ * p.r b) =
    Classical.epsilon fun t ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
⊢ ∀ y ∈ ball x D, φ y = 0

Tactic:
;

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
⊢ ∀ y ∈ ball x D, φ y = 0
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
ha : ↑a ≤ N
hb : ↑b ≤ N
H : p.c (p.index (G ↑b)) ∈ p.iUnionUpTo (G ↑a)
⊢ False

Tactic:
;

Goal state after:
α : 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
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
ha : ↑a ≤ N
hb : ↑b ≤ N
H : p.c (p.index (G ↑b)) ∈ p.iUnionUpTo (G ↑a)
⊢ False
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_3.hf.h0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
x : ℝ × E
hx : x ∈ Ioo 0 1 ×ˢ univ
⊢ x.1 ≠ 0

Tactic:
;

Goal state after:
case refine_3.hf.h0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
x : ℝ × E
hx : x ∈ Ioo 0 1 ×ˢ univ
⊢ x.1 ≠ 0
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
R : ℝ
hR : 1 < R
⊢ 0 < (R - 1) / (R + 1)

Tactic:
;

Goal state after:
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
R : ℝ
hR : 1 < R
⊢ 0 < (R - 1) / (R + 1)