-- Mathlib/MeasureTheory/Group/AddCircle.lean
theorem isAddFundamentalDomain_of_ae_ball (I : Set <| AddCircle T) (u x : AddCircle T)
    (hu : IsOfFinAddOrder u) (hI : I =ᵐ[volume] ball x (T / (2 * addOrderOf u))) :
    IsAddFundamentalDomain (AddSubgroup.zmultiples u) I

Proof state:
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 / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ Finset.univ.card = addOrderOf u

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

Result:
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 / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ Finset.univ.card = Fintype.card ↥(AddSubgroup.zmultiples u)

Proof state:
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ IsAddFundamentalDomain (↥G) I volume

Tactic:
have hn : 1 ≤ (n : ℝ) := by norm_cast; linarith [hu.addOrderOf_pos]

Result:
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ IsAddFundamentalDomain (↥G) I volume

Proof state:
case refine_4
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 / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)

Tactic:
haveI : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples.to_subtype

Result:
case refine_4
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 / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ volume univ ≤ ∑' (g : ↥G), volume (g +ᵥ I)

Proof state:
case refine_4
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 / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : Finset.univ.card = n
⊢ 2 ≠ 0

Tactic:
exact two_ne_zero

Result:
no goals

Proof state:
case refine_3
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ ∀ (g : ↥G), QuasiMeasurePreserving (fun x => g +ᵥ x) volume volume

Tactic:
exact fun g => quasiMeasurePreserving_add_left (G := AddCircle T) volume g

Result:
no goals

Proof state:
case refine_2.mk.h
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑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) ?_)

Result:
case refine_2.mk.h
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ addOrderOf g ≤ n

Proof state:
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 / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ Finset.univ.card = n

Tactic:
show _ = addOrderOf u

Result:
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 / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ Finset.univ.card = addOrderOf u

Proof state:
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 volume] ball x (T / (2 * ↑n))
⊢ IsAddFundamentalDomain (↥G) I volume

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

Result:
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ IsAddFundamentalDomain (↥G) I volume

Proof state:
case refine_2.mk
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint volume (⟨g, hg⟩ +ᵥ I) I

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

Result:
case refine_2.mk
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint volume (g +ᵥ I) I

Proof state:
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 / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ 1 ≤ n

Tactic:
linarith [hu.addOrderOf_pos]

Result:
no goals