awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
have inr : LE.le (α := ℝ≥0∞) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
  ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (ball x ε) : ℝ≥0∞)
Tactic: suffices volume (closedBall x ε) ≤ volume (ball x ε) from
      (ae_eq_of_subset_of_measure_ge ball_subset_closedBall this
        measurableSet_ball.nullMeasurableSet (measure_ne_top _ _)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x δ) : ℝ≥0∞)) (𝓝[<] ε)
    (𝓝 ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε)) : Filter ℝ≥0∞)
have simp_rw : Tendsto (fun (δ : ℝ) ↦ ENNReal.ofReal (min T (2 * δ))) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))
Tactic: simp_rw [volume_closedBall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (δ : ℝ) ↦ ENNReal.ofReal (min T (2 * δ))) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))
have refine : Tendsto (fun (x : ℝ) ↦ x) (𝓝[<] ε) (𝓝 ε)
Tactic: refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
    ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (ball x ε) : ℝ≥0∞)
have this : Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x δ) : ℝ≥0∞)) (𝓝[<] ε)
  (𝓝 ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε)) : Filter ℝ≥0∞)
Tactic: have : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 <| volume (closedBall x ε)) := by
      simp_rw [volume_closedBall]
      refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)
      exact nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this :
  Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x δ) : ℝ≥0∞)) (𝓝[<] ε)
    (𝓝 ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε)) : Filter ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
    ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (ball x ε) : ℝ≥0∞)
have inr : ∀ (r : ℝ) (hr : r ∈ Ioo 0 ε),
  Membership.mem (γ := Set ℝ)
    {x_1 : ℝ |
      (fun (c : ℝ) ↦
          LE.le (α := ℝ≥0∞) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x c) : ℝ≥0∞)
            ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (ball x ε) : ℝ≥0∞))
        x_1}
    r
Tactic: refine le_of_tendsto this <| mem_of_superset (Ioo_mem_nhdsLT hε) fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)
have norm_cast : 1 ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
⊢ 1 ≤ n
have linarith : n < 1 → -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) + (HAdd.hAdd (α := ℤ) 0 1 - (↑(addOrderOf u) : ℤ)) = 0
Tactic: linarith [hu.addOrderOf_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
⊢ IsAddFundamentalDomain (↥G) I (volume : Measure (AddCircle T))
have hn : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: have hn : 1 ≤ (n : ℝ) := by norm_cast; linarith [hu.addOrderOf_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ IsAddFundamentalDomain (↥G) I (volume : Measure (AddCircle T))
have refine_1 : NullMeasurableSet I (volume : Measure (AddCircle T))
Tactic: refine IsAddFundamentalDomain.mk_of_measure_univ_le ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
refine_1 : NullMeasurableSet I (volume : Measure (AddCircle T))
⊢ IsAddFundamentalDomain (↥G) I (volume : Measure (AddCircle T))
have refine_2 : ∀ (g : ↥G),
  g ≠ 0 →
    AEDisjoint (m := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (volume : Measure (AddCircle T))
      (g +ᵥ I) I
Tactic: refine IsAddFundamentalDomain.mk_of_measure_univ_le ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
refine_1 : NullMeasurableSet I (volume : Measure (AddCircle T))
refine_2 :
  ∀ (g : ↥G),
    g ≠ 0 →
      AEDisjoint (m := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (volume : Measure (AddCircle T))
        (g +ᵥ I) I
⊢ IsAddFundamentalDomain (↥G) I (volume : Measure (AddCircle T))
have refine_3 : ∀ (g : ↥G),
  QuasiMeasurePreserving (β := AddCircle T) (mβ := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (m0 :=
    QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (fun (x : AddCircle T) ↦ g +ᵥ x)
    (volume : Measure (AddCircle T)) (volume : Measure (AddCircle T))
Tactic: refine IsAddFundamentalDomain.mk_of_measure_univ_le ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
refine_1 : NullMeasurableSet I (volume : Measure (AddCircle T))
refine_2 :
  ∀ (g : ↥G),
    g ≠ 0 →
      AEDisjoint (m := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (volume : Measure (AddCircle T))
        (g +ᵥ I) I
refine_3 :
  ∀ (g : ↥G),
    QuasiMeasurePreserving (β := AddCircle T) (mβ := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (m0 :=
      QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (fun (x : AddCircle T) ↦ g +ᵥ x)
      (volume : Measure (AddCircle T)) (volume : Measure (AddCircle T))
⊢ IsAddFundamentalDomain (↥G) I (volume : Measure (AddCircle T))
have refine_4 : LE.le (α := ℝ≥0∞) (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞)
  (∑' (g : ↥G), ((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (g +ᵥ I) : ℝ≥0∞)
Tactic: refine IsAddFundamentalDomain.mk_of_measure_univ_le ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : Subtype.mk (p := fun (x : AddCircle T) ↦ x ∈ G) g hg ≠ 0
⊢ AEDisjoint (m := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (volume : Measure (AddCircle T))
    (Subtype.mk (p := fun (x : AddCircle T) ↦ x ∈ G) g hg +ᵥ I) I
have hg'₁ : g ≠ 0
Tactic: replace hg' : g ≠ 0 := by simpa only [Ne, AddSubgroup.mk_eq_zero] using hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint (m := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (volume : Measure (AddCircle T))
    (Subtype.mk (p := fun (x : AddCircle T) ↦ x ∈ G) g hg +ᵥ I) I
have refine_2 : AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume (g +ᵥ I) I
Tactic: change AEDisjoint volume (g +ᵥ I) I
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume (g +ᵥ I) I
have refine_2 : Disjoint (g +ᵥ B) B
Tactic: refine AEDisjoint.congr (Disjoint.aedisjoint ?_)
      ((quasiMeasurePreserving_add_left volume (-g)).vadd_ae_eq_of_ae_eq g hI) hI
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
have rw : g +ᵥ B = ball (x + g) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
Tactic: rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
rw : g +ᵥ B = ball (x + g) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
have rw₁ : g +ᵥ B = {x} + ball g (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
Tactic: rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
rw : g +ᵥ B = ball (x + g) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
rw₁ : g +ᵥ B = {x} + ball g (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
have rw₂ : g +ᵥ B = HVAdd.hVAdd (β := Set (AddCircle T)) g (thickening (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) {x})
Tactic: rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
rw : g +ᵥ B = ball (x + g) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
rw₁ : g +ᵥ B = {x} + ball g (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
rw₂ : g +ᵥ B = HVAdd.hVAdd (β := Set (AddCircle T)) g (thickening (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) {x})
⊢ g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
have rw₃ : g +ᵥ B = g +ᵥ ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
Tactic: rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ Disjoint (g +ᵥ B) B
have hBg : g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
Tactic: have hBg : g +ᵥ B = ball (g + x) (T / (2 * n)) := by
      rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ Disjoint (g +ᵥ B) B
have refine_2 : Disjoint (ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))) B
Tactic: rw [hBg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ Disjoint (ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))) B
have refine_2 : T / HMul.hMul (α := ℝ) 2 (↑n : ℝ) + T / HMul.hMul (α := ℝ) 2 (↑n : ℝ) ≤ dist (g + x) x
Tactic: apply ball_disjoint_ball
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ T / HMul.hMul (α := ℝ) 2 (↑n : ℝ) + T / HMul.hMul (α := ℝ) 2 (↑n : ℝ) ≤ dist (g + x) x
have refine_2 : T ≤ n • ‖g‖
Tactic: rw [dist_eq_norm, add_sub_cancel_right, div_mul_eq_div_div, ← add_div, ← add_div,
      add_self_div_two, div_le_iff₀' (by positivity : 0 < (n : ℝ)), ← nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ T ≤ n • ‖g‖
have refine_2 : addOrderOf g ≤ n
Tactic: refine (le_add_order_smul_norm_of_isOfFinAddOrder (hu.of_mem_zmultiples hg) hg').trans
      (nsmul_le_nsmul_left (norm_nonneg g) ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ LE.le (α := ℝ≥0∞) (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑' (g : ↥G), ((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (g +ᵥ I) : ℝ≥0∞)
have hI₁ : I =ᶠ[ae (F := Measure (AddCircle T)) volume] closedBall x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
Tactic: replace hI := hI.trans closedBall_ae_eq_ball.symm
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] closedBall x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ LE.le (α := ℝ≥0∞) (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑' (g : ↥G), ((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (g +ᵥ I) : ℝ≥0∞)
have refine_4 : ∀ (this : Fintype ↥G),
  LE.le (α := ℝ≥0∞) (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑' (g : ↥G), ((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (g +ᵥ I) : ℝ≥0∞)
Tactic: haveI : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] closedBall x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
this : Fintype ↥G
⊢ Finset.card (α := ↥G) Finset.univ = addOrderOf u
have rw : Finset.card (α := ↥G) Finset.univ = Fintype.card ↥(AddSubgroup.zmultiples u)
Tactic: rw [← Nat.card_zmultiples, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] closedBall x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
this : Fintype ↥G
⊢ LE.le (α := ℝ≥0∞) (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑' (g : ↥G), ((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (g +ᵥ I) : ℝ≥0∞)
have hG_card : Finset.card (α := ↥G) Finset.univ = n
Tactic: have hG_card : #(Finset.univ : Finset G) = n := by
      change _ = addOrderOf u
      rw [← Nat.card_zmultiples, Nat.card_eq_fintype_card]; rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] closedBall x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
this : Fintype ↥G
hG_card : Finset.card (α := ↥G) Finset.univ = n
⊢ LE.le (α := ℝ≥0∞) (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑' (g : ↥G), ((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (g +ᵥ I) : ℝ≥0∞)
have refine_4 : LE.le (α := ℝ≥0∞) (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞)
  (∑' (g : ↥G), (volume : (a : Set (AddCircle T)) → ℝ≥0∞) I : ℝ≥0∞)
Tactic: simp_rw [measure_vadd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] closedBall x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
this : Fintype ↥G
hG_card : Finset.card (α := ↥G) Finset.univ = n
⊢ LE.le (α := ℝ≥0∞) (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑' (g : ↥G), (volume : (a : Set (AddCircle T)) → ℝ≥0∞) I : ℝ≥0∞)
have refine_4 : Ne (α := ℝ) 2 0
Tactic: rw [AddCircle.measure_univ, tsum_fintype, Finset.sum_const, measure_congr hI,
      volume_closedBall, ← ENNReal.ofReal_nsmul, mul_div, mul_div_mul_comm,
      div_self, one_mul, min_eq_right (div_le_self hT.out.le hn), hG_card,
      nsmul_eq_mul, mul_div_cancel₀ T (lt_of_lt_of_le zero_lt_one hn).ne.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf u) : ℝ))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) s =
    HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
have haveI : ∀ (this : Fintype ↥G),
  (volume : (a : Set (AddCircle T)) → ℝ≥0∞) s =
    HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
Tactic: haveI : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples.to_subtype
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf u) : ℝ))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype ↥G
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) s =
    HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
have hsG : ∀ (g : ↥G), g +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
Tactic: have hsG : ∀ g : G, (g +ᵥ s : Set <| AddCircle T) =ᵐ[volume] s := by
    rintro ⟨y, hy⟩; exact (vadd_ae_eq_self_of_mem_zmultiples hs hy :)