awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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)
⊢ (Z n).Nonempty
have h_symm' : ∀ x ∈ S n, -x ∈ S n
Tactic: have h_symm' : ∀ x ∈ S n, -x ∈ S n := by
        rintro _ ⟨y, hy, rfl⟩
        exact ⟨-y, h_symm _ hy, by simp⟩
-- 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 : 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
⊢ (Z n).Nonempty
have obtain : ∀ (x : ↥L) (hx_nz : x ≠ 0) (hx_mem : (↑x : E) ∈ (↑(S n) : Set E)), (Z n).Nonempty
Tactic: 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
-- 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 : 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 : ℕ
⊢ (Z n).Nonempty
have 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)
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⟩
-- 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 : 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)
have refine_2 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑(S n) : Set E) : ℝ≥0∞)
Tactic: refine lt_of_le_of_lt 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 : 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 : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑(S n) : Set E) : ℝ≥0∞)
have 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∞)
Tactic: rw [ConvexBody.coe_smul', NNReal.smul_def, addHaar_smul_of_nonneg _ (NNReal.coe_nonneg _)]
-- 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 : 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 : ℕ
⊢ (μ : (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∞)
have 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∞)
Tactic: rw [one_mul]
-- 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 : 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 : ℕ
⊢ (μ : (a : Set E) → ℝ≥0∞) s <
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal ((↑(1 + u n) : ℝ) ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞) (↑K : Set E) : ℝ≥0∞)
have 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∞)
Tactic: rw [show μ s < _ ↔ 1 * μ s < _ by rw [one_mul]]
-- 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 : 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∞) (β := ℝ≥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∞)
have 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∞)
Tactic: dsimp [K]
-- 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 : 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∞) (β := ℝ≥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∞)
have refine_2 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: gcongr
-- 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 : 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∞)
⊢ 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∞)
have refine_2₁ : 1 < ENNReal.ofReal ((1 + (↑(u n) : ℝ)) ^ finrank ℝ E)
Tactic: gcongr
-- 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 : 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)
have refine_2 : 1 < ENNReal.ofReal (1 + (↑(u n) : ℝ)) ^ finrank ℝ E
Tactic: rw [ofReal_pow (by positivity)]
-- 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 : 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
have refine_2 : 1 < ENNReal.ofReal (1 + (↑(u n) : ℝ))
Tactic: refine one_lt_pow₀ ?_ (ne_of_gt finrank_pos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (hypothesis)
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
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x⁻¹ ∂μ) (∫ (x : G), f x ∂μ)
have h : MeasurableEmbedding (β := G) fun (x : G) ↦ x⁻¹
Tactic: have h : MeasurableEmbedding fun x : G => x⁻¹ := (MeasurableEquiv.inv G).measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
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⁻¹
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x⁻¹ ∂μ) (∫ (x : G), f x ∂μ)
have rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst (map (fun (x : G) ↦ x⁻¹) μ) fun (y : G) ↦ f y) (∫ (x : G), f x ∂μ)
Tactic: rw [← h.integral_map, map_inv_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
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 ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x⁻¹ ∂μ) (∫ (x : G), f x ∂μ)
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (y : G), f y ∂μ) (∫ (x : G), f x ∂μ)
Tactic: rw [← h.integral_map, map_inv_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
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
s : Set G
hf : IntegrableOn f s μ
⊢ IntegrableOn.{u_4, u_6} (ε := F) (fun (x : G) ↦ f x⁻¹) s⁻¹ μ
have apply : @Integrable _ _ _ _ inst f (map (⇑(MeasurableEquiv.inv G) : (a : G) → G) (μ.restrict s⁻¹))
Tactic: apply (integrable_map_equiv (MeasurableEquiv.inv G) f).mp
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (hypothesis)
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
s : Set G
hf : IntegrableOn f s μ
⊢ @Integrable _ _ _ _ inst f (map (⇑(MeasurableEquiv.inv G) : (a : G) → G) (μ.restrict s⁻¹))
have this : s⁻¹ = (⇑(MeasurableEquiv.inv G) : (a : G) → G) ⁻¹' s
Tactic: have : s⁻¹ = MeasurableEquiv.inv G ⁻¹' s := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
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
s : Set G
hf : IntegrableOn f s μ
this : s⁻¹ = (⇑(MeasurableEquiv.inv G) : (a : G) → G) ⁻¹' s
⊢ @Integrable _ _ _ _ inst f (map (⇑(MeasurableEquiv.inv G) : (a : G) → G) (μ.restrict s⁻¹))
have rw : @Integrable _ _ _ _ inst f (Measure.restrict (map (⇑(MeasurableEquiv.inv G) : (a : G) → G) μ) s)
Tactic: rw [this, ← MeasurableEquiv.restrict_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (hypothesis)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
f : G → E
g : G
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (g * x) ∂μ) (∫ (x : G), f x ∂μ)
have h_mul : MeasurableEmbedding (β := G) fun (x : G) ↦ g * x
Tactic: have h_mul : MeasurableEmbedding fun x => g * x := (MeasurableEquiv.mulLeft g).measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding (β := G) fun (x : G) ↦ g * x
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (g * x) ∂μ) (∫ (x : G), f x ∂μ)
have rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst (map (fun (x : G) ↦ g * x) μ) fun (y : G) ↦ f y) (∫ (x : G), f x ∂μ)
Tactic: rw [← h_mul.integral_map, map_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding (β := G) fun (x : G) ↦ g * x
rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst (map (fun (x : G) ↦ g * x) μ) fun (y : G) ↦ f y) (∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (g * x) ∂μ) (∫ (x : G), f x ∂μ)
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (y : G), f y ∂μ) (∫ (x : G), f x ∂μ)
Tactic: rw [← h_mul.integral_map, map_mul_left_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (hypothesis)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
f : G → E
g : G
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x * g) ∂μ) (∫ (x : G), f x ∂μ)
have h_mul : MeasurableEmbedding (β := G) fun (x : G) ↦ x * g
Tactic: have h_mul : MeasurableEmbedding fun x => x * g :=
    (MeasurableEquiv.mulRight g).measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Integral (goal)
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding (β := G) fun (x : G) ↦ x * g
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x * g) ∂μ) (∫ (x : G), f x ∂μ)
have rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst (map (fun (x : G) ↦ x * g) μ) fun (y : G) ↦ f y) (∫ (x : G), f x ∂μ)
Tactic: rw [← h_mul.integral_map, map_mul_right_eq_self]