-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem mem_iUnionUpTo_lastStep (x : β) : p.c x ∈ p.iUnionUpTo p.lastStep

Proof state:
case inr.intro.intro.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
y : β
hy1 : p.c y ∉ p.iUnionUpTo p.lastStep
hy2 : p.τ⁻¹ * p.R p.lastStep < p.r y
Hy : p.τ * p.r y < p.R p.lastStep
⊢ False

Tactic:
rw [← div_eq_inv_mul] at hy2

Result:
case inr.intro.intro.inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
y : β
hy1 : p.c y ∉ p.iUnionUpTo p.lastStep
hy2 : p.R p.lastStep / p.τ < p.r y
Hy : p.τ * p.r y < p.R p.lastStep
⊢ False

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
⊢ ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep

Tactic:
have : p.lastStep ∈ {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b} :=
  csInf_mem p.lastStep_nonempty

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
this : p.lastStep ∈ {i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
⊢ ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
⊢ p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep

Tactic:
conv_rhs => rw [← one_mul (p.R p.lastStep)]

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
⊢ p.τ⁻¹ * p.R p.lastStep < 1 * p.R p.lastStep

Proof state:
case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
⊢ (range fun b => p.r ↑b).Nonempty

Tactic:
rw [← image_univ, image_nonempty]

Result:
case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
⊢ univ.Nonempty

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
⊢ 0 < p.R p.lastStep

Tactic:
apply lt_trans (mul_pos (_root_.zero_lt_one.trans p.one_lt_tau) (p.rpos _)) H

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
⊢ p.c x ∈ p.iUnionUpTo p.lastStep

Tactic:
have A : ∀ z : β, p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep := by
  have : p.lastStep ∈ {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b} :=
    csInf_mem p.lastStep_nonempty
  simpa only [not_exists, mem_setOf_eq, not_and_or, not_le, not_not_mem]

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
⊢ p.c x ∈ p.iUnionUpTo p.lastStep

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
⊢ p.c x ∈ p.iUnionUpTo p.lastStep

Tactic:
by_contra h

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
⊢ False

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
this : p.lastStep ∈ {i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
⊢ ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep

Tactic:
simpa only [not_exists, mem_setOf_eq, not_and_or, not_le, not_not_mem]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.c x ∈ p.iUnionUpTo p.lastStep
⊢ False

Tactic:
exact h H

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
⊢ univ.Nonempty

Tactic:
exact ⟨⟨_, h⟩, mem_univ _⟩

Result:
no goals

Proof state:
case inr.intro.intro.inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
y : β
hy1 : p.c y ∉ p.iUnionUpTo p.lastStep
hy2 : p.τ⁻¹ * p.R p.lastStep < p.r y
Hy : p.c y ∈ p.iUnionUpTo p.lastStep
⊢ False

Tactic:
exact hy1 Hy

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
⊢ ∃ y, p.c y ∉ p.iUnionUpTo p.lastStep ∧ p.τ⁻¹ * p.R p.lastStep < p.r y

Tactic:
have := exists_lt_of_lt_csSup ?_ B

Result:
case refine_2
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
this : ∃ a ∈ range fun b => p.r ↑b, p.τ⁻¹ * p.R p.lastStep < a
⊢ ∃ y, p.c y ∉ p.iUnionUpTo p.lastStep ∧ p.τ⁻¹ * p.R p.lastStep < p.r y

case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
⊢ (range fun b => p.r ↑b).Nonempty