awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, ∀ (hi : y < p.lastStep), p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ (j : { j : Ordinal.{u} // j < i }),
    ⋃ (_ :
      (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),
      {p.color (↑j : Ordinal.{u})}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : (k : ℕ) → 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))
Gab :
  ∀ (a b : Fin N.succ),
    G (↑a : ℕ) < G (↑b : ℕ) →
      p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ)))) ∧
        p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
a : Fin (N + 1)
ha : a < last N
I : (↑a : ℕ) < N
⊢ G N = i

Tactic:
simp only [G, if_true]

Premises used: if_true
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, ∀ (hi : y < p.lastStep), p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ (j : { j : Ordinal.{u} // j < i }),
    ⋃ (_ :
      (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),
      {p.color (↑j : Ordinal.{u})}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : (k : ℕ) → 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))
Gab :
  ∀ (a b : Fin N.succ),
    G (↑a : ℕ) < G (↑b : ℕ) →
      p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ)))) ∧
        p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
a : Fin (N + 1)
ha : a < last N
I : (↑a : ℕ) < N
⊢ G (↑(last N) : ℕ) = i

Tactic:
have J : G (Fin.last N) = i := by dsimp; simp only [G, if_true]
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, ∀ (hi : y < p.lastStep), p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ (j : { j : Ordinal.{u} // j < i }),
    ⋃ (_ :
      (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),
      {p.color (↑j : Ordinal.{u})}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : (k : ℕ) → 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))
Gab :
  ∀ (a b : Fin N.succ),
    G (↑a : ℕ) < G (↑b : ℕ) →
      p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ)))) ∧
        p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
a : Fin (N + 1)
ha : a < last N
I : (↑a : ℕ) < N
J : G (↑(last N) : ℕ) = i
⊢ G (↑a : ℕ) = g (↑a : ℕ)

Tactic:
simp [G, I.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, ∀ (hi : y < p.lastStep), p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ (j : { j : Ordinal.{u} // j < i }),
    ⋃ (_ :
      (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),
      {p.color (↑j : Ordinal.{u})}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : (k : ℕ) → 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))
Gab :
  ∀ (a b : Fin N.succ),
    G (↑a : ℕ) < G (↑b : ℕ) →
      p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ)))) ∧
        p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
a : Fin (N + 1)
ha : a < last N
I : (↑a : ℕ) < N
J : G (↑(last N) : ℕ) = i
⊢ G (↑a : ℕ) = g (↑a : ℕ)

Tactic:
have K : G a = g a := by simp [G, I.ne]
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, ∀ (hi : y < p.lastStep), p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ (j : { j : Ordinal.{u} // j < i }),
    ⋃ (_ :
      (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),
      {p.color (↑j : Ordinal.{u})}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : (k : ℕ) → 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))
Gab :
  ∀ (a b : Fin N.succ),
    G (↑a : ℕ) < G (↑b : ℕ) →
      p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ)))) ∧
        p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
a : Fin (N + 1)
ha : a < last N
I : (↑a : ℕ) < N
J : G (↑(last N) : ℕ) = i
K : G (↑a : ℕ) = g (↑a : ℕ)
⊢ dist (p.c (p.index (g (↑a : ℕ)))) (p.c (p.index i)) ≤ p.r (p.index (g (↑a : ℕ))) + p.r (p.index i)

Tactic:
dist_le_add_of_nonempty_closedBall_inter_closedBall (hg _ I).2.1

Premises used: And.right, And.left, Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, ∀ (hi : y < p.lastStep), p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ (j : { j : Ordinal.{u} // j < i }),
    ⋃ (_ :
      (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),
      {p.color (↑j : Ordinal.{u})}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : (k : ℕ) → 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))
Gab :
  ∀ (a b : Fin N.succ),
    G (↑a : ℕ) < G (↑b : ℕ) →
      p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ)))) ∧
        p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
a : Fin (N + 1)
ha : a < last N
I : (↑a : ℕ) < N
J : G (↑(last N) : ℕ) = i
K : G (↑a : ℕ) = g (↑a : ℕ)
⊢ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑(last N) : ℕ)))) ≤
    p.r (p.index (G (↑a : ℕ))) + p.r (p.index (G (↑(last N) : ℕ)))

Tactic:
convert! dist_le_add_of_nonempty_closedBall_inter_closedBall (hg _ I).2.1

Premises used: And.right, And.left, Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, ∀ (hi : y < p.lastStep), p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ (j : { j : Ordinal.{u} // j < i }),
    ⋃ (_ :
      (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),
      {p.color (↑j : Ordinal.{u})}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : (k : ℕ) → 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))
Gab :
  ∀ (a b : Fin N.succ),
    G (↑a : ℕ) < G (↑b : ℕ) →
      p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ)))) ∧
        p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
sc : SatelliteConfig α N p.τ :=
  { c := fun (k : Fin N.succ) ↦ p.c (p.index (G (↑k : ℕ))), r := fun (k : Fin N.succ) ↦ p.r (p.index (G (↑k : ℕ))),
    rpos := ⋯, h := ⋯, hlast := ⋯, inter := ⋯ }
⊢ False

Tactic:
hN.false sc

Premises used: IsEmpty.false
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, ∀ (hi : y < p.lastStep), p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ (j : { j : Ordinal.{u} // j < i }),
    ⋃ (_ :
      (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),
      {p.color (↑j : Ordinal.{u})}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : (k : ℕ) → 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))
Gab :
  ∀ (a b : Fin N.succ),
    G (↑a : ℕ) < G (↑b : ℕ) →
      p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ)))) ∧
        p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
sc : SatelliteConfig α N p.τ :=
  { c := fun (k : Fin N.succ) ↦ p.c (p.index (G (↑k : ℕ))), r := fun (k : Fin N.succ) ↦ p.r (p.index (G (↑k : ℕ))),
    rpos := ⋯, h := ⋯, hlast := ⋯, inter := ⋯ }
⊢ False

Tactic:
exact hN.false sc

Premises used: IsEmpty.false
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
inl :
  IsEmpty β →
    ∃ (s : Fin N → Set β),
      (∀ (i : Fin N), PairwiseDisjoint.{u_1, u} (α := Set α) (s i) fun (j : β) ↦ closedBall (q.c j) (q.r j)) ∧
        range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, ball (q.c j) (q.r j)
inr :
  Nonempty β →
    ∃ (s : Fin N → Set β),
      (∀ (i : Fin N), PairwiseDisjoint.{u_1, u} (α := Set α) (s i) fun (j : β) ↦ closedBall (q.c j) (q.r j)) ∧
        range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, ball (q.c j) (q.r j)
⊢ ∃ (s : Fin N → Set β),
    (∀ (i : Fin N), PairwiseDisjoint.{u_1, u} (α := Set α) (s i) fun (j : β) ↦ closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
cases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : IsEmpty β
⊢ ∃ (s : Fin N → Set β),
    (∀ (i : Fin N), PairwiseDisjoint.{u_1, u} (α := Set α) (s i) fun (j : β) ↦ closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
⟨fun _ => ∅, fun _ => pairwiseDisjoint_empty, ?_⟩

Premises used: Set.pairwiseDisjoint_empty, And.intro, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : IsEmpty β
inl :
  range q.c ⊆
    ⋃ (i : Fin N),
      ⋃ (j : β), ⋃ (_ : Membership.mem (γ := Set β) ((fun (x : Fin N) ↦ (∅ : Set β)) i) j), ball (q.c j) (q.r j)
⊢ ∃ (s : Fin N → Set β),
    (∀ (i : Fin N), PairwiseDisjoint.{u_1, u} (α := Set α) (s i) fun (j : β) ↦ closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
refine ⟨fun _ => ∅, fun _ => pairwiseDisjoint_empty, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : IsEmpty β
inl :
  q.c '' ∅ ⊆
    ⋃ (i : Fin N),
      ⋃ (j : β), ⋃ (_ : Membership.mem (γ := Set β) ((fun (x : Fin N) ↦ (∅ : Set β)) i) j), ball (q.c j) (q.r j)
⊢ range q.c ⊆
    ⋃ (i : Fin N),
      ⋃ (j : β), ⋃ (_ : Membership.mem (γ := Set β) ((fun (x : Fin N) ↦ (∅ : Set β)) i) j), ball (q.c j) (q.r j)

Tactic:
rw [← image_univ, eq_empty_of_isEmpty (univ : Set β)]

Premises used: Set.image_univ, Set.univ, Set.eq_empty_of_isEmpty
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : IsEmpty β
⊢ q.c '' ∅ ⊆
    ⋃ (i : Fin N),
      ⋃ (j : β), ⋃ (_ : Membership.mem (γ := Set β) ((fun (x : Fin N) ↦ (∅ : Set β)) i) j), ball (q.c j) (q.r j)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : (i : Fin N) → Set β :=
  fun (i : Fin N) ↦ ⋃ (k : Ordinal.{u}), ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = (↑i : ℕ)), {p.index k}
⊢ ∃ (s : Fin N → Set β),
    (∀ (i : Fin N), PairwiseDisjoint.{u_1, u} (α := Set α) (s i) fun (j : β) ↦ closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
⟨s, fun i => ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : (i : Fin N) → Set β :=
  fun (i : Fin N) ↦ ⋃ (k : Ordinal.{u}), ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = (↑i : ℕ)), {p.index k}
inr : ∀ (i : Fin N), PairwiseDisjoint.{u_1, u} (α := Set α) (s i) fun (j : β) ↦ closedBall (q.c j) (q.r j)
inr₁ : range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, ball (q.c j) (q.r j)
⊢ ∃ (s : Fin N → Set β),
    (∀ (i : Fin N), PairwiseDisjoint.{u_1, u} (α := Set α) (s i) fun (j : β) ↦ closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
refine ⟨s, fun i => ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : (i : Fin N) → Set β :=
  fun (i : Fin N) ↦ ⋃ (k : Ordinal.{u}), ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = (↑i : ℕ)), {p.index k}
i : Fin N
x : β
hx : x ∈ s i
y : β
hy : y ∈ s i
x_ne_y : x ≠ y
⊢ ∃ jx < p.lastStep, p.color jx = (↑i : ℕ) ∧ x = p.index jx

Tactic:
simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hx

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : (i : Fin N) → Set β :=
  fun (i : Fin N) ↦ ⋃ (k : Ordinal.{u}), ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = (↑i : ℕ)), {p.index k}
i : Fin N
x : β
hx : x ∈ s i
y : β
hy : y ∈ s i
x_ne_y : x ≠ y
inr :
  ∀ (jx : Ordinal.{u}) (jx_lt : jx < p.lastStep) (jxi : p.color jx = (↑i : ℕ)) (hx : p.index jx ∈ s i)
    (x_ne_y : p.index jx ≠ y),
    Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx) y
⊢ Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) x y

Tactic:
obtain ⟨jx, jx_lt, jxi, rfl⟩ :
      ∃ jx : Ordinal, jx < p.lastStep ∧ p.color jx = i ∧ x = p.index jx := by
      simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hx

Premises used: Besicovitch.TauPackage.lastStep, rfl, Ordinal
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : (i : Fin N) → Set β :=
  fun (i : Fin N) ↦ ⋃ (k : Ordinal.{u}), ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = (↑i : ℕ)), {p.index k}
i : Fin N
y : β
hy : y ∈ s i
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = (↑i : ℕ)
hx : p.index jx ∈ s i
x_ne_y : p.index jx ≠ y
⊢ ∃ jy < p.lastStep, p.color jy = (↑i : ℕ) ∧ y = p.index jy

Tactic:
simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hy

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : (i : Fin N) → Set β :=
  fun (i : Fin N) ↦ ⋃ (k : Ordinal.{u}), ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = (↑i : ℕ)), {p.index k}
i : Fin N
y : β
hy : y ∈ s i
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = (↑i : ℕ)
hx : p.index jx ∈ s i
x_ne_y : p.index jx ≠ y
inr :
  ∀ (jy : Ordinal.{u}) (jy_lt : jy < p.lastStep) (jyi : p.color jy = (↑i : ℕ)) (hy : p.index jy ∈ s i)
    (x_ne_y : p.index jx ≠ p.index jy),
    Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx)
      (p.index jy)
⊢ Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx) y

Tactic:
obtain ⟨jy, jy_lt, jyi, rfl⟩ :
      ∃ jy : Ordinal, jy < p.lastStep ∧ p.color jy = i ∧ y = p.index jy := by
      simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hy

Premises used: Besicovitch.TauPackage.lastStep, rfl, Ordinal
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : (i : Fin N) → Set β :=
  fun (i : Fin N) ↦ ⋃ (k : Ordinal.{u}), ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = (↑i : ℕ)), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = (↑i : ℕ)
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = (↑i : ℕ)
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
inr :
  ∀
    (this :
      ∀ (jx : Ordinal.{u}) (jx_lt : jx < p.lastStep) (jxi : p.color jx = (↑i : ℕ)) (hx : p.index jx ∈ s i)
        (jy : Ordinal.{u}) (jy_lt : jy < p.lastStep) (jyi : p.color jy = (↑i : ℕ)) (hy : p.index jy ∈ s i)
        (x_ne_y : p.index jx ≠ p.index jy) (jxy : jx ≤ jy),
        Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx)
          (p.index jy))
    (jxy : ¬jx ≤ jy),
    Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx)
      (p.index jy)
wlog :
  ∀ (jx : Ordinal.{u}) (jx_lt : jx < p.lastStep) (jxi : p.color jx = (↑i : ℕ)) (hx : p.index jx ∈ s i)
    (jy : Ordinal.{u}) (jy_lt : jy < p.lastStep) (jyi : p.color jy = (↑i : ℕ)) (hy : p.index jy ∈ s i)
    (x_ne_y : p.index jx ≠ p.index jy) (jxy : jx ≤ jy),
    Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx)
      (p.index jy)
⊢ Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx)
    (p.index jy)

Tactic:
wlog jxy : jx ≤ jy generalizing jx jy
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
q : BallPackage β α
h : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : (i : Fin N) → Set β :=
  fun (i : Fin N) ↦ ⋃ (k : Ordinal.{u}), ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = (↑i : ℕ)), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = (↑i : ℕ)
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = (↑i : ℕ)
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
this :
  ∀ (jx : Ordinal.{u}) (jx_lt : jx < p.lastStep) (jxi : p.color jx = (↑i : ℕ)) (hx : p.index jx ∈ s i)
    (jy : Ordinal.{u}) (jy_lt : jy < p.lastStep) (jyi : p.color jy = (↑i : ℕ)) (hy : p.index jy ∈ s i)
    (x_ne_y : p.index jx ≠ p.index jy) (jxy : jx ≤ jy),
    Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx)
      (p.index jy)
jxy : ¬jx ≤ jy
⊢ Function.onFun.{u + 1, u_1 + 1, 1} (β := Set α) Disjoint (fun (j : β) ↦ closedBall (q.c j) (q.r j)) (p.index jx)
    (p.index jy)

Tactic:
(this jy jy_lt jyi hy jx jx_lt jxi hx x_ne_y.symm (le_of_not_ge jxy)).symm

Premises used: le_of_not_ge, Ne.symm, Disjoint.symm