awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine_1 : ∀ (s : Set α) (fund_dom_s : IsFundamentalDomain G s ν),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: obtain ⟨s, fund_dom_s⟩ := i'
Cleared hypotheses: i'
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
Tactic: have : π ⁻¹' π '' (A n) = _ := MulAction.quotient_preimage_image_eq_union_mul (A n) (G := G)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
x : Setoid α := α_mod_G
⊢ MeasurableSet (Quotient.mk α_mod_G '' A n)
have rw : MeasurableSet.{u_3} (α := α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' A n)
Tactic: rw [measurableSet_quotient, Quotient.mk''_eq_mk, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
x : Setoid α := α_mod_G
⊢ MeasurableSet.{u_3} (α := α) (⋃ (g : G), (fun (x : α) ↦ g • x) '' A n)
have h : ∀ (b : G), MeasurableSet (α := α) ((fun (x : α) ↦ b • x) '' A n)
Tactic: apply MeasurableSet.iUnion
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
Tactic: have measπAn : MeasurableSet (π '' A n) := by
      let _ : Setoid α := α_mod_G
      rw [measurableSet_quotient, Quotient.mk''_eq_mk, this]
      apply MeasurableSet.iUnion
      exact fun g ↦ MeasurableSet.const_smul (hA_meas n) g
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) ((fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [fund_dom_s.projection_respects_measure_apply (μ := μ) measπAn, this, iUnion_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞)
Tactic: refine lt_of_le_of_lt ?_ (hA n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ (g : G), (fun (x : α) ↦ g • x) '' A n
measπAn : MeasurableSet (Quotient.mk α_mod_G '' A n)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (A n) : ℝ≥0∞)
have refine_1 : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : G), (fun (x : α) ↦ i • x) '' A n ∩ s) : ℝ≥0∞)
  (∑' (g : G), (ν : (a : Set α) → ℝ≥0∞) (g • A n ∩ s) : ℝ≥0∞)
Tactic: rw [fund_dom_s.measure_eq_tsum (A n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A i) : ℝ≥0∞) (∞ : ℝ≥0∞)
hA' : Eq.{u_3 + 1} (α := Set α) (⋃ (i : ℕ), A i) univ
⊢ Eq.{u_3 + 1} (α := Set (Quotient α_mod_G)) (⋃ (i : ℕ), (fun (n : ℕ) ↦ Quotient.mk α_mod_G '' A n) i) univ
have refine_2 : Quotient.mk α_mod_G '' univ = univ
Tactic: rw [← image_iUnion, hA']
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
⊢ IsFiniteMeasure μ
have obtain : ∀ (𝓕 : Set α) (h𝓕 : IsFundamentalDomain G 𝓕 ν), IsFiniteMeasure μ
Tactic: obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ IsFiniteMeasure μ
have rw : IsFiniteMeasure (m0 := Quotient.instMeasurableSpace) (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
Tactic: rw [h𝓕.projection_respects_measure (μ := μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞))
have out : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply Fact.mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
have h₁ : (ν : (a : Set α) → ℝ≥0∞) 𝓕 = covolume G α ν
Tactic: convert! Ne.lt_top h
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ IsFiniteMeasure (m0 := Quotient.instMeasurableSpace) (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))
have this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (ν 𝓕 < ∞) := by
    apply Fact.mk
    convert! Ne.lt_top h
    exact (h𝓕.covolume_eq_volume ν).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
inst_7 : IsFiniteMeasure μ
⊢ covolume G α ν < ∞
have pos : ∀ (hasFun : HasFundamentalDomain G α ν), covolume G α ν < ∞
Tactic: by_cases hasFun : HasFundamentalDomain G α ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
inst_7 : IsFiniteMeasure μ
pos : ∀ (hasFun : HasFundamentalDomain G α ν), covolume G α ν < ∞
⊢ covolume G α ν < ∞
have neg : ∀ (hasFun : ¬HasFundamentalDomain G α ν), covolume G α ν < ∞
Tactic: by_cases hasFun : HasFundamentalDomain G α ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
inst_7 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
⊢ covolume G α ν < ∞
have pos : ∀ (𝓕 : Set α) (h𝓕 : IsFundamentalDomain G 𝓕 ν), covolume G α ν < ∞
Tactic: obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
inst_7 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ covolume G α ν < ∞
have H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have H : μ univ < ∞ := IsFiniteMeasure.measure_univ_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
ν : Measure α
inst_3 : SMulInvariantMeasure G α ν
inst_4 : Countable G
inst_5 : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst_6 : QuotientMeasureEqMeasurePreimage ν μ
inst_7 : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ covolume G α ν < ∞
have H₁ : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' univ ∩ 𝓕) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [h𝓕.projection_respects_measure_apply (μ := μ) MeasurableSet.univ] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.GeometryOfNumbers (goal)
Goal:
E : Type u_1
L : Type u_2
inst : MeasurableSpace E
μ : Measure E
F s : Set E
inst_1 : AddGroup L
inst_2 : Countable L
inst_3 : AddAction L E
inst_4 : MeasurableSpace L
inst_5 : MeasurableVAdd L E
inst_6 : VAddInvariantMeasure L E μ
fund : IsAddFundamentalDomain L F μ
hS : NullMeasurableSet s μ
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∃ (x : L) (y : L), x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)
have contrapose! : ∀ (h : ∀ (x y : L) (_ : x ≠ y), Disjoint (x +ᵥ s) (y +ᵥ s)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.GeometryOfNumbers (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
F s : Set E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_6 : Countable.{u_1 + 1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) s
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 2⁻¹ s) : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
  HMul.hMul (β := ℝ≥0∞) ((ENNReal.ofReal 2)⁻¹ ^ finrank ℝ E * HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E))
    ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [addHaar_smul_of_nonneg μ (by simp : 0 ≤ (2 : ℝ)⁻¹) s,
      ← ENNReal.mul_lt_mul_iff_left (pow_ne_zero (finrank ℝ E) (two_ne_zero' _)) (by finiteness),
      mul_right_comm, ofReal_pow (by simp : 0 ≤ (2 : ℝ)⁻¹), ofReal_inv_of_pos zero_lt_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.GeometryOfNumbers (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
F s : Set E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_6 : Countable.{u_1 + 1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) s
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have h_vol : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 2⁻¹ s) : ℝ≥0∞)
Tactic: have h_vol : μ F < μ ((2⁻¹ : ℝ) • s) := by
    rw [addHaar_smul_of_nonneg μ (by simp : 0 ≤ (2 : ℝ)⁻¹) s,
      ← ENNReal.mul_lt_mul_iff_left (pow_ne_zero (finrank ℝ E) (two_ne_zero' _)) (by finiteness),
      mul_right_comm, ofReal_pow (by simp : 0 ≤ (2 : ℝ)⁻¹), ofReal_inv_of_pos zero_lt_two]
    simpa [← mul_pow, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.GeometryOfNumbers (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
F s : Set E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_6 : Countable.{u_1 + 1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) s
h_vol :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 2⁻¹ s) : ℝ≥0∞)
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have obtain : ∀ (x y : ↥L) (hxy : x ≠ y) (h : ¬Disjoint (x +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s) (y +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s)),
  ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
Tactic: obtain ⟨x, y, hxy, h⟩ :=
    exists_pair_mem_lattice_not_disjoint_vadd fund ((h_conv.smul _).nullMeasurableSet _) h_vol
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.GeometryOfNumbers (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
F s : Set E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_6 : Countable.{u_1 + 1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_1 :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) s
h_vol :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 2⁻¹ s) : ℝ≥0∞)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s) (y +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s)
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have obtain : ∀ (v : E) (hv : v ∈ HSMul.hSMul (α := ℝ) 2⁻¹ s) (w : E) (hw : w ∈ HSMul.hSMul (α := ℝ) 2⁻¹ s)
  (hvw : Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ y +ᵥ x) w) ((fun (x_1 : E) ↦ x +ᵥ x_1) v)),
  ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
Tactic: obtain ⟨_, ⟨v, hv, rfl⟩, w, hw, hvw⟩ := Set.not_disjoint_iff.mp h
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.GeometryOfNumbers (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
F s : Set E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_6 : Countable.{u_1 + 1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_1 :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) s
h_vol :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 2⁻¹ s) : ℝ≥0∞)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s) (y +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s)
v : E
hv : v ∈ HSMul.hSMul (α := ℝ) 2⁻¹ s
w : E
hw : w ∈ HSMul.hSMul (α := ℝ) 2⁻¹ s
hvw : Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ y +ᵥ x) w) ((fun (x_1 : E) ↦ x +ᵥ x_1) v)
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have refine : (↑(x - y) : E) ∈ s
Tactic: refine ⟨x - y, sub_ne_zero.2 hxy, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.GeometryOfNumbers (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
F s : Set E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_6 : Countable.{u_1 + 1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_1 :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) s
h_vol :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 2⁻¹ s) : ℝ≥0∞)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s) (y +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s)
v : E
hv : v ∈ HSMul.hSMul (α := ℝ) 2⁻¹ s
w : E
hw : w ∈ HSMul.hSMul (α := ℝ) 2⁻¹ s
hvw : Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ y +ᵥ x) w) ((fun (x_1 : E) ↦ x +ᵥ x_1) v)
⊢ (↑(x - y) : E) ∈ s
have rw : ∀ (hv : HSMul.hSMul (α := ℝ) 2 v ∈ s) (w : E) (hw : HSMul.hSMul (α := ℝ) 2 w ∈ s)
  (hvw : Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ y +ᵥ x) w) ((fun (x_1 : E) ↦ x +ᵥ x_1) v)), (↑(x - y) : E) ∈ s
Tactic: rw [Set.mem_inv_smul_set_iff₀ (two_ne_zero' ℝ)] at hv hw
Cleared hypotheses: hv, w, hw, hvw
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.GeometryOfNumbers (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
μ : Measure E
F s : Set E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_6 : Countable.{u_1 + 1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_1 :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) s
h_vol :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 2⁻¹ s) : ℝ≥0∞)
x y : ↥L
hxy : x ≠ y
h : ¬Disjoint (x +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s) (y +ᵥ HSMul.hSMul (α := ℝ) 2⁻¹ s)
v : E
hv : HSMul.hSMul (α := ℝ) 2 v ∈ s
w : E
hw : HSMul.hSMul (α := ℝ) 2 w ∈ s
hvw : Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ y +ᵥ x) w) ((fun (x_1 : E) ↦ x +ᵥ x_1) v)
⊢ (↑(x - y) : E) ∈ s
have hvw₁ : w - v = (↑(x - y) : E)
Tactic: simp_rw [AddSubgroup.vadd_def, vadd_eq_add, add_comm _ w, ← sub_eq_sub_iff_add_eq_add, ←
    AddSubgroup.coe_sub] at hvw
Cleared hypotheses: hvw