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
⊢ ∃ (U : Set E), IsOpen U ∧ U ∩ (↑L : Set E) = {0}

Tactic:
isOpen_inter_eq_singleton_of_mem_discrete ⟨inferInstance⟩ (zero_mem L)

Premises used: inferInstance, IsDiscrete.mk, ZeroMemClass.zero_mem, isOpen_inter_eq_singleton_of_mem_discrete
-- 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
⊢ ∃ (U : Set E), IsOpen U ∧ U ∩ (↑L : Set E) = {0}

Tactic:
exact isOpen_inter_eq_singleton_of_mem_discrete ⟨inferInstance⟩ (zero_mem L)

Premises used: inferInstance, IsDiscrete.mk, ZeroMemClass.zero_mem, isOpen_inter_eq_singleton_of_mem_discrete
-- 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
⊢ IsClosed ((↑L : Set E) \ {0})

Tactic:
have h_clos : IsClosed ((L : Set E) \ {0}) := by
    rsuffices ⟨U, hU⟩ : ∃ U : Set E, IsOpen U ∧ U ∩ L = {0}
    · rw [sdiff_eq_sdiff_iff_inf_eq_inf (z := U).mpr (by simp [Set.inter_comm .. ▸ hU.2, zero_mem])]
      exact AddSubgroup.isClosed_of_discrete.sdiff hU.1
    exact isOpen_inter_eq_singleton_of_mem_discrete ⟨inferInstance⟩ (zero_mem L)
-- 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})
⊢ Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)

Tactic:
IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed Z (fun n => ?_)
    (fun n => ?_) ((S 0).isCompact.inter_right h_clos) (fun n => (S n).isClosed.inter h_clos)

Premises used: IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed, ConvexBody.isClosed, ConvexBody.isCompact, IsCompact.inter_right, IsClosed.inter, OfNat.ofNat
-- 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})
refine_1 : ∀ (n : ℕ), Z (n + 1) ⊆ Z n
refine_2 : ∀ (n : ℕ), (Z n).Nonempty
⊢ Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)

Tactic:
refine IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed Z (fun n => ?_)
    (fun n => ?_) ((S 0).isCompact.inter_right h_clos) (fun n => (S n).isClosed.inter h_clos)

Premises used: IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed, ConvexBody.isClosed, ConvexBody.isCompact, IsCompact.inter_right, IsClosed.inter, OfNat.ofNat
-- 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 : ℕ
⊢ Z (n + 1) ⊆ Z n

Tactic:
Set.inter_subset_inter_left _ (SetLike.coe_subset_coe.mpr ?_)

Premises used: Iff.mpr, Set.inter_subset_inter_left, SetLike.coe_subset_coe
-- 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_1 : S (n + 1) ≤ S n
⊢ Z (n + 1) ⊆ Z n

Tactic:
refine Set.inter_subset_inter_left _ (SetLike.coe_subset_coe.mpr ?_)

Premises used: Iff.mpr, Set.inter_subset_inter_left, SetLike.coe_subset_coe
-- 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 : ℕ
⊢ S (n + 1) ≤ S n

Tactic:
ConvexBody.smul_le_of_le K h_zero ?_

Premises used: Set.Mem, ConvexBody.smul_le_of_le
-- 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_1 : 1 + u (n + 1) ≤ 1 + u n
⊢ S (n + 1) ≤ S n

Tactic:
refine ConvexBody.smul_le_of_le K h_zero ?_

Premises used: ConvexBody.smul_le_of_le
-- 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_1 : u (n + 1) ≤ u n
⊢ 1 + u (n + 1) ≤ 1 + u n

Tactic:
rw [add_le_add_iff_left]

Premises used: add_le_add_iff_left
-- 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 : ℕ
⊢ u (n + 1) ≤ u n

Tactic:
le_of_lt <| (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.1 (Nat.lt_add_one n)

Premises used: Exists.choose_spec, exists_seq_strictAnti_tendsto, le_of_lt, Nat.lt_add_one, And.left, OfNat.ofNat
-- 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 : ℕ
⊢ u (n + 1) ≤ u n

Tactic:
exact le_of_lt <| (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.1 (Nat.lt_add_one n)

Premises used: Exists.choose_spec, exists_seq_strictAnti_tendsto, le_of_lt, Nat.lt_add_one, And.left, OfNat.ofNat
-- 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)
y : E
hy : y ∈ (↑K : Set E)
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ (↑(1 + u n) : ℝ) • x) (-y)) (-(fun (x : E) ↦ (↑(1 + u n) : ℝ) • x) y)

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 : 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)
y : E
hy : y ∈ (↑K : Set E)
⊢ -(fun (x : E) ↦ (↑(1 + u n) : ℝ) • x) y ∈ S n

Tactic:
exact ⟨-y, h_symm _ hy, by 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 : 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)
⊢ ∀ 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⟩
-- 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
obtain : ∀ (x : ↥L) (hx_nz : x ≠ 0) (hx_mem : (↑x : E) ∈ (↑(S n) : Set E)), (Z n).Nonempty
⊢ (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

Premises used: MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure, ConvexBody.convex
-- 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)
⊢ (↑x : E) ∈ (↑L : Set E) \ {0}

Tactic:
simp_all