awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x y : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (uIcc x y) = edist y x

Tactic:
simp only [uIcc, volume_apply, image_subtype_val_Icc, Icc.coe_inf, Icc.coe_sup, Real.volume_Icc,
    max_sub_min_eq_abs, edist_dist, Subtype.dist_eq, Real.dist_eq]

Premises used: unitInterval.volume_apply, Subtype.dist_eq, Real.volume_Icc, max_sub_min_eq_abs, edist_dist, Real.dist_eq, Set.Icc.coe_inf, Set.Icc.coe_sup, Set.uIcc, Set.image_subtype_val_Icc
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x y : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (Ico x y) = ENNReal.ofReal ((↑y : ℝ) - (↑x : ℝ))

Tactic:
simp only [volume_apply, image_subtype_val_Ico, Real.volume_Ico]

Premises used: unitInterval.volume_apply, Real.volume_Ico, Set.image_subtype_val_Ico
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x y : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (Ioc x y) = ENNReal.ofReal ((↑y : ℝ) - (↑x : ℝ))

Tactic:
simp only [volume_apply, image_subtype_val_Ioc, Real.volume_Ioc]

Premises used: unitInterval.volume_apply, Real.volume_Ioc, Set.image_subtype_val_Ioc
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x y : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (uIoc x y) = edist y x

Tactic:
simp only [uIoc, volume_apply, image_subtype_val_Ioc, Icc.coe_inf, Icc.coe_sup, Real.volume_Ioc,
    max_sub_min_eq_abs, edist_dist, Subtype.dist_eq, Real.dist_eq]

Premises used: unitInterval.volume_apply, Set.uIoc, Subtype.dist_eq, max_sub_min_eq_abs, Real.volume_Ioc, edist_dist, Real.dist_eq, Set.Icc.coe_inf, Set.image_subtype_val_Ioc, Set.Icc.coe_sup
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x y : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (Ioo x y) = ENNReal.ofReal ((↑y : ℝ) - (↑x : ℝ))

Tactic:
simp only [volume_apply, image_subtype_val_Ioo, Real.volume_Ioo]

Premises used: unitInterval.volume_apply, Set.image_subtype_val_Ioo, Real.volume_Ioo
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x y : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (uIoo x y) = edist y x

Tactic:
simp only [uIoo, volume_apply, image_subtype_val_Ioo, Icc.coe_inf, Icc.coe_sup, Real.volume_Ioo,
    max_sub_min_eq_abs, edist_dist, Subtype.dist_eq, Real.dist_eq]

Premises used: unitInterval.volume_apply, Subtype.dist_eq, max_sub_min_eq_abs, Set.uIoo, edist_dist, Set.image_subtype_val_Ioo, Real.dist_eq, Set.Icc.coe_inf, Real.volume_Ioo, Set.Icc.coe_sup
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
τ : ℝ
inst : Inhabited α
inst_1 : MetricSpace α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
hi : i < last 0
⊢ LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (last 0) (last 0)

Tactic:
rw [Subsingleton.elim (α := Fin 1) i (last 0)] at hi

Premises used: Fin.last, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
τ : ℝ
inst : Inhabited α
inst_1 : MetricSpace α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
hi : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (last 0) (last 0)
⊢ 1 ≤ dist.{u_1} (α := α) (default i) (default (last 0)) ∧ 1 ≤ τ * 1

Tactic:
(lt_irrefl _ hi).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
τ : ℝ
inst : Inhabited α
inst_1 : MetricSpace α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
hi : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (last 0) (last 0)
⊢ 1 ≤ dist.{u_1} (α := α) (default i) (default (last 0)) ∧ 1 ≤ τ * 1

Tactic:
exact (lt_irrefl _ hi).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
τ : ℝ
inst : Inhabited α
inst_1 : MetricSpace α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
hi : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (last 0) (last 0)
⊢ dist.{u_1} (α := α) (default i) (default (last 0)) ≤ HAdd.hAdd (α := ℝ) 1 1

Tactic:
(lt_irrefl _ hi).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
τ : ℝ
inst : Inhabited α
inst_1 : MetricSpace α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
hi : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (last 0) (last 0)
⊢ dist.{u_1} (α := α) (default i) (default (last 0)) ≤ HAdd.hAdd (α := ℝ) 1 1

Tactic:
exact (lt_irrefl _ hi).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
inl : ∀ (H : i < last N), dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
inr : ∀ (H : last N ≤ i), dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
rcases lt_or_ge i (last N) with (H | H)

Premises used: Fin.last, lt_or_ge
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : i < last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
a.inter i H

Premises used: Besicovitch.SatelliteConfig.inter
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : i < last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
exact a.inter i H

Premises used: Besicovitch.SatelliteConfig.inter
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
⊢ i = last N

Tactic:
have I : i = last N := top_le_iff.1 H
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
I : i = last N
⊢ 0 ≤ a.r (last N)

Tactic:
have := (a.rpos (last N)).le
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
I : i = last N
this : 0 ≤ a.r (last N)
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
simp only [I, add_nonneg this this, dist_self]

Premises used: add_nonneg, dist_self
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
inl : ∀ (H : i < last N), a.r (last N) ≤ τ * a.r i
inr : ∀ (H : last N ≤ i), a.r (last N) ≤ τ * a.r i
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
rcases lt_or_ge i (last N) with (H | H)

Premises used: Fin.last, lt_or_ge
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : i < last N
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
(a.hlast i H).2

Premises used: Besicovitch.SatelliteConfig.hlast, And.right
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : i < last N
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
exact (a.hlast i H).2

Premises used: Besicovitch.SatelliteConfig.hlast, And.right
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
⊢ i = last N

Tactic:
have : i = last N := top_le_iff.1 H
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
inr : a.r (last N) ≤ τ * a.r (last N)
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ τ * a.r (last N)

Tactic:
le_mul_of_one_le_left (a.rpos _).le h

Premises used: le_mul_of_one_le_left, Besicovitch.SatelliteConfig.rpos, LT.lt.le
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ τ * a.r (last N)

Tactic:
exact le_mul_of_one_le_left (a.rpos _).le h

Premises used: le_mul_of_one_le_left, Besicovitch.SatelliteConfig.rpos, LT.lt.le
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
a : Ordinal.{u}
i : Ordinal.{u} := a
j : { j : Ordinal.{u} // j < i }
⊢ (↑j : Ordinal.{u}) < a

Tactic:
j.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
a : Ordinal.{u}
i : Ordinal.{u} := a
j : { j : Ordinal.{u} // j < i }
⊢ (↑j : Ordinal.{u}) < a

Tactic:
exact j.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
a : Ordinal.{u}
i : Ordinal.{u} := a
j : { j : Ordinal.{u} // j < i }
⊢ (↑j : Ordinal.{u}) < a

Tactic:
decreasing_by exact j.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
i j : Ordinal.{u}
hij : i ≤ j
⊢ LE.le.{u_1} (α := Set α)
    (⋃ (j : { j : Ordinal.{u} // j < i }), ball (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))))
    (⋃ (j_1 : { j_1 : Ordinal.{u} // j_1 < j }),
      ball (p.c (p.index (↑j_1 : Ordinal.{u}))) (p.r (p.index (↑j_1 : Ordinal.{u}))))

Tactic:
iUnion_mono' fun r => ⟨⟨r, r.2.trans_le hij⟩, Subset.rfl⟩

Premises used: Set.iUnion_mono', Subtype.mk, Set.Subset.rfl, LT.lt.trans_le, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
i j : Ordinal.{u}
hij : i ≤ j
⊢ LE.le.{u_1} (α := Set α)
    (⋃ (j : { j : Ordinal.{u} // j < i }), ball (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))))
    (⋃ (j_1 : { j_1 : Ordinal.{u} // j_1 < j }),
      ball (p.c (p.index (↑j_1 : Ordinal.{u}))) (p.r (p.index (↑j_1 : Ordinal.{u}))))

Tactic:
exact iUnion_mono' fun r => ⟨⟨r, r.2.trans_le hij⟩, Subset.rfl⟩

Premises used: Set.iUnion_mono', Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
a : Ordinal.{u}
i : Ordinal.{u} := a
j : { j : Ordinal.{u} // j < i }
h :
  (closedBall (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) ∩
      closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty
⊢ (↑j : Ordinal.{u}) < a

Tactic:
j.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
a : Ordinal.{u}
i : Ordinal.{u} := a
j : { j : Ordinal.{u} // j < i }
h :
  (closedBall (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) ∩
      closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty
⊢ (↑j : Ordinal.{u}) < a

Tactic:
exact j.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
a : Ordinal.{u}
i : Ordinal.{u} := a
j : { j : Ordinal.{u} // j < i }
h :
  (closedBall (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) ∩
      closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty
⊢ (↑j : Ordinal.{u}) < a

Tactic:
decreasing_by exact j.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
by_contra :
  ∀
    (h :
      ¬Set.Nonempty.{u + 1} (α := Ordinal.{u})
          {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}),
    False
⊢ Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}

Tactic:
by_contra h
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
suffices : Function.Injective p.index
⊢ False

Tactic:
suffices H : Function.Injective p.index from not_injective_of_ordinal p.index H
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
inr : ∀ (this : ∀ ⦃x y : Ordinal.{u}⦄ (hxy : p.index x = p.index y) (x_le_y : x ≤ y), x = y) (x_le_y : ¬x ≤ y), x = y
wlog : ∀ ⦃x y : Ordinal.{u}⦄ (hxy : p.index x = p.index y) (x_le_y : x ≤ y), x = y
⊢ x = y

Tactic:
wlog x_le_y : x ≤ y generalizing x y
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
this : ∀ ⦃x y : Ordinal.{u}⦄ (hxy : p.index x = p.index y) (x_le_y : x ≤ y), x = y
x_le_y : ¬x ≤ y
⊢ x = y

Tactic:
(this hxy.symm (le_of_not_ge x_le_y)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
this : ∀ ⦃x y : Ordinal.{u}⦄ (hxy : p.index x = p.index y) (x_le_y : x ≤ y), x = y
x_le_y : ¬x ≤ y
⊢ x = y

Tactic:
exact (this hxy.symm (le_of_not_ge x_le_y)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
inl : ∀ (hxy : p.index x = p.index x) (x_le_y : x ≤ x), x = x
inr : ∀ (H : x < y), x = y
⊢ x = y

Tactic:
rcases eq_or_lt_of_le x_le_y with (rfl | H)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x : Ordinal.{u}
hxy : p.index x = p.index x
x_le_y : x ≤ x
⊢ x = x

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
⊢ ∀ (x : Ordinal.{u}), ∃ (x_1 : β), p.c x_1 ∉ p.iUnionUpTo x ∧ p.R x ≤ p.τ * p.r x_1

Tactic:
simp only [nonempty_def, not_exists, exists_prop, not_and, not_lt, not_le, mem_setOf_eq,
    not_forall] at h

Premises used: not_le, not_exists, Set.mem_setOf_eq, Set.nonempty_def, exists_prop, not_lt, not_and, Classical.not_forall
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∀ (x : Ordinal.{u}), ∃ (x_1 : β), p.c x_1 ∉ p.iUnionUpTo x ∧ p.R x ≤ p.τ * p.r x_1
⊢ ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x

Tactic:
specialize h y
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
rw :
  Eq.{u + 1} (α := β)
    (Classical.epsilon fun (b : β) ↦
      p.c b ∉
          ⋃ (j : { j : Ordinal.{u} // j < y }),
            ball (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) ∧
        ⨆ (b :
            { b : β //
              p.c b ∉
                ⋃ (j : { j : Ordinal.{u} // j < y }),
                  ball (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) }),
            p.r (↑b : β) ≤
          p.τ * p.r b)
    (Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b)
⊢ p.index y = Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b

Tactic:
rw [TauPackage.index]

Premises used: Besicovitch.TauPackage.index
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ Eq.{u + 1} (α := β)
    (Classical.epsilon fun (b : β) ↦
      p.c b ∉
          ⋃ (j : { j : Ordinal.{u} // j < y }),
            ball (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) ∧
        ⨆ (b :
            { b : β //
              p.c b ∉
                ⋃ (j : { j : Ordinal.{u} // j < y }),
                  ball (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) }),
            p.r (↑b : β) ≤
          p.τ * p.r b)
    (Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ p.index y = Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b

Tactic:
have :
        p.index y =
          Classical.epsilon fun b : β => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b := by
      rw [TauPackage.index]; rfl
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
rw : p.c (Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b) ∉ p.iUnionUpTo y
⊢ p.c (p.index y) ∉ p.iUnionUpTo y

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
⊢ p.c (Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b) ∉ p.iUnionUpTo y

Tactic:
(Classical.epsilon_spec h).1

Premises used: Set.Mem, And.left, Classical.epsilon_spec
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
⊢ p.c (Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b) ∉ p.iUnionUpTo y

Tactic:
exact (Classical.epsilon_spec h).1

Premises used: And.left, Classical.epsilon_spec
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ p.c (p.index y) ∉ p.iUnionUpTo y

Tactic:
have A : p.c (p.index y) ∉ p.iUnionUpTo y := by
    have :
        p.index y =
          Classical.epsilon fun b : β => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b := by
      rw [TauPackage.index]; rfl
    rw [this]
    exact (Classical.epsilon_spec h).1
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.c (p.index y) ∉ p.iUnionUpTo y
⊢ ∀ x < y, p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))

Tactic:
simp only [iUnionUpTo, not_exists, exists_prop, mem_iUnion, not_and,
    Subtype.exists] at A

Premises used: Besicovitch.TauPackage.iUnionUpTo, Set.mem_iUnion, Subtype.exists, not_exists, exists_prop, not_and
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : ∀ x < y, p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
⊢ p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))

Tactic:
specialize A x H
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
⊢ p.r (p.index y) ≤ 0

Tactic:
simpa [hxy] using A
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
⊢ p.r (p.index y) ≤ 0

Tactic:
replace A : p.r (p.index y) ≤ 0 := by simpa [hxy] using A
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.r (p.index y) ≤ 0
⊢ x = y

Tactic:
(lt_irrefl _ ((p.rpos (p.index y)).trans_le A)).elim

Premises used: lt_irrefl, Besicovitch.TauPackage.index, False.elim, Besicovitch.TauPackage.toBallPackage, LT.lt.trans_le, Besicovitch.BallPackage.rpos
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.r (p.index y) ≤ 0
⊢ x = y

Tactic:
exact (lt_irrefl _ ((p.rpos (p.index y)).trans_le A)).elim

Premises used: lt_irrefl, Besicovitch.TauPackage.index, False.elim, Besicovitch.TauPackage.toBallPackage, LT.lt.trans_le, Besicovitch.BallPackage.rpos
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x : β
⊢ Membership.mem (γ := Set Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
    p.lastStep

Tactic:
have : p.lastStep ∈ {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b} :=
      csInf_mem p.lastStep_nonempty
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x : β
this :
  Membership.mem (γ := Set Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
    p.lastStep
⊢ ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep

Tactic:
simpa only [not_exists, mem_setOf_eq, not_and_or, not_le, not_notMem]

Premises used: not_le, not_exists, Set.mem_setOf_eq, Set.not_notMem, not_and_or