awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 :
  ∀ (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
⊢ (∀ 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:
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 => ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c

Tactic:
(UT uU).2.2 a hat b hbu hab

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
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
⊢ ∃ (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

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : ι
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:
⟨c, ⟨u, uU, cu⟩, ac, hc⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 : ι
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:
exact ⟨c, ⟨u, uU, cu⟩, ac, hc⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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}
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
⊢ ∃ 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⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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

Tactic:
⟨u, hu.prop.1, hu.prop.2.1, fun a hat => ?_⟩

Premises used: Maximal.prop, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
refine : ∀ (a : ι) (hat : a ∈ t), ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
⊢ ∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b

Tactic:
refine ⟨u, hu.prop.1, hu.prop.2.1, fun a hat => ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
by_contra! : ∀ (hcon : ∀ (b : ι) (_ : b ∈ u) (_ : (B a ∩ B b).Nonempty), τ * δ b < δ a), False
⊢ ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b

Tactic:
by_contra! hcon
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
by_contra : ∀ (h : ¬Disjoint (B a) (B c)), False
⊢ Disjoint (B a) (B c)

Tactic:
by_contra h
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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)
⊢ (B a ∩ B c).Nonempty

Tactic:
rw [not_disjoint_iff_nonempty_inter] at h

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
⊢ ∃ d ∈ u, (B a ∩ B d).Nonempty ∧ δ a ≤ τ * δ d

Tactic:
hu.prop.2.2 a hat c hc h

Premises used: Maximal.prop, And.right
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
obtain : ∀ (d : ι) (du : d ∈ u) (ad : (B a ∩ B d).Nonempty) (hd : δ a ≤ τ * δ d), False
⊢ 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

Premises used: Maximal.prop, And.right
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
d : ι
du : d ∈ u
ad : (B a ∩ B d).Nonempty
hd : δ a ≤ τ * δ d
⊢ False

Tactic:
lt_irrefl _ ((hcon d du ad).trans_le hd)

Premises used: lt_irrefl, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
d : ι
du : d ∈ u
ad : (B a ∩ B d).Nonempty
hd : δ a ≤ τ * δ d
⊢ False

Tactic:
exact lt_irrefl _ ((hcon d du ad).trans_le hd)

Premises used: lt_irrefl, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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 ∈ 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)
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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)}
⊢ A.Nonempty

Tactic:
have Anonempty : A.Nonempty := ⟨a, hat, a_disj⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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)

Tactic:
⟨R, fun x xA => ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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)
refine : ∀ (x : ℝ) (xA : x ∈ δ '' A), x ≤ R
⊢ BddAbove (δ '' A)

Tactic:
refine ⟨R, fun x xA => ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
rcases : ∀ (a' : ι) (ha' : a' ∈ A) (xA : δ a' ∈ δ '' A), δ a' ≤ R
⊢ x ≤ R

Tactic:
rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩

Premises used: Set.mem_image, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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)
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
⊢ δ a' ≤ R

Tactic:
δle a' ha'.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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)
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
⊢ δ a' ≤ R

Tactic:
exact δle a' ha'.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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)

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
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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)
⊢ 0 ≤ m

Tactic:
have : 0 ≤ m := (δnonneg a hat).trans (le_csSup bddA (mem_image_of_mem _ ⟨hat, a_disj⟩))
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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'
inr : ∀ (mpos : 0 < m), ∃ a' ∈ A, m / τ ≤ δ a'
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
rcases eq_or_lt_of_le this with (mzero | mpos)

Premises used: eq_or_lt_of_le
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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'

Tactic:
⟨a, ⟨hat, a_disj⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
inl : m / τ ≤ δ a
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
refine ⟨a, ⟨hat, a_disj⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
⊢ m / τ ≤ δ a

Tactic:
simpa only [← mzero, zero_div] using δnonneg a hat

Premises used: zero_div
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
rw : m < m * τ
⊢ m / τ < m

Tactic:
rw [div_lt_iff₀ (zero_lt_one.trans hτ)]

Premises used: div_lt_iff₀, zero_lt_one, LT.lt.trans
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
rw : m * 1
| m

Tactic:
rw [← mul_one m]

Premises used: mul_one
-- Module: Mathlib.MeasureTheory.Covering.Vitali
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
conv_lhs : m * 1 < m * τ
⊢ m < m * τ

Tactic:
conv_lhs => rw [← mul_one m]

Premises used: mul_one