awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : (↑(Icc 0 n) : Type)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
linarith : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → 2 / 2 = 1
⊢ dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) ≤ δ
have linarith₁ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : (↑(Icc 0 n) : Type)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
linarith : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → 2 / 2 = 1
linarith₁ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) ≤ δ
have linarith₂ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → GT.gt (α := ℝ) 2 0
Tactic: linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : (↑(Icc 0 n) : Type)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
linarith : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → 2 / 2 = 1
linarith₁ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → GT.gt (α := ℝ) 2 0
linarith₃ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → 2 / 2 = 1
linarith₄ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → GT.gt (α := ℝ) 2 0
⊢ dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) ≤ δ
have linarith₆ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) →
  2 * (δ - (dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ))) + (2 * dist x ((↑i : ℕ) • ξ) - 1 * δ) +
      (2 * dist ((↑j : ℕ) • ξ) x - 1 * δ) =
    0
Tactic: linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
have suffices : ¬Pairwise (Disjoint on B)
Tactic: suffices ¬ Pairwise (Disjoint on B) by
    obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this
    refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
    · simpa only [tsub_le_iff_right] using j.property.2.trans le_self_add
    · rw [sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm]
      exact (dist_triangle ((j : ℕ) • ξ) x ((i : ℕ) • ξ)).trans (by
        linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2])
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ False
have apply : n = 0
Tactic: apply hn.ne'
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ
have rw : Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (⋃ (i : (↑(Icc 0 n) : Type)), B i) : ENNReal)
  ((μ : (a : Set A) → ENNReal) univ : ENNReal)
Tactic: rw [← (isClosed_iUnion_of_finite hB).measure_eq_univ_iff_eq (μ := μ)]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (⋃ (i : (↑(Icc 0 n) : Type)), B i) : ENNReal)
    ((μ : (a : Set A) → ENNReal) univ : ENNReal)
have refine : LE.le (α := ENNReal) ((μ : (a : Set A) → ENNReal) univ : ENNReal)
  ((μ : (a : Set A) → ENNReal) (⋃ (i : (↑(Icc 0 n) : Type)), B i) : ENNReal)
Tactic: refine le_antisymm (μ.mono (subset_univ _)) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ n = 0
have h' : Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ
Tactic: have h' : ⋃ j, B j = univ := by
    rw [← (isClosed_iUnion_of_finite hB).measure_eq_univ_iff_eq (μ := μ)]
    refine le_antisymm (μ.mono (subset_univ _)) ?_
    simp_rw [measure_iUnion h (fun _ ↦ measurableSet_closedBall), tsum_fintype,
      B, μ.addHaar_closedBall_center, Finset.sum_const, Finset.card_univ, Fintype.card_Icc,
      Nat.card_Icc, tsub_zero]
    exact hδ
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ
⊢ 0 ≤ δ / 2
have by_contra : ∀ (contra : ¬0 ≤ δ / 2), False
Tactic: by_contra contra
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ
contra : ¬0 ≤ δ / 2
⊢ False
have refine : HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) ≤ 0
Tactic: refine (isOpen_univ.measure_pos μ univ_nonempty).not_ge <| hδ.trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ
contra : ¬0 ≤ δ / 2
⊢ HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) ≤ 0
have suffices : Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) (0 : ENNReal)
Tactic: suffices μ (closedBall 0 (δ / 2)) = 0 by simp [this]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ
contra : ¬0 ≤ δ / 2
⊢ Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) (0 : ENNReal)
have contra₁ : Eq.{u_1 + 1} (α := Set A) (closedBall 0 (δ / 2)) ∅
Tactic: rw [not_le, ← closedBall_eq_empty (x := (0 : A))] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ
⊢ n = 0
have hδ₁ : 0 ≤ δ / 2
Tactic: replace hδ : 0 ≤ δ / 2 := by
    by_contra contra
    refine (isOpen_univ.measure_pos μ univ_nonempty).not_ge <| hδ.trans ?_
    suffices μ (closedBall 0 (δ / 2)) = 0 by simp [this]
    rw [not_le, ← closedBall_eq_empty (x := (0 : A))] at contra
    simp [contra]
Cleared hypotheses: hδ
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
h' : Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ
hδ : 0 ≤ δ / 2
⊢ n = 0
have h'' : ∀ (j : (↑(Icc 0 n) : Type)), (B j).Nonempty
Tactic: have h'' : ∀ j, (B j).Nonempty := by intro j; rwa [nonempty_closedBall]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ T / (↑(n + 1) : ℝ)
have hδ : (volume : (a : Set 𝕊) → ENNReal) univ ≤
  HSMul.hSMul (β := ENNReal) (n + 1)
    ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
Tactic: apply NormedAddCommGroup.exists_norm_nsmul_le (μ := volume) ξ hn
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ (volume : (a : Set 𝕊) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
have hδ : ENNReal.ofReal T ≤
  HSMul.hSMul (β := ENNReal) (n + 1)
    ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
Tactic: rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
    mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
    mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
hδ :
  ENNReal.ofReal T ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
⊢ (volume : (a : Set 𝕊) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
have hδ₁ : ENNReal.ofReal T ≤ (n + 1) • ENNReal.ofReal (min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
Tactic: rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
    mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
    mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
hδ :
  ENNReal.ofReal T ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
hδ₁ : ENNReal.ofReal T ≤ (n + 1) • ENNReal.ofReal (min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
⊢ (volume : (a : Set 𝕊) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
have hδ₂ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
Tactic: rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
    mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
    mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
hδ :
  ENNReal.ofReal T ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
hδ₁ : ENNReal.ofReal T ≤ (n + 1) • ENNReal.ofReal (min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
hδ₂ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
⊢ (volume : (a : Set 𝕊) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
have hδ₃ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (T / (↑(n + 1) : ℝ)))
Tactic: rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
    mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
    mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
hδ :
  ENNReal.ofReal T ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
hδ₁ : ENNReal.ofReal T ≤ (n + 1) • ENNReal.ofReal (min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
hδ₂ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
hδ₃ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (T / (↑(n + 1) : ℝ)))
⊢ (volume : (a : Set 𝕊) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
have hδ₄ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • (T / (↑(n + 1) : ℝ)))
Tactic: rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
    mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
    mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
hδ :
  ENNReal.ofReal T ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
hδ₁ : ENNReal.ofReal T ≤ (n + 1) • ENNReal.ofReal (min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
hδ₂ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
hδ₃ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (T / (↑(n + 1) : ℝ)))
hδ₄ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • (T / (↑(n + 1) : ℝ)))
⊢ (volume : (a : Set 𝕊) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
have hδ₅ : ENNReal.ofReal T ≤ ENNReal.ofReal ((↑(n + 1) : ℝ) * (T / (↑(n + 1) : ℝ)))
Tactic: rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
    mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
    mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
hδ :
  ENNReal.ofReal T ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
hδ₁ : ENNReal.ofReal T ≤ (n + 1) • ENNReal.ofReal (min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
hδ₂ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (2 * (T / (↑(n + 1) : ℝ) / 2)))
hδ₃ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • min T (T / (↑(n + 1) : ℝ)))
hδ₄ : ENNReal.ofReal T ≤ ENNReal.ofReal ((n + 1) • (T / (↑(n + 1) : ℝ)))
hδ₅ : ENNReal.ofReal T ≤ ENNReal.ofReal ((↑(n + 1) : ℝ) * (T / (↑(n + 1) : ℝ)))
⊢ (volume : (a : Set 𝕊) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
have hδ₆ : ENNReal.ofReal T ≤ ENNReal.ofReal T
Tactic: rw [AddCircle.measure_univ, volume_closedBall, ← ENNReal.ofReal_nsmul,
    mul_div_cancel₀ _ two_ne_zero, min_eq_right (div_le_self hT.out.le <| by simp), nsmul_eq_mul,
    mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ZMod p) (↑(p - 1)! : ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
have rw : Eq (α := ZMod p) (↑(∏ x ∈ Ico 1 (p - 1 + 1), x) : ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
Tactic: rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑(∏ x ∈ Ico 1 (p - 1 + 1), x) : ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
⊢ Eq (α := ZMod p) (↑(p - 1)! : ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
have rw₁ : Eq (α := ZMod p) (∏ i ∈ Ico 1 (p - 1 + 1), (↑i : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
Tactic: rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (-1)
have simp_rw : Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) x) (-1)
Tactic: simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
simp_rw : Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) x) (-1)
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (-1)
have simp_rw₁ : Eq (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) (∏ x : (ZMod p)ˣ, x)) (-1)
Tactic: simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
simp_rw : Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) x) (-1)
simp_rw₁ : Eq (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) (∏ x : (ZMod p)ˣ, x)) (-1)
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (-1)
have simp_rw₂ : Eq (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) (-1)) (-1)
Tactic: simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]