awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.WellApproximable
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)

Tactic:
le_antisymm (μ.mono (subset_univ _)) ?_

Premises used: Set.subset_univ, MeasureTheory.OuterMeasure.mono, MeasureTheory.Measure.toOuterMeasure, le_antisymm
-- Module: Mathlib.NumberTheory.WellApproximable
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)
refine :
  LE.le (α := ENNReal) ((μ : (a : Set A) → ENNReal) univ : ENNReal)
    ((μ : (a : Set A) → ENNReal) (⋃ (i : (↑(Icc 0 n) : Type)), B i) : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (⋃ (i : (↑(Icc 0 n) : Type)), B i) : ENNReal)
    ((μ : (a : Set A) → ENNReal) univ : ENNReal)

Tactic:
refine le_antisymm (μ.mono (subset_univ _)) ?_

Premises used: Set.subset_univ, MeasureTheory.OuterMeasure.mono, MeasureTheory.Measure.toOuterMeasure, le_antisymm
-- Module: Mathlib.NumberTheory.WellApproximable
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)
simp_rw :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
⊢ LE.le (α := ENNReal) ((μ : (a : Set A) → ENNReal) univ : ENNReal)
    ((μ : (a : Set A) → ENNReal) (⋃ (i : (↑(Icc 0 n) : Type)), B i) : ENNReal)

Tactic:
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]

Premises used: Finset.card_univ, Fintype.card_Icc, Nat.card_Icc, MeasureTheory.measure_iUnion, tsub_zero, tsum_fintype, measurableSet_closedBall, MeasureTheory.Measure.addHaar_closedBall_center, Finset.sum_const
-- Module: Mathlib.NumberTheory.WellApproximable
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)
⊢ (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)

Tactic:
hδ
-- Module: Mathlib.NumberTheory.WellApproximable
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)
⊢ (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)

Tactic:
exact hδ
-- Module: Mathlib.NumberTheory.WellApproximable
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

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δ
-- Module: Mathlib.NumberTheory.WellApproximable
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
by_contra : ∀ (contra : ¬0 ≤ δ / 2), False
⊢ 0 ≤ δ / 2

Tactic:
by_contra contra
-- Module: Mathlib.NumberTheory.WellApproximable
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

Tactic:
(isOpen_univ.measure_pos μ univ_nonempty).not_ge <| hδ.trans ?_

Premises used: Set.univ_nonempty, IsOpen.measure_pos, isOpen_univ, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.NumberTheory.WellApproximable
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
refine : HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) ≤ 0
⊢ False

Tactic:
refine (isOpen_univ.measure_pos μ univ_nonempty).not_ge <| hδ.trans ?_

Premises used: Set.univ_nonempty, IsOpen.measure_pos, isOpen_univ, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.NumberTheory.WellApproximable
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
this : Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) (0 : ENNReal)
⊢ HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) ≤ 0

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.WellApproximable
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
suffices : Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) (0 : ENNReal)
⊢ HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) ≤ 0

Tactic:
suffices μ (closedBall 0 (δ / 2)) = 0 by simp [this]
-- Module: Mathlib.NumberTheory.WellApproximable
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.{u_1 + 1} (α := Set A) (closedBall 0 (δ / 2)) ∅

Tactic:
rw [not_le, ← closedBall_eq_empty (x := (0 : A))] at contra

Premises used: not_le, Metric.closedBall_eq_empty
-- Module: Mathlib.NumberTheory.WellApproximable
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 : Eq.{u_1 + 1} (α := Set A) (closedBall 0 (δ / 2)) ∅
⊢ Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal) (0 : ENNReal)

Tactic:
simp [contra]
-- Module: Mathlib.NumberTheory.WellApproximable
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

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]
-- Module: Mathlib.NumberTheory.WellApproximable
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
j : (↑(Icc 0 n) : Type)
rwa rwa₁ rwa₂ rwa₃ : 0 ≤ δ / 2
⊢ (B j).Nonempty

Tactic:
rwa [nonempty_closedBall]

Premises used: Metric.nonempty_closedBall
-- Module: Mathlib.NumberTheory.WellApproximable
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
⊢ ∀ (j : (↑(Icc 0 n) : Type)), (B j).Nonempty

Tactic:
have h'' : ∀ j, (B j).Nonempty := by intro j; rwa [nonempty_closedBall]
-- Module: Mathlib.NumberTheory.WellApproximable
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
h'' : ∀ (j : (↑(Icc 0 n) : Type)), (B j).Nonempty
⊢ n = 0

Tactic:
simpa using subsingleton_of_disjoint_isClosed_iUnion_eq_univ h'' h hB h'

Premises used: subsingleton_of_disjoint_isClosed_iUnion_eq_univ
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
hδ :
  (volume : (a : Set 𝕊) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1)
      ((volume : (a : Set 𝕊) → ENNReal) (closedBall 0 (T / (↑(n + 1) : ℝ) / 2)) : ENNReal)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ T / (↑(n + 1) : ℝ)

Tactic:
apply NormedAddCommGroup.exists_norm_nsmul_le (μ := volume) ξ hn

Premises used: NormedAddCommGroup.exists_norm_nsmul_le
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
T : ℝ
hT : Fact (0 < T)
ξ : 𝕊
n : ℕ
hn : 0 < n
⊢ LE.le (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.WellApproximable
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) : ℝ)))
hδ₆ hδ₇ : ENNReal.ofReal T ≤ ENNReal.ofReal T
⊢ (volume : (a : Set 𝕊) → ENNReal) univ ≤
    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)]

Premises used: AddCircle.measure_univ, AddCircle.volume_closedBall, LT.lt.le, div_le_self, mul_div_cancel₀, min_eq_right, two_ne_zero, ENNReal.ofReal_nsmul, nsmul_eq_mul, Fact.out
-- Module: Mathlib.NumberTheory.Wilson
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))
rw₁ rw₂ : Eq (α := ZMod p) (∏ i ∈ Ico 1 (p - 1 + 1), (↑i : 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))

Tactic:
rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]

Premises used: Finset.prod_Ico_id_eq_factorial, Finset.prod_natCast
-- Module: Mathlib.NumberTheory.Wilson
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)
simp_rw₂ : Eq (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) (-1)) (-1)
simp_rw₃ : Eq (α := ZMod p) (↑(-1) : ZMod p) (-1)
simp_rw₄ : Eq (α := ZMod p) (-(↑1 : ZMod p)) (-1)
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (-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]

Premises used: Units.coeHom, map_prod, ZMod, Units.val_neg, Units.val_one, Units.coeHom_apply, FiniteField.prod_univ_units_id_eq_neg_one
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ZMod :
  Eq (α := _root_.ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : _root_.ZMod p))
    (∏ x : (_root_.ZMod p)ˣ, (↑x : _root_.ZMod p))
⊢ Eq (α := _root_.ZMod p) (↑(p - 1)! : _root_.ZMod p) (-1)

Tactic:
refine
    calc
      ((p - 1)! : ZMod p) = ∏ x ∈ Ico 1 (succ (p - 1)), (x : ZMod p) := by
        rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
      _ = ∏ x : (ZMod p)ˣ, (x : ZMod p) := ?_
      _ = -1 := by
        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]

Premises used: HSub.hSub, Finset.Ico, Nat.cast, ZMod, Nat.factorial, OfNat.ofNat, Nat.succ
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ 0 < p

Tactic:
have hp : 0 < p := (Fact.out (p := p.Prime)).pos
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
symm : Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p)) (∏ x : (ZMod p)ˣ, (↑x : ZMod p))

Tactic:
symm
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))

Tactic:
prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_

Premises used: Units.val, Finset.prod_bij, ZMod.val
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
refine_1 :
  ∀ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ∈
      Ico 1 (p - 1).succ
refine_2 :
  ∀ (a₁ : (ZMod p)ˣ) (ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁) (a₂ : (ZMod p)ˣ)
    (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂
refine_3 :
  ∀ b ∈ Ico 1 (p - 1).succ,
    ∃ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
      (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = b
refine_4 :
  ∀ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (↑a : ZMod p) =
      (↑((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) : ZMod p)
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))

Tactic:
refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_

Premises used: Finset.prod_bij, ZMod.val
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
refine_1 :
  LE.le (α := ℕ) 1
      ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) ∧
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p
⊢ (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ∈
    Ico 1 (p - 1).succ

Tactic:
rw [mem_Ico, ← Nat.succ_sub hp, Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, Nat.succ_sub, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
refine_1 :
  LE.le (α := ℕ) 1 ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha)
refine_1₁ : (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p
⊢ LE.le (α := ℕ) 1
      ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) ∧
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
refine_1 :
  Ne (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) 0
⊢ LE.le (α := ℕ) 1 ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha)

Tactic:
apply Nat.pos_of_ne_zero

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
refine_1 :
  (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ≠ val (n := p) 0
⊢ Ne (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) 0

Tactic:
rw [← @val_zero p]

Premises used: ZMod.val_zero