awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
⊢ ∃ (m : Set ι), Maximal (fun (x : Set ι) ↦ x ∈ T) m
have refine : ∀ (U : Set (Set ι)) (UT : U ⊆ T) (hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U), ∃ ub ∈ T, ∀ s ∈ U, s ⊆ ub
Tactic: refine zorn_subset _ fun U UT hU => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U
⊢ ∃ ub ∈ T, ∀ s ∈ U, s ⊆ ub
have refine : ⋃₀ U ∈ T
Tactic: refine ⟨⋃₀ U, ?_, fun s hs => subset_sUnion_of_mem hs⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U
⊢ ⋃₀ U ∈ T
have simp : (∀ t' ∈ U, t' ⊆ t) ∧
  (⋃₀ U).PairwiseDisjoint B ∧
    ∀ a ∈ t,
      ∀ (b : ι),
        ∀ x ∈ U, b ∈ x → (B a ∩ B b).Nonempty → ∃ (c : ι), (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c
Tactic: simp only [T, Set.sUnion_subset_iff, and_imp, forall_exists_index, mem_sUnion,
      Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U
⊢ (∀ t' ∈ U, t' ⊆ t) ∧
    (⋃₀ U).PairwiseDisjoint B ∧
      ∀ a ∈ t,
        ∀ (b : ι),
          ∀ x ∈ U, b ∈ x → (B a ∩ B b).Nonempty → ∃ (c : ι), (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c
have u : ∀ (a : ι) (hat : a ∈ t) (b : ι) (u : Set ι) (uU : u ∈ U) (hbu : b ∈ u) (hab : (B a ∩ B b).Nonempty),
  ∃ (c : ι), (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c
Tactic: refine
      ⟨fun u hu => (UT hu).1, (pairwiseDisjoint_sUnion hU.directedOn).2 fun u hu => (UT hu).2.1,
        fun a hat b u uU hbu hab => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U
a : ι
hat : a ∈ t
b : ι
u : Set ι
uU : u ∈ U
hbu : b ∈ u
hab : (B a ∩ B b).Nonempty
⊢ ∃ (c : ι), (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c
have obtain : ∀ (c : ι) (cu : c ∈ u) (ac : (B a ∩ B c).Nonempty) (hc : δ a ≤ τ * δ c),
  ∃ (c : ι), (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c
Tactic: obtain ⟨c, cu, ac, hc⟩ : ∃ c, c ∈ u ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c :=
      (UT uU).2.2 a hat b hbu hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
⊢ ∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
have obtain : ∀ (u : Set ι) (hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u),
  ∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
Tactic: obtain ⟨u, hu⟩ : ∃ m, Maximal (fun x ↦ x ∈ T) m := by
    refine zorn_subset _ fun U UT hU => ?_
    refine ⟨⋃₀ U, ?_, fun s hs => subset_sUnion_of_mem hs⟩
    simp only [T, Set.sUnion_subset_iff, and_imp, forall_exists_index, mem_sUnion,
      Set.mem_setOf_eq]
    refine
      ⟨fun u hu => (UT hu).1, (pairwiseDisjoint_sUnion hU.directedOn).2 fun u hu => (UT hu).2.1,
        fun a hat b u uU hbu hab => ?_⟩
    obtain ⟨c, cu, ac, hc⟩ : ∃ c, c ∈ u ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c :=
      (UT uU).2.2 a hat b hbu hab
    exact ⟨c, ⟨u, uU, cu⟩, ac, hc⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
⊢ ∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
have refine : ∀ (a : ι) (hat : a ∈ t), ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
Tactic: refine ⟨u, hu.prop.1, hu.prop.2.1, fun a hat => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
⊢ ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
have by_contra! : ∀ (hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a), False
Tactic: by_contra! hcon
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
c : ι
hc : c ∈ u
⊢ Disjoint (B a) (B c)
have by_contra : ∀ (h : ¬Disjoint (B a) (B c)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
c : ι
hc : c ∈ u
h : ¬Disjoint (B a) (B c)
⊢ False
have h₁ : (B a ∩ B c).Nonempty
Tactic: rw [not_disjoint_iff_nonempty_inter] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
c : ι
hc : c ∈ u
h : (B a ∩ B c).Nonempty
⊢ False
have obtain : ∀ (d : ι) (du : d ∈ u) (ad : (B a ∩ B d).Nonempty) (hd : δ a ≤ τ * δ d), False
Tactic: obtain ⟨d, du, ad, hd⟩ : ∃ d, d ∈ u ∧ (B a ∩ B d).Nonempty ∧ δ a ≤ τ * δ d :=
      hu.prop.2.2 a hat c hc h
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
⊢ False
have a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
Tactic: have a_disj : ∀ c ∈ u, Disjoint (B a) (B c) := by
    intro c hc
    by_contra h
    rw [not_disjoint_iff_nonempty_inter] at h
    obtain ⟨d, du, ad, hd⟩ : ∃ d, d ∈ u ∧ (B a ∩ B d).Nonempty ∧ δ a ≤ τ * δ d :=
      hu.prop.2.2 a hat c hc h
    exact lt_irrefl _ ((hcon d du ad).trans_le hd)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
⊢ False
have Anonempty : A.Nonempty
Tactic: have Anonempty : A.Nonempty := ⟨a, hat, a_disj⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
⊢ BddAbove (δ '' A)
have refine : ∀ (x : ℝ) (xA : x ∈ δ '' A), x ≤ R
Tactic: refine ⟨R, fun x xA => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
x : ℝ
xA : x ∈ δ '' A
⊢ x ≤ R
have rcases : ∀ (a' : ι) (ha' : a' ∈ A) (xA : δ a' ∈ δ '' A), δ a' ≤ R
Tactic: rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
Cleared hypotheses: x, xA
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
⊢ False
have bddA : BddAbove (δ '' A)
Tactic: have bddA : BddAbove (δ '' A) := by
    refine ⟨R, fun x xA => ?_⟩
    rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
    exact δle a' ha'.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
have this : 0 ≤ m
Tactic: have : 0 ≤ m := (δnonneg a hat).trans (le_csSup bddA (mem_image_of_mem _ ⟨hat, a_disj⟩))
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
have inl : ∀ (mzero : 0 = m), ∃ a' ∈ A, m / τ ≤ δ a'
Tactic: rcases eq_or_lt_of_le this with (mzero | mpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
inl : ∀ (mzero : 0 = m), ∃ a' ∈ A, m / τ ≤ δ a'
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
have inr : ∀ (mpos : 0 < m), ∃ a' ∈ A, m / τ ≤ δ a'
Tactic: rcases eq_or_lt_of_le this with (mzero | mpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mzero : 0 = m
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
have inl : m / τ ≤ δ a
Tactic: refine ⟨a, ⟨hat, a_disj⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ m / τ < m
have rw : m < m * τ
Tactic: rw [div_lt_iff₀ (zero_lt_one.trans hτ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
| m
have rw : m * 1
Tactic: rw [← mul_one m]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ m < m * τ
have conv_lhs : m * 1 < m * τ
Tactic: conv_lhs => rw [← mul_one m]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
have I : m / τ < m
Tactic: have I : m / τ < m := by
        rw [div_lt_iff₀ (zero_lt_one.trans hτ)]
        conv_lhs => rw [← mul_one m]
        gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
have inr : ∀ (x : ℝ) (xA : x ∈ δ '' A) (hx : m / τ < x), ∃ a' ∈ A, m / τ ≤ δ a'
Tactic: rcases exists_lt_of_lt_csSup (Anonempty.image _) I with ⟨x, xA, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
x : ℝ
xA : x ∈ δ '' A
hx : m / τ < x
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
have inr : ∀ (a' : ι) (ha' : a' ∈ A) (xA : δ a' ∈ δ '' A) (hx : m / τ < δ a'), ∃ a' ∈ A, m / τ ≤ δ a'
Tactic: rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
Cleared hypotheses: x, xA, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
⊢ False
have obtain : ∀ (a' : ι) (a'A : a' ∈ A) (ha' : m / τ ≤ δ a'), False
Tactic: obtain ⟨a', a'A, ha'⟩ : ∃ a' ∈ A, m / τ ≤ δ a' := by
    have : 0 ≤ m := (δnonneg a hat).trans (le_csSup bddA (mem_image_of_mem _ ⟨hat, a_disj⟩))
    rcases eq_or_lt_of_le this with (mzero | mpos)
    · refine ⟨a, ⟨hat, a_disj⟩, ?_⟩
      simpa only [← mzero, zero_div] using δnonneg a hat
    · have I : m / τ < m := by
        rw [div_lt_iff₀ (zero_lt_one.trans hτ)]
        conv_lhs => rw [← mul_one m]
        gcongr
      rcases exists_lt_of_lt_csSup (Anonempty.image _) I with ⟨x, xA, hx⟩
      rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩
      exact ⟨a', ha', hx.le⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun (x : Set ι) ↦ x ∈ T) u
A : Set ι := {a' : ι | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
⊢ False
have a'_ne_u : a' ∉ u
Tactic: have a'_ne_u : a' ∉ u := fun H => (hne _ a'A.1).ne_empty (disjoint_self.1 (a'A.2 _ H))