awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
this :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) (↑(S n) : Set E)
h_symm' : ∀ x ∈ S n, -x ∈ S n
x : ↥L
hx_nz : x ≠ 0
hx_mem : (↑x : E) ∈ (↑(S n) : Set E)
⊢ (Z n).Nonempty

Tactic:
exact ⟨x, hx_mem, by simp_all⟩
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
refine_2 :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) (↑(S n) : Set E)
⊢ (Z n).Nonempty

Tactic:
suffices μ F * 2 ^ finrank ℝ E < μ (S n : Set E) by
      have h_symm' : ∀ x ∈ S n, -x ∈ S n := by
        rintro _ ⟨y, hy, rfl⟩
        exact ⟨-y, h_symm _ hy, by simp⟩
      obtain ⟨x, hx_nz, hx_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
        fund h_symm' (S n).convex this
      exact ⟨x, hx_mem, by simp_all⟩
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) (↑(S n) : Set E)

Tactic:
lt_of_le_of_lt h ?_

Premises used: lt_of_le_of_lt
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
refine_2 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑(S n) : Set E) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) <
    (μ : (a : Set E) → ℝ≥0∞) (↑(S n) : Set E)

Tactic:
refine lt_of_le_of_lt h ?_

Premises used: lt_of_le_of_lt
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
refine_2 :
  (μ : (a : Set E) → ℝ≥0∞) s <
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑(S n) : Set E) : ℝ≥0∞)

Tactic:
rw [ConvexBody.coe_smul', NNReal.smul_def, addHaar_smul_of_nonneg _ (NNReal.coe_nonneg _)]

Premises used: NNReal.smul_def, MeasureTheory.Measure.addHaar_smul_of_nonneg, NNReal.coe_nonneg, ConvexBody.coe_smul'
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
rw rw₁ :
  (μ : (a : Set E) → ℝ≥0∞) s <
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
        ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞) ↔
    (μ : (a : Set E) → ℝ≥0∞) s <
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
        ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) s <
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
        ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞) ↔
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) <
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
        ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞)

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
refine_2 :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) s <
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞)

Tactic:
rw [show μ s < _ ↔ 1 * μ s < _ by rw [one_mul]]
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
refine_2 :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((1 + (↑(u n) : ℝ)) ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞)

Tactic:
dsimp [K]
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
refine_2 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2₁ : 1 < ENNReal.ofReal ((1 + (↑(u n) : ℝ)) ^ finrank ℝ E)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((1 + (↑(u n) : ℝ)) ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
gcongr
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
h_cpt.measure_ne_top

Premises used: IsCompact.measure_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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact h_cpt.measure_ne_top

Premises used: IsCompact.measure_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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
⊢ 0 ≤ 1 + (↑(u n) : ℝ)

Tactic:
positivity
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
refine_2 : 1 < ENNReal.ofReal (1 + (↑(u n) : ℝ)) ^ finrank ℝ E
⊢ 1 < ENNReal.ofReal ((1 + (↑(u n) : ℝ)) ^ finrank ℝ E)

Tactic:
rw [ofReal_pow (by positivity)]

Premises used: ENNReal.ofReal_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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal (1 + (↑(u n) : ℝ)) ^ finrank ℝ E

Tactic:
one_lt_pow₀ ?_ (ne_of_gt finrank_pos)

Premises used: ne_of_gt, one_lt_pow₀, Module.finrank_pos
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
refine_2 : 1 < ENNReal.ofReal (1 + (↑(u n) : ℝ))
⊢ 1 < ENNReal.ofReal (1 + (↑(u n) : ℝ)) ^ finrank ℝ E

Tactic:
refine one_lt_pow₀ ?_ (ne_of_gt finrank_pos)

Premises used: ne_of_gt, one_lt_pow₀, Module.finrank_pos
-- 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 : Nontrivial E
inst_6 : μ.IsAddHaarMeasure
L : AddSubgroup E
inst_7 : Countable.{u_1 + 1} ↥L
inst_8 : DiscreteTopology.{u_1} ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) 2 (finrank ℝ E)) ≤
    (μ : (a : Set E) → ℝ≥0∞) s
h_mes : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := Exists.choose (p := fun (u : ℕ → ℝ≥0) ↦ StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (nhds 0)) ⋯
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun (n : ℕ) ↦ (1 + u n) • K
Z : ℕ → Set E := fun (n : ℕ) ↦ (↑(S n) : Set E) ∩ ((↑L : Set E) \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed ((↑L : Set E) \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal (1 + (↑(u n) : ℝ))

Tactic:
simp [u, (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.2.1 n]

Premises used: Exists.choose_spec, exists_seq_strictAnti_tendsto, And.right, And.left, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableInv G
inst_4 : μ.IsInvInvariant
f : G → F
hf : Integrable f μ
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f t⁻¹) μ

Tactic:
(hf.mono_measure (map_inv_eq_self μ).le).comp_measurable measurable_inv

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.Integrable.comp_measurable, Eq.le, MeasurableInv.measurable_inv, MeasureTheory.Measure.map_inv_eq_self
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : Group G
inst_4 : MeasurableInv G
f : G → E
μ : Measure G
inst_5 : μ.IsInvInvariant
⊢ MeasurableEmbedding (β := G) fun (x : G) ↦ x⁻¹

Tactic:
have h : MeasurableEmbedding fun x : G => x⁻¹ := (MeasurableEquiv.inv G).measurableEmbedding
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : Group G
inst_4 : MeasurableInv G
f : G → E
μ : Measure G
inst_5 : μ.IsInvInvariant
h : MeasurableEmbedding (β := G) fun (x : G) ↦ x⁻¹
rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst (map (fun (x : G) ↦ x⁻¹) μ) fun (y : G) ↦ f y) (∫ (x : G), f x ∂μ)
rw₁ rw₂ : Eq.{u_5 + 1} (α := E) (∫ (y : G), f y ∂μ) (∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x⁻¹ ∂μ) (∫ (x : G), f x ∂μ)

Tactic:
rw [← h.integral_map, map_inv_eq_self]

Premises used: MeasurableEmbedding.integral_map, MeasureTheory.Measure.map_inv_eq_self