awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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
⊢ False
have color_G : ∀ n ≤ N, p.color (G n) = n
Tactic: have color_G : ∀ n, n ≤ N → p.color (G n) = n := by
    intro n hn
    rcases hn.eq_or_lt with (rfl | H)
    · simp only [G]; simp only [color_i, Inf_eq_N, if_true]
    · simp only [G]; simp only [H.ne, (hg n H).right.right.symm, if_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
n : ℕ
hn : n ≤ N
⊢ G n < p.lastStep
have inl : ∀ (hN : IsEmpty.{u_1 + 1} (SatelliteConfig α n p.τ)) (IH : ∀ y < i, ∀ (hi : 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)),
  let 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
Tactic: rcases hn.eq_or_lt with (rfl | H)
Cleared hypotheses: N, hN, IH, N_mem, Inf_eq_N, hg, G, color_G, hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
n : ℕ
hn : n ≤ N
inl :
  ∀ (hN : IsEmpty.{u_1 + 1} (SatelliteConfig α n p.τ)) (IH : ∀ y < i, ∀ (hi : 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)),
    let 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
⊢ G n < p.lastStep
have inr : ∀ (H : n < N), G n < p.lastStep
Tactic: rcases hn.eq_or_lt with (rfl | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
i : Ordinal.{u}
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)
g : (k : ℕ) → Ordinal.{u}
n : ℕ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α n p.τ)
IH : ∀ y < i, ∀ (hi : 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
have inl : (if True then i else g n) < p.lastStep
Tactic: simp only [G]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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
⊢ False
have G_lt_last : ∀ n ≤ N, G n < p.lastStep
Tactic: have G_lt_last : ∀ n, n ≤ N → G n < p.lastStep := by
    intro n hn
    rcases hn.eq_or_lt with (rfl | H)
    · simp only [G]; simp only [hi, if_true]
    · simp only [G]; simp only [H.ne, (hg n H).left.trans hi, if_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
n : ℕ
hn : n ≤ N
⊢ p.index (G n) = Classical.epsilon fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t
have rw : Eq.{u + 1} (α := β)
  (Classical.epsilon fun (b : β) ↦
    p.c b ∉
        ⋃ (j : { j : Ordinal.{u} // j < G n }),
          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 < G n }),
                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 (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t)
Tactic: rw [index]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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
n : ℕ
hn : n ≤ N
⊢ p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
have this : p.index (G n) = Classical.epsilon fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t
Tactic: have :
      p.index (G n) =
        Classical.epsilon fun t => p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t := by
      rw [index]; rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
n : ℕ
hn : n ≤ N
this : p.index (G n) = Classical.epsilon fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t
⊢ p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
have rw : p.c (Classical.epsilon fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t) ∉ p.iUnionUpTo (G n) ∧
  p.R (G n) ≤ p.τ * p.r (Classical.epsilon fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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
n : ℕ
hn : n ≤ N
this : p.index (G n) = Classical.epsilon fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t
⊢ p.c (Classical.epsilon fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t) ∉ p.iUnionUpTo (G n) ∧
    p.R (G n) ≤ p.τ * p.r (Classical.epsilon fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t)
have this₁ : ∃ (t : β), p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t
Tactic: have : ∃ t, p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t := by
      simpa only [not_exists, exists_prop, not_and, not_lt, not_le, mem_setOf_eq, not_forall] using
        notMem_of_lt_csInf (G_lt_last n hn) (OrderBot.bddBelow _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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
⊢ False
have fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Tactic: have fGn :
      ∀ n, n ≤ N →
        p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n)) := by
    intro n hn
    have :
      p.index (G n) =
        Classical.epsilon fun t => p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t := by
      rw [index]; rfl
    rw [this]
    have : ∃ t, p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t := by
      simpa only [not_exists, exists_prop, not_and, not_lt, not_le, mem_setOf_eq, not_forall] using
        notMem_of_lt_csInf (G_lt_last n hn) (OrderBot.bddBelow _)
    exact Classical.epsilon_spec this
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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))
a b : Fin N.succ
G_lt : 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 : ℕ)))
have ha : (↑a : ℕ) ≤ N
Tactic: have ha : (a : ℕ) ≤ N := Nat.lt_succ_iff.1 a.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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))
a b : Fin N.succ
G_lt : G (↑a : ℕ) < G (↑b : ℕ)
ha : (↑a : ℕ) ≤ N
⊢ 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 : ℕ)))
have hb : (↑b : ℕ) ≤ N
Tactic: have hb : (b : ℕ) ≤ N := Nat.lt_succ_iff.1 b.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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))
a b : Fin N.succ
G_lt : G (↑a : ℕ) < G (↑b : ℕ)
ha : (↑a : ℕ) ≤ N
hb : (↑b : ℕ) ≤ N
⊢ 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 : ℕ)))
have left : p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ))))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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))
a b : Fin N.succ
G_lt : G (↑a : ℕ) < G (↑b : ℕ)
ha : (↑a : ℕ) ≤ N
hb : (↑b : ℕ) ≤ N
left : p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (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 : ℕ)))
have right : p.r (p.index (G (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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))
a b : Fin N.succ
G_lt : G (↑a : ℕ) < G (↑b : ℕ)
ha : (↑a : ℕ) ≤ N
hb : (↑b : ℕ) ≤ N
⊢ p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ))))
have this : p.c (p.index (G (↑b : ℕ))) ∉ p.iUnionUpTo (G (↑b : ℕ))
Tactic: have := (fGn b hb).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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))
a b : Fin N.succ
G_lt : G (↑a : ℕ) < G (↑b : ℕ)
ha : (↑a : ℕ) ≤ N
hb : (↑b : ℕ) ≤ N
this : p.c (p.index (G (↑b : ℕ))) ∉ p.iUnionUpTo (G (↑b : ℕ))
⊢ p.r (p.index (G (↑a : ℕ))) ≤ dist (p.c (p.index (G (↑a : ℕ)))) (p.c (p.index (G (↑b : ℕ))))
have this₁ : ∀ x < G (↑b : ℕ), p.c (p.index (G (↑b : ℕ))) ∉ 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 this
Cleared hypotheses: this