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 : μ.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)
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) 2 w) + HSMul.hSMul (α := ℝ) 2⁻¹ (-HSMul.hSMul (α := ℝ) 2 v) ∈ s

Tactic:
h_conv hw (h_symm _ hv) ?_ ?_ ?_

Premises used: Set.Mem
-- 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)
refine_1 refine_2 : LE.le (α := ℝ) 0 2⁻¹
refine_3 : HAdd.hAdd (α := ℝ) 2⁻¹ 2⁻¹ = 1
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) 2 w) + HSMul.hSMul (α := ℝ) 2⁻¹ (-HSMul.hSMul (α := ℝ) 2 v) ∈ s

Tactic:
refine h_conv hw (h_symm _ hv) ?_ ?_ ?_
-- 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)
⊢ LE.le (α := ℝ) 0 2⁻¹

Tactic:
norm_num
-- 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)
⊢ HAdd.hAdd (α := ℝ) 2⁻¹ 2⁻¹ = 1

Tactic:
norm_num
-- 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μ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [hμ] using h
-- 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
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have h_mes : μ s ≠ 0 := fun hμ ↦ fund.measure_ne_zero (NeZero.ne μ) <| by simpa [hμ] using h
-- 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∞)
⊢ s.Nonempty

Tactic:
have h_nemp : s.Nonempty := nonempty_of_measure_ne_zero h_mes
-- 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})
⊢ 0 ∈ K

Tactic:
have h_zero : 0 ∈ K := K.zero_mem_of_symmetric h_symm
-- 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
this : Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)
erw : ∀ (this : ((↑K : Set E) ∩ ((↑L : Set E) \ {0})).Nonempty), ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
erw₁ : ∀ (this : ((⋂ (i : ℕ), (↑(S i) : Set E)) ∩ ((↑L : Set E) \ {0})).Nonempty), Tendsto u atTop (nhds 0)
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s

Tactic:
erw [← Set.iInter_inter, K.iInter_smul_eq_self h_zero] at this

Premises used: Set.iInter_inter, ConvexBody.iInter_smul_eq_self
-- 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
this : ((↑K : Set E) ∩ ((↑L : Set E) \ {0})).Nonempty
obtain : ∀ (x : E) (hx : x ∈ (↑K : Set E) ∩ ((↑L : Set E) \ {0})), ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s

Tactic:
obtain ⟨x, hx⟩ := this
-- 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
x : E
hx : x ∈ (↑K : Set E) ∩ ((↑L : Set E) \ {0})
⊢ x ∈ L

Tactic:
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
x : E
hx : x ∈ (↑K : Set E) ∩ ((↑L : Set E) \ {0})
⊢ Ne (α := ↥L) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) x ⋯) 0 ∧ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ L) x ⋯) : E) ∈ s

Tactic:
aesop
-- 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
x : E
hx : x ∈ (↑K : Set E) ∩ ((↑L : Set E) \ {0})
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s

Tactic:
exact ⟨⟨x, by simp_all⟩, by aesop⟩
-- 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
this : ((⋂ (i : ℕ), (↑(S i) : Set E)) ∩ ((↑L : Set E) \ {0})).Nonempty
⊢ Tendsto u atTop (nhds 0)

Tactic:
(exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.2.2

Premises used: Exists.choose_spec, exists_seq_strictAnti_tendsto, And.right, 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
this : ((⋂ (i : ℕ), (↑(S i) : Set E)) ∩ ((↑L : Set E) \ {0})).Nonempty
⊢ Tendsto u atTop (nhds 0)

Tactic:
exact (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.2.2

Premises used: Exists.choose_spec, exists_seq_strictAnti_tendsto, And.right, 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
suffices : Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s

Tactic:
suffices Set.Nonempty (⋂ n, Z n) by
    erw [← Set.iInter_inter, K.iInter_smul_eq_self h_zero] at this
    · obtain ⟨x, hx⟩ := this
      exact ⟨⟨x, by simp_all⟩, by aesop⟩
    · exact (exists_seq_strictAnti_tendsto (0 : ℝ≥0)).choose_spec.2.2
-- 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
rsuffices : ∀ (U : Set E) (hU : IsOpen U ∧ U ∩ (↑L : Set E) = {0}), IsClosed ((↑L : Set E) \ {0})
rsuffices₁ : ∃ (U : Set E), IsOpen U ∧ U ∩ (↑L : Set E) = {0}
⊢ IsClosed ((↑L : Set E) \ {0})

Tactic:
rsuffices ⟨U, hU⟩ : ∃ U : Set E, IsOpen U ∧ U ∩ L = {0}

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

Tactic:
simp [Set.inter_comm .. ▸ hU.2, zero_mem]

Premises used: ZeroMemClass.zero_mem
-- 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
hU : IsOpen U ∧ U ∩ (↑L : Set E) = {0}
rw : IsClosed ((↑L : Set E) \ U)
⊢ IsClosed ((↑L : Set E) \ {0})

Tactic:
rw [sdiff_eq_sdiff_iff_inf_eq_inf (z := U).mpr (by simp [Set.inter_comm .. ▸ hU.2, zero_mem])]

Premises used: Iff.mpr, sdiff_eq_sdiff_iff_inf_eq_inf
-- 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
hU : IsOpen U ∧ U ∩ (↑L : Set E) = {0}
⊢ IsClosed ((↑L : Set E) \ U)

Tactic:
AddSubgroup.isClosed_of_discrete.sdiff hU.1

Premises used: AddSubgroup.isClosed_of_discrete, IsClosed.sdiff, And.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
U : Set E
hU : IsOpen U ∧ U ∩ (↑L : Set E) = {0}
⊢ IsClosed ((↑L : Set E) \ U)

Tactic:
exact AddSubgroup.isClosed_of_discrete.sdiff hU.1

Premises used: AddSubgroup.isClosed_of_discrete, IsClosed.sdiff, And.left