-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux (μ : Measure α)
    [IsFiniteMeasure μ] (f : α → Set ℝ) (s : Set α)
    (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty) :
    ∃ t : Set (α × ℝ), t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧
      μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.1 p.2) = 0 ∧
        t.PairwiseDisjoint fun p => closedBall p.1 p.2

Proof state:
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
n : ℕ
IH : μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n.succ * μ s

Tactic:
rw [pow_succ', mul_assoc]

Result:
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
n : ℕ
IH : μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * ((↑N / (↑N + 1)) ^ n * μ s)

Proof state:
case intro.intro.intro.refine_1
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
p : α × ℝ
hp : p ∈ ⋃ n, ↑(u n)
⊢ p.1 ∈ s

Tactic:
rcases mem_iUnion.1 hp with ⟨n, hn⟩

Result:
case intro.intro.intro.refine_1.intro
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
p : α × ℝ
hp : p ∈ ⋃ n, ↑(u n)
n : ℕ
hn : p ∈ ↑(u n)
⊢ p.1 ∈ s

Proof state:
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅
n : ℕ
⊢ u n.succ = F (u n)

Tactic:
simp only [u, Function.comp_apply, Function.iterate_succ']

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
n : ℕ
IH : P (u n)
⊢ P (u (n + 1))

Tactic:
rw [u_succ]

Result:
case succ
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t => ((↑t).PairwiseDisjoint fun p => closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n => F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
n : ℕ
IH : P (u n)
⊢ P (F (u n))