awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
tfae_6_to_7 :
  ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ
tfae_7_to_4 :
  ∀ (a : ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ) (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_4_to_5 :
  ∀
    (a :
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (c : G) (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_5_to_3 :
  ∀
    (a :
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (c : G) (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_3_to_2 :
  ∀
    (a :
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (c : G) (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ [SMulInvariantMeasure G α μ,
      ∀ (c : G) (s : Set α),
        MeasurableSet s →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : MeasurableConstSMul G α
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ NullMeasurableSet (c • s) μ

Tactic:
simpa only [← preimage_smul_inv] using
    hs.preimage (measurePreserving_smul _ _).quasiMeasurePreserving

Premises used: MeasureTheory.NullMeasurableSet.preimage, Set.preimage_smul_inv, MeasureTheory.measurePreserving_smul, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
K U : Set α
hK : IsCompact K
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
hU : IsOpen[inst_3] U
hne : U.Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, g • U
hμU : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
x : G
h : x ∈ (↑t : Set G)
rwa rwa₁ rwa₂ rwa₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (x • U) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [measure_smul]

Premises used: MeasureTheory.measure_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
hU : IsOpen[inst_3] U
hne : U.Nonempty
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
g : G
hg : g • x ∈ U
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ g • x) ⁻¹' U) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [measure_preimage_smul]

Premises used: MeasureTheory.measure_preimage_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
inst_6 : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst_3] U
hne : U.Nonempty
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
let ⟨_K, hK, hμK⟩ := Regular.exists_isCompact_not_null.mpr hμ
  measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero G hK hμK hU hne

Premises used: Iff.mpr, _private.0.MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero.match_1, MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_compact_ne_zero, LT.lt, OfNat.ofNat, MeasureTheory.Measure.Regular.exists_isCompact_not_null, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
inst_6 : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst_3] U
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ↔ U.Nonempty

Tactic:
⟨fun h => nonempty_of_measure_ne_zero h.ne',
    measure_isOpen_pos_of_smulInvariant_of_ne_zero G hμ hU⟩

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, LT.lt.ne', Iff.intro, MeasureTheory.measure_isOpen_pos_of_smulInvariant_of_ne_zero
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
inst_6 : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst_3] U
rw : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
rw₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
rw₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ↔ ¬U = ∅
rw₃ : U.Nonempty ↔ ¬U = ∅
rw₄ rw₅ : U ≠ ∅ ↔ ¬U = ∅
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅

Tactic:
rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero,
    measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]

Premises used: not_iff_not, Ne, MeasureTheory.measure_pos_iff_nonempty_of_smulInvariant, Set.nonempty_iff_ne_empty, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
inl : ∀ (hε : ε ≤ 0), closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
inr : ∀ (hε : 0 < ε), closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
⊢ closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε

Tactic:
rcases le_or_gt ε 0 with hε | hε

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
linarith : T < 2 * ε → 2 * (ε - 0) + (T - 2 * ε) + (0 - T) = 0
linarith₁ : T < 2 * ε → GT.gt (α := ℝ) 2 0
⊢ 2 * ε ≤ T

Tactic:
linarith [hT.out]

Premises used: Fact.out
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
inl : 2 * ε ≤ 0
⊢ closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε

Tactic:
rw [ball_eq_empty.mpr hε, ae_eq_empty, volume_closedBall,
      min_eq_right (by linarith [hT.out] : 2 * ε ≤ T), ENNReal.ofReal_eq_zero]

Premises used: Iff.mpr, ENNReal.ofReal_eq_zero, AddCircle.volume_closedBall, MeasureTheory.ae_eq_empty, min_eq_right, Metric.ball_eq_empty
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos zero_le_two hε

Premises used: mul_nonpos_of_nonneg_of_nonpos, zero_le_two
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos zero_le_two hε

Premises used: mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
inr :
  LE.le (α := ℝ≥0∞) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
    ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (ball x ε) : ℝ≥0∞)
⊢ closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε

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
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
simp_rw : Tendsto (fun (δ : ℝ) ↦ ENNReal.ofReal (min T (2 * δ))) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))
⊢ Tendsto (β := ℝ≥0∞) (fun (δ : ℝ) ↦ ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x δ) : ℝ≥0∞)) (𝓝[<] ε)
    (𝓝 ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε)) : Filter ℝ≥0∞)

Tactic:
simp_rw [volume_closedBall]

Premises used: AddCircle.volume_closedBall
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (δ : ℝ) ↦ ENNReal.ofReal (min T (2 * δ))) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))

Tactic:
ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)

Premises used: tendsto_const_nhds, Filter.Tendsto.const_mul, ENNReal.tendsto_ofReal, Filter.Tendsto.min
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
refine : Tendsto (fun (x : ℝ) ↦ x) (𝓝[<] ε) (𝓝 ε)
⊢ Tendsto (fun (δ : ℝ) ↦ ENNReal.ofReal (min T (2 * δ))) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))

Tactic:
refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)

Premises used: tendsto_const_nhds, Filter.Tendsto.const_mul, ENNReal.tendsto_ofReal, Filter.Tendsto.min
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (x : ℝ) ↦ x) (𝓝[<] ε) (𝓝 ε)

Tactic:
nhdsWithin_le_nhds

Premises used: Set.Mem, setOf, nhdsWithin_le_nhds, Set.preimage, Filter.Tendsto
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun (x : ℝ) ↦ x) (𝓝[<] ε) (𝓝 ε)

Tactic:
exact nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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∞)

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
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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∞)

Tactic:
le_of_tendsto this <| mem_of_superset (Ioo_mem_nhdsLT hε) fun r hr ↦ ?_

Premises used: le_of_tendsto, Ioo_mem_nhdsLT, Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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∞)
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
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
    ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (ball x ε) : ℝ≥0∞)

Tactic:
refine le_of_tendsto this <| mem_of_superset (Ioo_mem_nhdsLT hε) fun r hr ↦ ?_

Premises used: le_of_tendsto, Ioo_mem_nhdsLT, Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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∞)
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:
measure_mono (closedBall_subset_ball hr.2)

Premises used: Set.Mem, setOf, Metric.closedBall_subset_ball, And.right, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Group.AddCircle
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∞)
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:
exact measure_mono (closedBall_subset_ball hr.2)

Premises used: Metric.closedBall_subset_ball, And.right, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf u) : ℝ))
set :
  let G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u;
  IsAddFundamentalDomain (↥G) I (volume : Measure (AddCircle T))
⊢ IsAddFundamentalDomain (↥(AddSubgroup.zmultiples u)) I (volume : Measure (AddCircle T))

Tactic:
set G := AddSubgroup.zmultiples u

Premises used: AddSubgroup.zmultiples
-- Module: Mathlib.MeasureTheory.Group.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf u) : ℝ))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ let n := addOrderOf u;
  I =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))

Tactic:
set n := 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
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ let B := ball x (T / HMul.hMul (α := ℝ) 2 (↑n : ℝ));
  I =ᶠ[ae (F := Measure (AddCircle T)) volume] B

Tactic:
set B := ball x (T / (2 * n))

Premises used: HMul.hMul, HDiv.hDiv, Metric.ball, Nat.cast, OfNat.ofNat
-- 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
norm_cast : 1 ≤ n
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
norm_cast
-- 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
linarith : n < 1 → -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) + (HAdd.hAdd (α := ℤ) 0 1 - (↑(addOrderOf u) : ℤ)) = 0
⊢ 1 ≤ n

Tactic:
linarith [hu.addOrderOf_pos]

Premises used: IsOfFinAddOrder.addOrderOf_pos
-- 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
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
have hn : 1 ≤ (n : ℝ) := by norm_cast; linarith [hu.addOrderOf_pos]
-- 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 : ℝ)
⊢ IsAddFundamentalDomain (↥G) I (volume : Measure (AddCircle T))

Tactic:
IsAddFundamentalDomain.mk_of_measure_univ_le ?_ ?_ ?_ ?_

Premises used: MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le, Set.Mem
-- 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 : ℝ)
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))
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∞)
⊢ IsAddFundamentalDomain (↥G) I (volume : Measure (AddCircle T))

Tactic:
refine IsAddFundamentalDomain.mk_of_measure_univ_le ?_ ?_ ?_ ?_

Premises used: MeasureTheory.IsAddFundamentalDomain.mk_of_measure_univ_le
-- 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 : ℝ)
⊢ NullMeasurableSet I (volume : Measure (AddCircle T))

Tactic:
measurableSet_ball.nullMeasurableSet.congr hI.symm

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.congr, measurableSet_ball, Filter.EventuallyEq.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 : ℝ))
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] B
hn : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ NullMeasurableSet I (volume : Measure (AddCircle T))

Tactic:
exact measurableSet_ball.nullMeasurableSet.congr hI.symm

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.NullMeasurableSet.congr, measurableSet_ball, Filter.EventuallyEq.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 : ℝ))
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
⊢ g ≠ 0

Tactic:
simpa only [Ne, AddSubgroup.mk_eq_zero] using hg'

Premises used: Ne, AddSubgroup.mk_eq_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 : ℝ))
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
⊢ g ≠ 0

Tactic:
replace hg' : g ≠ 0 := by simpa only [Ne, AddSubgroup.mk_eq_zero] using hg'
-- 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 : AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume (g +ᵥ I) I
⊢ AEDisjoint (m := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples T)) (volume : Measure (AddCircle T))
    (Subtype.mk (p := fun (x : AddCircle T) ↦ x ∈ G) g hg +ᵥ I) I

Tactic:
change AEDisjoint volume (g +ᵥ I) I

Premises used: MeasureTheory.AEDisjoint, HVAdd.hVAdd, 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 : ℝ)
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume (g +ᵥ I) I

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