awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
refine_2 : Disjoint (g +ᵥ B) B
⊢ AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume (g +ᵥ I) I

Tactic:
refine AEDisjoint.congr (Disjoint.aedisjoint ?_)
      ((quasiMeasurePreserving_add_left volume (-g)).vadd_ae_eq_of_ae_eq g hI) hI

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq, MeasureTheory.quasiMeasurePreserving_add_left, MeasureTheory.MeasureSpace.volume, Disjoint.aedisjoint, Neg.neg, MeasureTheory.AEDisjoint.congr
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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})
rw₃ rw₄ : g +ᵥ B = g +ᵥ ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ g +ᵥ B = ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))

Tactic:
rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]

Premises used: add_comm, Metric.thickening_singleton, add_ball, singleton_add_ball
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))

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]
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))
refine_2 : Disjoint (ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))) B
⊢ Disjoint (g +ᵥ B) B

Tactic:
rw [hBg]
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))
refine_2 : T / HMul.hMul (α := ℝ) 2 (↑n : ℝ) + T / HMul.hMul (α := ℝ) 2 (↑n : ℝ) ≤ dist (g + x) x
⊢ Disjoint (ball (g + x) (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))) B

Tactic:
apply ball_disjoint_ball

Premises used: Metric.ball_disjoint_ball
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))
refine_2 : T ≤ n • ‖g‖
⊢ T / HMul.hMul (α := ℝ) 2 (↑n : ℝ) + T / HMul.hMul (α := ℝ) 2 (↑n : ℝ) ≤ dist (g + x) x

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]

Premises used: dist_eq_norm, nsmul_eq_mul, add_sub_cancel_right, div_mul_eq_div_div, div_le_iff₀', add_div, add_self_div_two
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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‖

Tactic:
(le_add_order_smul_norm_of_isOfFinAddOrder (hu.of_mem_zmultiples hg) hg').trans
      (nsmul_le_nsmul_left (norm_nonneg g) ?_)

Premises used: IsOfFinAddOrder.of_mem_zmultiples, nsmul_le_nsmul_left, AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder, LE.le.trans, norm_nonneg
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))
refine_2 : addOrderOf g ≤ n
⊢ T ≤ n • ‖g‖

Tactic:
refine (le_add_order_smul_norm_of_isOfFinAddOrder (hu.of_mem_zmultiples hg) hg').trans
      (nsmul_le_nsmul_left (norm_nonneg g) ?_)

Premises used: IsOfFinAddOrder.of_mem_zmultiples, nsmul_le_nsmul_left, AddCircle.le_add_order_smul_norm_of_isOfFinAddOrder, LE.le.trans, norm_nonneg
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))
⊢ addOrderOf g ≤ n

Tactic:
Nat.le_of_dvd (addOrderOf_pos_iff.mpr hu) (addOrderOf_dvd_of_mem_zmultiples hg)

Premises used: Iff.mpr, addOrderOf_dvd_of_mem_zmultiples, addOrderOf_pos_iff, Nat.le_of_dvd
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))
⊢ addOrderOf g ≤ n

Tactic:
exact Nat.le_of_dvd (addOrderOf_pos_iff.mpr hu) (addOrderOf_dvd_of_mem_zmultiples hg)

Premises used: Iff.mpr, addOrderOf_dvd_of_mem_zmultiples, addOrderOf_pos_iff, Nat.le_of_dvd
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ↥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:
fun g => quasiMeasurePreserving_add_left (G := AddCircle T) volume g

Premises used: MeasureTheory.quasiMeasurePreserving_add_left, MeasureTheory.MeasureSpace.volume, Subtype.val
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ↥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:
exact fun g => quasiMeasurePreserving_add_left (G := AddCircle T) volume g

Premises used: MeasureTheory.quasiMeasurePreserving_add_left, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ)
⊢ I =ᶠ[ae (F := Measure (AddCircle T)) volume] closedBall x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))

Tactic:
replace hI := hI.trans closedBall_ae_eq_ball.symm
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 : ℝ))
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∞)
⊢ 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
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
change : Finset.card (α := ↥G) Finset.univ = addOrderOf u
⊢ Finset.card (α := ↥G) Finset.univ = n

Tactic:
change _ = addOrderOf u

Premises used: addOrderOf
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
rw : Finset.card (α := ↥G) Finset.univ = Fintype.card ↥(AddSubgroup.zmultiples u)
⊢ Finset.card (α := ↥G) Finset.univ = addOrderOf u

Tactic:
rw [← Nat.card_zmultiples, Nat.card_eq_fintype_card]

Premises used: Nat.card_zmultiples, Nat.card_eq_fintype_card
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 = Fintype.card ↥(AddSubgroup.zmultiples u)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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 = n

Tactic:
have hG_card : #(Finset.univ : Finset G) = n := by
      change _ = addOrderOf u
      rw [← Nat.card_zmultiples, Nat.card_eq_fintype_card]; rfl
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
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∞)
⊢ 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:
simp_rw [measure_vadd]

Premises used: MeasureTheory.measure_vadd
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
refine_4 : Ne (α := ℝ) 2 0
⊢ 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:
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]

Premises used: AddCircle.measure_univ, mul_div, MeasureTheory.measure_congr, AddCircle.volume_closedBall, LT.lt.le, Ne.symm, div_le_self, mul_div_cancel₀, min_eq_right, zero_lt_one, ENNReal.ofReal_nsmul, tsum_fintype, nsmul_eq_mul, mul_div_mul_comm, one_mul, div_self, Fact.out, lt_of_lt_of_le, LT.lt.ne, Finset.sum_const
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
⊢ Ne (α := ℝ) 2 0

Tactic:
two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
⊢ Ne (α := ℝ) 2 0

Tactic:
exact two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
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∞)
⊢ (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
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
y : AddCircle T
hy : y ∈ G
⊢ Subtype.mk (p := fun (x : AddCircle T) ↦ x ∈ G) y hy +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s

Tactic:
(vadd_ae_eq_self_of_mem_zmultiples hs hy :)

Premises used: MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
y : AddCircle T
hy : y ∈ G
⊢ Subtype.mk (p := fun (x : AddCircle T) ↦ x ∈ G) y hy +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s

Tactic:
exact (vadd_ae_eq_self_of_mem_zmultiples hs hy :)

Premises used: MeasureTheory.vadd_ae_eq_self_of_mem_zmultiples
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
⊢ ∀ (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 :)
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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
hsG : ∀ (g : ↥G), g +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
rw :
  HSMul.hSMul (β := ℝ≥0∞) (Nat.card ↥(AddSubgroup.zmultiples u))
      (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
rw₁ rw₂ :
  HSMul.hSMul (β := ℝ≥0∞) (Nat.card ↥(AddSubgroup.zmultiples u))
      (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (Nat.card ↥(AddSubgroup.zmultiples u))
      ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) s =
    HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)

Tactic:
rw [(isAddFundamentalDomain_of_ae_ball I u x hu hI).measure_eq_card_smul_of_vadd_ae_eq_self s hsG,
    ← Nat.card_zmultiples u]

Premises used: AddCircle.isAddFundamentalDomain_of_ae_ball, Nat.card_zmultiples, MeasureTheory.IsAddFundamentalDomain.measure_eq_card_smul_of_vadd_ae_eq_self
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
f : α → M
inst_2 : MeasurableMul M
hf : Measurable f
c : M
⊢ Measurable.{u_3, u_2} (β := M) fun (x : α) ↦ c * f x

Tactic:
(measurable_const_mul c).comp hf

Premises used: Measurable.comp, MeasurableMul.measurable_const_mul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
f : α → M
μ : Measure α
inst_2 : MeasurableMul M
hf : AEMeasurable f μ
c : M
⊢ AEMeasurable.{u_3, u_2} (β := M) (fun (x : α) ↦ c * f x) μ

Tactic:
(MeasurableMul.measurable_const_mul c).comp_aemeasurable hf

Premises used: MeasurableMul.measurable_const_mul, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
f : α → M
inst_2 : MeasurableMul M
hf : Measurable f
c : M
⊢ Measurable.{u_3, u_2} (β := M) fun (x : α) ↦ f x * c

Tactic:
(measurable_mul_const c).comp hf

Premises used: Measurable.comp, MeasurableMul.measurable_mul_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
f : α → M
μ : Measure α
inst_2 : MeasurableMul M
hf : AEMeasurable f μ
c : M
⊢ AEMeasurable.{u_3, u_2} (β := M) (fun (x : α) ↦ f x * c) μ

Tactic:
(measurable_mul_const c).comp_aemeasurable hf

Premises used: MeasurableMul.measurable_mul_const, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
f g : α → M
inst_2 : MeasurableMul₂ M
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_3, u_2} (β := M) fun (a : α) ↦ f a * g a

Tactic:
measurable_mul.comp (hf.prodMk hg)

Premises used: MeasurableMul₂.measurable_mul, Measurable.comp, Measurable.prodMk
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
mβ : MeasurableSpace β
inst_2 : MeasurableMul₂ M
f g : α → β → M
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
dsimp : Measurable.{u_3, u_2} (β := M) fun (a : α) ↦ f a (h a) * g a (h a)
⊢ Measurable.{u_3, u_2} (β := M) fun (a : α) ↦ (f a * g a) (h a)

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
mβ : MeasurableSpace β
inst_2 : MeasurableMul₂ M
f g : α → β → M
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable.{u_3, u_2} (β := M) fun (a : α) ↦ f a (h a) * g a (h a)

Tactic:
fun_prop