awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs_eq : s = cylinder (α := α) I S
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
let let₁ let₂ let₃ :
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
let₄ :
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
  ∀ (hS' : MeasurableSet S'),
    projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
let₅ :
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
  let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T;
  ∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T'),
    projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
let₆ :
  let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
  let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T;
  ∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T') (h_eq1 : s = cylinder (α := α) (I ∪ J) S'),
    projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
⊢ projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
have let₇ : let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' S;
let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) sorry ⁻¹' T;
∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T') (h_eq1 : s = cylinder (α := α) (I ∪ J) S')
  (h_eq2 : t = cylinder (α := α) (I ∪ J) T'),
  projectiveFamilyFun (α := α) P (s ∪ t) = projectiveFamilyFun (α := α) P s + projectiveFamilyFun (α := α) P t
Tactic: classical
  let S' := restrict₂ (subset_union_left (s₂ := J)) ⁻¹' S
  let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T
  have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
  have hT' : MeasurableSet T' := measurable_restrict₂ _ hT
  have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J
  have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I
  have h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T') := by
    rw [hs_eq, ht_eq]; exact union_cylinder _ _ _ _
  rw [projectiveFamilyFun_congr hP hs h_eq1 hS', projectiveFamilyFun_congr hP ht h_eq2 hT',
    projectiveFamilyFun_congr hP (union_mem_measurableCylinders hs ht) h_eq3 (hS'.union hT')]
  cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hP : IsProjectiveMeasureFamily (α := α) P
s : Set ((i : ι) → α i)
hs_eq : s = cylinder (α := α) I S
hS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞) ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)
have rw : projectiveFamilyFun (α := α) P s = (P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S
Tactic: rw [projectiveFamilyContent_eq,
    projectiveFamilyFun_congr hP ((mem_measurableCylinders s).mpr ⟨I, S, hS, hs_eq⟩) hs_eq hS]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hP : IsProjectiveMeasureFamily (α := α) P
s : Set ((i : ι) → α i)
hs_eq : s = cylinder (α := α) I S
hS : MeasurableSet S
rw : projectiveFamilyFun (α := α) P s = (P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S
⊢ Eq (α := ℝ≥0∞) ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)
  ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)
Tactic: rw [projectiveFamilyContent_eq,
    projectiveFamilyFun_congr hP ((mem_measurableCylinders s).mpr ⟨I, S, hS, hs_eq⟩) hs_eq hS]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.SimpleGraph (goal)
Goal:
V : Type u_1
a : Sym2 V
u v : V
⊢ Measurable (β := Prop) fun (x : SimpleGraph V) ↦ Quot.mk (Sym2.Rel V) (u, v) ∈ x.edgeSet
have mk : Measurable (β := Prop) fun (x : SimpleGraph V) ↦ x.Adj u v
Tactic: simp only [mem_edgeSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.SimpleGraph (goal)
Goal:
V : Type u_1
⊢ Measurable.{u_1, u_1} (α := Set (Sym2 V)) fromEdgeSet
have simp : ∀ (u v : V), Measurable (β := Prop) fun (ω : Set (Sym2 V)) ↦ s(u, v) ∈ ω ∧ ¬u = v
Tactic: simp only [measurable_iff_adj, fromEdgeSet_adj, ne_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.SimpleGraph (goal)
Goal:
V : Type u_1
inst : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
⊢ MeasurableSet (edgeSet '' s)
have simp : Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦
  fromEdgeSet x ∈ s ∧ ∀ ⦃a : Sym2 V⦄, Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet a → a ∉ x
Tactic: simp only [← measurable_mem, Set.mem_image, edgeSet_eq_iff, ↓existsAndEq, true_and,
      Set.disjoint_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.SimpleGraph (goal)
Goal:
V : Type u_1
inst : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
⊢ Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦
    fromEdgeSet x ∈ s ∧ ∀ ⦃a : Sym2 V⦄, Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet a → a ∉ x
have refine_1 : ∀ (e : Sym2 V), Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦ Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet e
Tactic: refine .and (hs.mem.comp measurable_fromEdgeSet) <| .forall fun e ↦ .imp ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.SimpleGraph (goal)
Goal:
V : Type u_1
inst : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
refine_1 :
  ∀ (e : Sym2 V), Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦ Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet e
⊢ Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦
    fromEdgeSet x ∈ s ∧ ∀ ⦃a : Sym2 V⦄, Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet a → a ∉ x
have refine_2 : ∀ (e : Sym2 V), Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦ e ∉ x
Tactic: refine .and (hs.mem.comp measurable_fromEdgeSet) <| .forall fun e ↦ .imp ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
⊢ Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) univ : ENNReal) (1 : ENNReal)
have rw : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc 0 1) : ENNReal) (1 : ENNReal)
Tactic: rw [Measure.Subtype.volume_univ nullMeasurableSet_Icc, Real.volume_Icc, sub_zero,
      ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
rw : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc 0 1) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) univ : ENNReal) (1 : ENNReal)
have rw₁ : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0) = 1
Tactic: rw [Measure.Subtype.volume_univ nullMeasurableSet_Icc, Real.volume_Icc, sub_zero,
      ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
rw : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc 0 1) : ENNReal) (1 : ENNReal)
rw₁ : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0) = 1
⊢ Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) univ : ENNReal) (1 : ENNReal)
have rw₂ : ENNReal.ofReal 1 = 1
Tactic: rw [Measure.Subtype.volume_univ nullMeasurableSet_Icc, Real.volume_Icc, sub_zero,
      ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
rw : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc 0 1) : ENNReal) (1 : ENNReal)
rw₁ : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0) = 1
rw₂ : ENNReal.ofReal 1 = 1
⊢ Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) univ : ENNReal) (1 : ENNReal)
have rw₃ : Eq (α := ENNReal) 1 1
Tactic: rw [Measure.Subtype.volume_univ nullMeasurableSet_Icc, Real.volume_Icc, sub_zero,
      ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
⊢ Eq (α := Measure (↑I : Type)) (map σ volume) volume
have h : ∀ (s : Set (↑I : Type)) (hs : MeasurableSet s),
  Eq (α := ENNReal) ((map σ volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
s : Set (↑I : Type)
hs : MeasurableSet s
⊢ Eq (α := ENNReal) ((map σ volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
have h : Eq (α := ENNReal)
  ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
    ENNReal)
  ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
Tactic: apply symmMeasurableEquiv.map_apply _ |>.trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
s : Set (↑I : Type)
hs : MeasurableSet s
| ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
    ENNReal)
have rw : ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
Tactic: rw [coe_symmMeasurableEquiv, volume_apply, image_coe_preimage_symm,
      ← map_apply (by fun_prop) (measurableSet_Icc.subtype_image hs),
      volume.measurePreserving_sub_left 1 |>.map_eq, ← volume_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
s : Set (↑I : Type)
hs : MeasurableSet s
⊢ Eq (α := ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
      ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
have conv_lhs : Eq (α := ENNReal)
  ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
    ENNReal)
  ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
Tactic: conv_lhs => rw [coe_symmMeasurableEquiv, volume_apply, image_coe_preimage_symm,
      ← map_apply (by fun_prop) (measurableSet_Icc.subtype_image hs),
      volume.measurePreserving_sub_left 1 |>.map_eq, ← volume_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.UnitInterval (goal)
Goal:
s : Set (↑I : Type)
hs : MeasurableSet s
conv_lhs :
  Eq (α := ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
      ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
      ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
have h : Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
  ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
Tactic: conv_lhs => rw [coe_symmMeasurableEquiv, volume_apply, image_coe_preimage_symm,
      ← map_apply (by fun_prop) (measurableSet_Icc.subtype_image hs),
      volume.measurePreserving_sub_left 1 |>.map_eq, ← volume_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
τ : ℝ
inst : Inhabited α
inst_1 : MetricSpace α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
hi : i < last 0
⊢ 1 ≤ dist.{u_1} (α := α) (default i) (default (last 0)) ∧ 1 ≤ τ * 1
have hi₁ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (last 0) (last 0)
Tactic: rw [Subsingleton.elim (α := Fin 1) i (last 0)] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
τ : ℝ
inst : Inhabited α
inst_1 : MetricSpace α
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
hi : i < last 0
⊢ dist.{u_1} (α := α) (default i) (default (last 0)) ≤ HAdd.hAdd (α := ℝ) 1 1
have hi₁ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (last 0) (last 0)
Tactic: rw [Subsingleton.elim (α := Fin 1) i (last 0)] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
have inl : ∀ (H : i < last N), dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
Tactic: rcases lt_or_ge i (last N) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
inl : ∀ (H : i < last N), dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
have inr : ∀ (H : last N ≤ i), dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
Tactic: rcases lt_or_ge i (last N) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
have I : i = last N
Tactic: have I : i = last N := top_le_iff.1 H
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
I : i = last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
have this : 0 ≤ a.r (last N)
Tactic: have := (a.rpos (last N)).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
⊢ a.r (last N) ≤ τ * a.r i
have inl : ∀ (H : i < last N), a.r (last N) ≤ τ * a.r i
Tactic: rcases lt_or_ge i (last N) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
inl : ∀ (H : i < last N), a.r (last N) ≤ τ * a.r i
⊢ a.r (last N) ≤ τ * a.r i
have inr : ∀ (H : last N ≤ i), a.r (last N) ≤ τ * a.r i
Tactic: rcases lt_or_ge i (last N) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
⊢ a.r (last N) ≤ τ * a.r i
have this : i = last N
Tactic: have : i = last N := top_le_iff.1 H
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
h : 1 ≤ τ
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ τ * a.r i
have inr : a.r (last N) ≤ τ * a.r (last N)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
⊢ Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
have by_contra : ∀
  (h :
    ¬Set.Nonempty.{u + 1} (α := Ordinal.{u})
        {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}),
  False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
⊢ False
have suffices : Function.Injective p.index
Tactic: suffices H : Function.Injective p.index from not_injective_of_ordinal p.index H
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
⊢ x = y
have inr : ∀ (this : ∀ ⦃x y : Ordinal.{u}⦄ (hxy : p.index x = p.index y) (x_le_y : x ≤ y), x = y) (x_le_y : ¬x ≤ y), x = y
Tactic: wlog x_le_y : x ≤ y generalizing x y
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
inr : ∀ (this : ∀ ⦃x y : Ordinal.{u}⦄ (hxy : p.index x = p.index y) (x_le_y : x ≤ y), x = y) (x_le_y : ¬x ≤ y), x = y
⊢ x = y
have wlog : ∀ ⦃x y : Ordinal.{u}⦄ (hxy : p.index x = p.index y) (x_le_y : x ≤ y), x = y
Tactic: wlog x_le_y : x ≤ y generalizing x y
Cleared hypotheses: x, y, hxy
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
⊢ x = y
have inl : ∀ (hxy : p.index x = p.index x) (x_le_y : x ≤ x), x = x
Tactic: rcases eq_or_lt_of_le x_le_y with (rfl | H)
Cleared hypotheses: y, hxy, x_le_y
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
inl : ∀ (hxy : p.index x = p.index x) (x_le_y : x ≤ x), x = x
⊢ x = y
have inr : ∀ (H : x < y), x = y
Tactic: rcases eq_or_lt_of_le x_le_y with (rfl | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
h :
  ¬Set.Nonempty.{u + 1} (α := Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
⊢ x = y
have h₁ : ∀ (x : Ordinal.{u}), ∃ (x_1 : β), p.c x_1 ∉ p.iUnionUpTo x ∧ p.R x ≤ p.τ * p.r x_1
Tactic: simp only [nonempty_def, not_exists, exists_prop, not_and, not_lt, not_le, mem_setOf_eq,
    not_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∀ (x : Ordinal.{u}), ∃ (x_1 : β), p.c x_1 ∉ p.iUnionUpTo x ∧ p.R x ≤ p.τ * p.r x_1
⊢ x = y
have h₁ : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
Tactic: specialize h y
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ p.index y = Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
have rw : Eq.{u + 1} (α := β)
  (Classical.epsilon fun (b : β) ↦
    p.c b ∉
        ⋃ (j : { j : Ordinal.{u} // j < y }),
          ball (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) ∧
      ⨆ (b :
          { b : β //
            p.c b ∉
              ⋃ (j : { j : Ordinal.{u} // j < y }),
                ball (p.c (p.index (↑j : Ordinal.{u}))) (p.r (p.index (↑j : Ordinal.{u}))) }),
          p.r (↑b : β) ≤
        p.τ * p.r b)
  (Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b)
Tactic: rw [TauPackage.index]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ p.c (p.index y) ∉ p.iUnionUpTo y
have this : p.index y = Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
Tactic: have :
        p.index y =
          Classical.epsilon fun b : β => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b := by
      rw [TauPackage.index]; rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
⊢ p.c (p.index y) ∉ p.iUnionUpTo y
have rw : p.c (Classical.epsilon fun (b : β) ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b) ∉ p.iUnionUpTo y
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
⊢ x = y
have A : p.c (p.index y) ∉ p.iUnionUpTo y
Tactic: have A : p.c (p.index y) ∉ p.iUnionUpTo y := by
    have :
        p.index y =
          Classical.epsilon fun b : β => p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b := by
      rw [TauPackage.index]; rfl
    rw [this]
    exact (Classical.epsilon_spec h).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.c (p.index y) ∉ p.iUnionUpTo y
⊢ x = y
have A₁ : ∀ x < y, p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
Tactic: simp only [iUnionUpTo, not_exists, exists_prop, mem_iUnion, not_and,
    Subtype.exists] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : ∀ x < y, p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
⊢ x = y
have A₁ : p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
Tactic: specialize A x H
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ (x : β), p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
⊢ x = y
have A₁ : p.r (p.index y) ≤ 0
Tactic: replace A : p.r (p.index y) ≤ 0 := by simpa [hxy] using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : Nonempty β
p : TauPackage β α
x : β
⊢ ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
have this : Membership.mem (γ := Set Ordinal.{u}) {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
  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