awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (↑b : ℕ))) ≤ p.τ * p.r (p.index (G (↑a : ℕ)))
have apply : p.r (p.index (G (↑b : ℕ))) ≤ p.R (G (↑a : ℕ))
Tactic: apply le_trans _ (fGn a ha).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
hb : (↑b : ℕ) ≤ N
⊢ p.r (p.index (G (↑b : ℕ))) ≤ p.R (G (↑a : ℕ))
have B : p.c (p.index (G (↑b : ℕ))) ∉ p.iUnionUpTo (G (↑a : ℕ))
Tactic: have B : p.c (p.index (G b)) ∉ p.iUnionUpTo (G a) := by
        intro H; exact (fGn b hb).1 (p.monotone_iUnionUpTo G_lt.le H)
-- 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
B : p.c (p.index (G (↑b : ℕ))) ∉ p.iUnionUpTo (G (↑a : ℕ))
b' : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) } :=
  Subtype.mk (p := fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G (↑a : ℕ))) (p.index (G (↑b : ℕ))) B
⊢ p.r (p.index (G (↑b : ℕ))) ≤ p.R (G (↑a : ℕ))
have apply : BddAbove (α := ℝ) (range fun (t : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) }) ↦ p.r (↑t : β))
Tactic: apply @le_ciSup _ _ _ (fun t : { t // p.c t ∉ p.iUnionUpTo (G a) } => p.r t) _ b'
-- 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
B : p.c (p.index (G (↑b : ℕ))) ∉ p.iUnionUpTo (G (↑a : ℕ))
b' : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) } :=
  Subtype.mk (p := fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G (↑a : ℕ))) (p.index (G (↑b : ℕ))) B
⊢ BddAbove (α := ℝ) (range fun (t : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) }) ↦ p.r (↑t : β))
have refine : ∀ (t : ℝ)
  (ht : Membership.mem (γ := Set ℝ) (range fun (t : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) }) ↦ p.r (↑t : β)) t),
  t ≤ p.r_bound
Tactic: refine ⟨p.r_bound, fun t ht => ?_⟩
-- 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
B : p.c (p.index (G (↑b : ℕ))) ∉ p.iUnionUpTo (G (↑a : ℕ))
b' : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) } :=
  Subtype.mk (p := fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G (↑a : ℕ))) (p.index (G (↑b : ℕ))) B
t : ℝ
ht : Membership.mem (γ := Set ℝ) (range fun (t : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) }) ↦ p.r (↑t : β)) t
⊢ t ≤ p.r_bound
have ht₁ : ∃ (a_1 : β), p.c a_1 ∉ p.iUnionUpTo (G (↑a : ℕ)) ∧ p.r a_1 = t
Tactic: simp only [exists_prop, mem_range, Subtype.exists] at ht
Cleared hypotheses: ht
-- 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
B : p.c (p.index (G (↑b : ℕ))) ∉ p.iUnionUpTo (G (↑a : ℕ))
b' : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) } :=
  Subtype.mk (p := fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G (↑a : ℕ))) (p.index (G (↑b : ℕ))) B
t : ℝ
ht : ∃ (a_1 : β), p.c a_1 ∉ p.iUnionUpTo (G (↑a : ℕ)) ∧ p.r a_1 = t
⊢ t ≤ p.r_bound
have rcases : ∀ (u : β) (hu : p.c u ∉ p.iUnionUpTo (G (↑a : ℕ)) ∧ p.r u = t), t ≤ p.r_bound
Tactic: rcases ht with ⟨u, hu⟩
Cleared hypotheses: ht
-- 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
B : p.c (p.index (G (↑b : ℕ))) ∉ p.iUnionUpTo (G (↑a : ℕ))
b' : { t : β // p.c t ∉ p.iUnionUpTo (G (↑a : ℕ)) } :=
  Subtype.mk (p := fun (t : β) ↦ p.c t ∉ p.iUnionUpTo (G (↑a : ℕ))) (p.index (G (↑b : ℕ))) B
t : ℝ
u : β
hu : p.c u ∉ p.iUnionUpTo (G (↑a : ℕ)) ∧ p.r u = t
⊢ t ≤ p.r_bound
have rw : p.r u ≤ p.r_bound
Tactic: rw [← hu.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))
⊢ False
have 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 : ℕ)))
Tactic: have Gab :
    ∀ a b : Fin (Nat.succ N),
      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)) := by
    intro a b G_lt
    have ha : (a : ℕ) ≤ N := Nat.lt_succ_iff.1 a.2
    have hb : (b : ℕ) ≤ N := Nat.lt_succ_iff.1 b.2
    constructor
    · have := (fGn b hb).1
      simp only [iUnionUpTo, not_exists, exists_prop, mem_iUnion, not_and,
        Subtype.exists] at this
      simpa only [dist_comm, mem_ball, not_lt] using this (G a) G_lt
    · apply le_trans _ (fGn a ha).2
      have B : p.c (p.index (G b)) ∉ p.iUnionUpTo (G a) := by
        intro H; exact (fGn b hb).1 (p.monotone_iUnionUpTo G_lt.le H)
      let b' : { t // p.c t ∉ p.iUnionUpTo (G a) } := ⟨p.index (G b), B⟩
      apply @le_ciSup _ _ _ (fun t : { t // p.c t ∉ p.iUnionUpTo (G a) } => p.r t) _ b'
      refine ⟨p.r_bound, fun t ht => ?_⟩
      simp only [exists_prop, mem_range, Subtype.exists] at ht
      rcases ht with ⟨u, hu⟩
      rw [← hu.2]
      exact p.r_le _
-- 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))
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 b : Fin N.succ
a_ne_b : a ≠ 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 : ℕ))) ∨
    p.r (p.index (G (↑b : ℕ))) ≤ dist (p.c (p.index (G (↑b : ℕ)))) (p.c (p.index (G (↑a : ℕ)))) ∧
      p.r (p.index (G (↑a : ℕ))) ≤ p.τ * p.r (p.index (G (↑b : ℕ)))
have inr : ∀
  (this :
    ∀ ⦃a b : Fin N.succ⦄ (a_ne_b : a ≠ b) (G_le : 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 : ℕ))) ∨
        p.r (p.index (G (↑b : ℕ))) ≤ dist (p.c (p.index (G (↑b : ℕ)))) (p.c (p.index (G (↑a : ℕ)))) ∧
          p.r (p.index (G (↑a : ℕ))) ≤ p.τ * p.r (p.index (G (↑b : ℕ))))
  (G_le : ¬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 : ℕ))) ∨
    p.r (p.index (G (↑b : ℕ))) ≤ dist (p.c (p.index (G (↑b : ℕ)))) (p.c (p.index (G (↑a : ℕ)))) ∧
      p.r (p.index (G (↑a : ℕ))) ≤ p.τ * p.r (p.index (G (↑b : ℕ)))
Tactic: wlog G_le : G a ≤ G b generalizing a b
-- 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))
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 b : Fin N.succ
a_ne_b : a ≠ b
inr :
  ∀
    (this :
      ∀ ⦃a b : Fin N.succ⦄ (a_ne_b : a ≠ b) (G_le : 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 : ℕ))) ∨
          p.r (p.index (G (↑b : ℕ))) ≤ dist (p.c (p.index (G (↑b : ℕ)))) (p.c (p.index (G (↑a : ℕ)))) ∧
            p.r (p.index (G (↑a : ℕ))) ≤ p.τ * p.r (p.index (G (↑b : ℕ))))
    (G_le : ¬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 : ℕ))) ∨
      p.r (p.index (G (↑b : ℕ))) ≤ dist (p.c (p.index (G (↑b : ℕ)))) (p.c (p.index (G (↑a : ℕ)))) ∧
        p.r (p.index (G (↑a : ℕ))) ≤ p.τ * p.r (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 : ℕ))) ∨
    p.r (p.index (G (↑b : ℕ))) ≤ dist (p.c (p.index (G (↑b : ℕ)))) (p.c (p.index (G (↑a : ℕ)))) ∧
      p.r (p.index (G (↑a : ℕ))) ≤ p.τ * p.r (p.index (G (↑b : ℕ)))
have wlog : ∀ ⦃a b : Fin N.succ⦄ (a_ne_b : a ≠ b) (G_le : 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 : ℕ))) ∨
    p.r (p.index (G (↑b : ℕ))) ≤ dist (p.c (p.index (G (↑b : ℕ)))) (p.c (p.index (G (↑a : ℕ)))) ∧
      p.r (p.index (G (↑a : ℕ))) ≤ p.τ * p.r (p.index (G (↑b : ℕ)))
Tactic: wlog G_le : G a ≤ G b generalizing a b
Cleared hypotheses: a, b, a_ne_b
-- 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))
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 b : Fin N.succ
a_ne_b : a ≠ b
G_le : G (↑a : ℕ) ≤ G (↑b : ℕ)
⊢ G (↑a : ℕ) < G (↑b : ℕ)
have inl : ∀ (H : G (↑a : ℕ) < G (↑b : ℕ)), G (↑a : ℕ) < G (↑b : ℕ)
Tactic: rcases G_le.lt_or_eq with (H | H)
-- 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))
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 b : Fin N.succ
a_ne_b : a ≠ b
G_le : G (↑a : ℕ) ≤ G (↑b : ℕ)
inl : ∀ (H : G (↑a : ℕ) < G (↑b : ℕ)), G (↑a : ℕ) < G (↑b : ℕ)
⊢ G (↑a : ℕ) < G (↑b : ℕ)
have inr : ∀ (H : G (↑a : ℕ) = G (↑b : ℕ)), G (↑a : ℕ) < G (↑b : ℕ)
Tactic: rcases G_le.lt_or_eq with (H | H)
-- 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))
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 b : Fin N.succ
a_ne_b : a ≠ b
G_le : G (↑a : ℕ) ≤ G (↑b : ℕ)
H : G (↑a : ℕ) = G (↑b : ℕ)
⊢ G (↑a : ℕ) < G (↑b : ℕ)
have A₁ : (↑a : ℕ) ≠ (↑b : ℕ)
Tactic: have A : (a : ℕ) ≠ b := Fin.val_injective.ne a_ne_b