awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith₂ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 2 1 = 2
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith₃ : τ * r b < r a + dist (x a) (x b) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) ≤ r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : τ * r b < r a + dist (x a) (x b) → GT.gt (α := ℝ) 2 0
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith₄ : τ * r b < r a + dist (x a) (x b) →
  2 * r a - (1 * τ - HMul.hMul (α := ℝ) 1 1) * (1 * r b) + (dist (x a) (x b) - (r a + r b)) +
      (τ * r b - (r a + dist (x a) (x b))) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
have A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
Tactic: have A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b) := by
    intro a ha
    rcases hu a ha with ⟨b, bu, hb, rb⟩
    refine ⟨b, bu, ?_⟩
    have : dist (x a) (x b) ≤ r a + r b := dist_le_add_of_nonempty_closedBall_inter_closedBall hb
    apply closedBall_subset_closedBall'
    linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
have neg : ∀ (a : ι) (ha : a ∈ t), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
Tactic: refine ⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
have neg : ∀ (h'a : 0 ≤ r a), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
Tactic: rcases le_or_gt 0 (r a) with (h'a | h'a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
neg : ∀ (h'a : 0 ≤ r a), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
have neg₁ : ∀ (h'a : r a < 0), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
Tactic: rcases le_or_gt 0 (r a) with (h'a | h'a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 ≤ r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
have neg : ∀ (b : ι) (rb : b ∈ t ∧ 0 ≤ r b), ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
Tactic: rcases ht with ⟨b, rb⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
t' : Set ι := {a : ι | a ∈ t ∧ 0 ≤ r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ closedBall (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (closedBall (x a) (r a) ∩ closedBall (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : r a < 0
b : ι
rb : b ∈ t ∧ 0 ≤ r b
⊢ ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
have neg : ∀ (c : ι) (cu : c ∈ u),
  closedBall (x b) (r b) ⊆ closedBall (x c) (τ * r c) → ∃ b ∈ u, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)
Tactic: rcases A b ⟨rb.1, rb.2⟩ with ⟨c, cu, _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have inl : ∀ (hr : ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → r a ≤ R),
  ∃ u ⊆ ∅,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Tactic: rcases eq_empty_or_nonempty t with (rfl | _)
Cleared hypotheses: t, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
inl :
  ∀ (hr : ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → r a ≤ R),
    ∃ u ⊆ ∅,
      (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
        ∀ (a : ι), Membership.mem (γ := Set ι) ∅ a → ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have inr : t.Nonempty →
  ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Tactic: rcases eq_empty_or_nonempty t with (rfl | _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have pos : ∀ (ht : ∀ a ∈ t, r a ≤ 0),
  ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Tactic: by_cases! ht : ∀ a ∈ t, r a ≤ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
pos :
  ∀ (ht : ∀ a ∈ t, r a ≤ 0),
    ∃ u ⊆ t,
      (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
        ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have neg : ∀ (ht : ∃ a ∈ t, 0 < r a),
  ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Tactic: by_cases! ht : ∀ a ∈ t, r a ≤ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
⊢ 1 < (τ - 1) / 2
have linarith : (τ - 1) / 2 ≤ 1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
linarith : (τ - 1) / 2 ≤ 1 → 2 / 2 = 1
⊢ 1 < (τ - 1) / 2
have linarith₁ : (τ - 1) / 2 ≤ 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
linarith : (τ - 1) / 2 ≤ 1 → 2 / 2 = 1
linarith₁ : (τ - 1) / 2 ≤ 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 < (τ - 1) / 2
have linarith₂ : (τ - 1) / 2 ≤ 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
linarith : (τ - 1) / 2 ≤ 1 → 2 / 2 = 1
linarith₁ : (τ - 1) / 2 ≤ 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (τ - 1) / 2 ≤ 1 → GT.gt (α := ℝ) 2 0
⊢ 1 < (τ - 1) / 2
have linarith₃ : (τ - 1) / 2 ≤ 1 → 3 - τ + (1 * τ - HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 2 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
⊢ ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have neg : ∀ (u : Set ι) (ut' : u ⊆ t') (u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a))
  (hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b),
  ∃ u ⊆ t,
    (PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)) ∧
      ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Tactic: rcases exists_disjoint_subfamily_covering_enlargement (fun a => ball (x a) (r a)) t' r
      ((τ - 1) / 2) (by linarith) (fun a ha => ha.2.le) R (fun a ha => hr a ha.1) fun a ha =>
      ⟨x a, mem_ball_self ha.2⟩ with
    ⟨u, ut', u_disj, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
⊢ ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have rcases : ∀ (b : ι) (bu : b ∈ u) (hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty) (rb : r a ≤ (τ - 1) / 2 * r b),
  ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Tactic: rcases hu a ha with ⟨b, bu, hb, rb⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
⊢ ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have refine : ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Tactic: refine ⟨b, bu, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
⊢ ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have this : dist (x a) (x b) < r a + r b
Tactic: have : dist (x a) (x b) < r a + r b := dist_lt_add_of_nonempty_ball_inter_ball hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) < r a + r b
⊢ ball (x a) (r a) ⊆ ball (x b) (τ * r b)
have h : r a + dist (x a) (x b) ≤ τ * r b
Tactic: apply ball_subset_ball'
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) < r a + r b
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) < r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) < r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith₂ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) < r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 2 1 = 2
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith₃ : τ * r b < r a + dist (x a) (x b) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h : t.Nonempty
ht : ∃ a ∈ t, 0 < r a
t' : Set ι := {a : ι | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : PairwiseDisjoint.{u_1, u_2} (α := Set α) u fun (a : ι) ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
a : ι
ha : a ∈ t'
b : ι
bu : b ∈ u
hb : (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty
rb : r a ≤ (τ - 1) / 2 * r b
this : dist (x a) (x b) < r a + r b
linarith : τ * r b < r a + dist (x a) (x b) → 2 / 2 = 1
linarith₁ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : τ * r b < r a + dist (x a) (x b) → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : τ * r b < r a + dist (x a) (x b) → GT.gt (α := ℝ) 2 0
⊢ r a + dist (x a) (x b) ≤ τ * r b
have linarith₄ : τ * r b < r a + dist (x a) (x b) →
  2 * r a - (1 * τ - HMul.hMul (α := ℝ) 1 1) * (1 * r b) + (dist (x a) (x b) - (r a + r b)) +
      (τ * r b - (r a + dist (x a) (x b))) =
    0
Tactic: linarith