awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 𝓕 ν
out : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
apply Fact.mk

Premises used: Fact.mk
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 𝓕 ν
⊢ covolume G α ν < ∞

Tactic:
Ne.lt_top h

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 𝓕 ν
h₁ : (ν : (a : Set α) → ℝ≥0∞) 𝓕 = covolume G α ν
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
convert! Ne.lt_top h

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 𝓕 ν
⊢ (ν : (a : Set α) → ℝ≥0∞) 𝓕 = covolume G α ν

Tactic:
(h𝓕.covolume_eq_volume ν).symm

Premises used: MeasureTheory.IsFundamentalDomain.covolume_eq_volume, Eq.symm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 𝓕 ν
⊢ (ν : (a : Set α) → ℝ≥0∞) 𝓕 = covolume G α ν

Tactic:
exact (h𝓕.covolume_eq_volume ν).symm

Premises used: MeasureTheory.IsFundamentalDomain.covolume_eq_volume, Eq.symm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞))

Tactic:
have : Fact (ν 𝓕 < ∞) := by
    apply Fact.mk
    convert! Ne.lt_top h
    exact (h𝓕.covolume_eq_volume ν).symm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 𝓕 ν
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) 𝓕 : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ IsFiniteMeasure (m0 := Quotient.instMeasurableSpace) (Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α ν < ∞
neg : ∀ (hasFun : ¬HasFundamentalDomain G α ν), covolume G α ν < ∞
⊢ covolume G α ν < ∞

Tactic:
by_cases hasFun : HasFundamentalDomain G α ν

Premises used: MeasureTheory.HasFundamentalDomain
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α ν
pos : ∀ (𝓕 : Set α) (h𝓕 : IsFundamentalDomain G 𝓕 ν), covolume G α ν < ∞
⊢ covolume G α ν < ∞

Tactic:
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain

Premises used: MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 𝓕 ν
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set (Quotient α_mod_G)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have H : μ univ < ∞ := IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' univ ∩ 𝓕) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [h𝓕.projection_respects_measure_apply (μ := μ) MeasurableSet.univ] at H

Premises used: MeasurableSet.univ, MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α) → ℝ≥0∞) (Quotient.mk α_mod_G ⁻¹' univ ∩ 𝓕) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ covolume G α ν < ∞

Tactic:
simpa [h𝓕.covolume_eq_volume ν] using H

Premises used: MeasureTheory.IsFundamentalDomain.covolume_eq_volume
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 α ν < ∞

Tactic:
simp [covolume, hasFun]
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasureSpace α
inst_3 : Countable G
inst_4 : @SMulInvariantMeasure G α _ MeasureSpace.toMeasurableSpace volume
inst_5 : MeasurableConstSMul G α
inst_6 : SigmaFinite.{u_3} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_7 : HasFundamentalDomain G α volume
μ : Measure (Quotient α_mod_G)
inst_8 : QuotientMeasureEqMeasurePreimage volume μ
⊢ SigmaFinite μ

Tactic:
QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient (ν := (volume : Measure α)) (μ := μ)

Premises used: MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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∞)
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∞)
⊢ ∃ (x : L) (y : L), x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)

Tactic:
contrapose! h
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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 : ∀ (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:
((fund.measure_eq_tsum _).trans (measure_iUnion₀
    (Pairwise.mono h fun i j hij => (hij.mono inf_le_left inf_le_left).aedisjoint)
      fun _ => (hS.vadd _).inter fund.nullMeasurableSet).symm).trans_le
      (measure_mono <| Set.iUnion_subset fun _ => Set.inter_subset_right)

Premises used: Set.iUnion_subset, MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet, MeasureTheory.measure_iUnion₀, Eq.trans_le, MeasureTheory.NullMeasurableSet.inter, MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum, Disjoint.aedisjoint, MeasureTheory.measure_mono, Disjoint.mono, inf_le_left, Eq.symm, MeasureTheory.NullMeasurableSet.vadd, Eq.trans, Set.inter_subset_right, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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 : ∀ (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:
exact ((fund.measure_eq_tsum _).trans (measure_iUnion₀
    (Pairwise.mono h fun i j hij => (hij.mono inf_le_left inf_le_left).aedisjoint)
      fun _ => (hS.vadd _).inter fund.nullMeasurableSet).symm).trans_le
      (measure_mono <| Set.iUnion_subset fun _ => Set.inter_subset_right)

Premises used: Set.iUnion_subset, MeasureTheory.IsAddFundamentalDomain.nullMeasurableSet, MeasureTheory.measure_iUnion₀, Eq.trans_le, MeasureTheory.NullMeasurableSet.inter, MeasureTheory.IsAddFundamentalDomain.measure_eq_tsum, Disjoint.aedisjoint, MeasureTheory.measure_mono, Disjoint.mono, inf_le_left, Eq.symm, MeasureTheory.NullMeasurableSet.vadd, Eq.trans, Set.inter_subset_right, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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
⊢ LE.le (α := ℝ) 0 2⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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
⊢ HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E) ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (HSMul.hSMul (α := ℝ) 2⁻¹ 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]

Premises used: Real, pow_ne_zero, two_ne_zero', ENNReal.ofReal_inv_of_pos, MeasureTheory.Measure.addHaar_smul_of_nonneg, ENNReal.mul_lt_mul_iff_left, mul_right_comm, zero_lt_two, ENNReal.ofReal_pow, Module.finrank
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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
⊢ 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:
simpa [← mul_pow, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]

Premises used: ENNReal.ofNat_ne_top, two_ne_zero, ENNReal.inv_mul_cancel, mul_pow
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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∞)

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]
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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∞)
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
⊢ ∃ (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

Premises used: Convex.smul, Convex.nullMeasurableSet, MeasureTheory.exists_pair_mem_lattice_not_disjoint_vadd
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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)
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
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s

Tactic:
obtain ⟨_, ⟨v, hv, rfl⟩, w, hw, hvw⟩ := Set.not_disjoint_iff.mp h

Premises used: Set.not_disjoint_iff, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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

Tactic:
⟨x - y, sub_ne_zero.2 hxy, ?_⟩

Premises used: Iff.mpr, sub_ne_zero, HSub.hSub, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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)
refine : (↑(x - y) : E) ∈ s
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s

Tactic:
refine ⟨x - y, sub_ne_zero.2 hxy, ?_⟩
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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)
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
⊢ (↑(x - y) : E) ∈ s

Tactic:
rw [Set.mem_inv_smul_set_iff₀ (two_ne_zero' ℝ)] at hv hw

Premises used: Real, Set.mem_inv_smul_set_iff₀, two_ne_zero'
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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)
⊢ 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

Premises used: sub_eq_sub_iff_add_eq_add, add_comm, AddSubgroup.coe_sub, AddSubgroup.vadd_def, vadd_eq_add
-- Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers
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 : w - v = (↑(x - y) : E)
rw : HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) 2 w) + HSMul.hSMul (α := ℝ) 2⁻¹ (-HSMul.hSMul (α := ℝ) 2 v) ∈ s
⊢ (↑(x - y) : E) ∈ s

Tactic:
rw [← hvw, ← inv_smul_smul₀ (two_ne_zero' ℝ) (_ - _), smul_sub, sub_eq_add_neg, smul_add]

Premises used: inv_smul_smul₀, Real, sub_eq_add_neg, HSub.hSub, smul_sub, two_ne_zero', smul_add