awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : μ.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)
⊢ (↑(x - y) : E) ∈ s
have rw : HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) 2 w) + HSMul.hSMul (α := ℝ) 2⁻¹ (-HSMul.hSMul (α := ℝ) 2 v) ∈ s
Tactic: rw [← hvw, ← inv_smul_smul₀ (two_ne_zero' ℝ) (_ - _), smul_sub, sub_eq_add_neg, smul_add]
-- 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 : μ.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
have refine_1 : LE.le (α := ℝ) 0 2⁻¹
Tactic: refine h_conv hw (h_symm _ hv) ?_ ?_ ?_
-- 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 : μ.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⁻¹
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) 2 w) + HSMul.hSMul (α := ℝ) 2⁻¹ (-HSMul.hSMul (α := ℝ) 2 v) ∈ s
have refine_3 : HAdd.hAdd (α := ℝ) 2⁻¹ 2⁻¹ = 1
Tactic: refine h_conv hw (h_symm _ hv) ?_ ?_ ?_
-- 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
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have h_mes : 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
-- 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∞)
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have h_nemp : s.Nonempty
Tactic: have h_nemp : s.Nonempty := nonempty_of_measure_ne_zero h_mes
-- 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})
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have h_zero : 0 ∈ K
Tactic: have h_zero : 0 ∈ K := K.zero_mem_of_symmetric h_symm
-- 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
this : Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have erw : ∀ (this : ((↑K : Set E) ∩ ((↑L : Set E) \ {0})).Nonempty), ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
Tactic: erw [← Set.iInter_inter, K.iInter_smul_eq_self h_zero] at this
Cleared hypotheses: 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
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
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have erw₁ : ∀ (this : ((⋂ (i : ℕ), (↑(S i) : Set E)) ∩ ((↑L : Set E) \ {0})).Nonempty), Tendsto u atTop (nhds 0)
Tactic: erw [← Set.iInter_inter, K.iInter_smul_eq_self h_zero] at this
Cleared hypotheses: 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
this : ((↑K : Set E) ∩ ((↑L : Set E) \ {0})).Nonempty
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have obtain : ∀ (x : E) (hx : x ∈ (↑K : Set E) ∩ ((↑L : Set E) \ {0})), ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
Tactic: obtain ⟨x, hx⟩ := this
Cleared hypotheses: 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
⊢ ∃ (x : ↥L), x ≠ 0 ∧ (↑x : E) ∈ s
have suffices : Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)
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
-- 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
⊢ IsClosed ((↑L : Set E) \ {0})
have rsuffices : ∀ (U : Set E) (hU : IsOpen U ∧ U ∩ (↑L : Set E) = {0}), IsClosed ((↑L : Set E) \ {0})
Tactic: rsuffices ⟨U, hU⟩ : ∃ U : Set E, IsOpen U ∧ U ∩ L = {0}
-- 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
rsuffices : ∀ (U : Set E) (hU : IsOpen U ∧ U ∩ (↑L : Set E) = {0}), IsClosed ((↑L : Set E) \ {0})
⊢ IsClosed ((↑L : Set E) \ {0})
have rsuffices₁ : ∃ (U : Set E), IsOpen U ∧ U ∩ (↑L : Set E) = {0}
Tactic: rsuffices ⟨U, hU⟩ : ∃ U : Set E, IsOpen U ∧ U ∩ L = {0}
-- 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
U : Set E
hU : IsOpen U ∧ U ∩ (↑L : Set E) = {0}
⊢ IsClosed ((↑L : Set E) \ {0})
have rw : IsClosed ((↑L : Set E) \ U)
Tactic: rw [sdiff_eq_sdiff_iff_inf_eq_inf (z := U).mpr (by simp [Set.inter_comm .. ▸ hU.2, zero_mem])]
-- 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
⊢ Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)
have h_clos : 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)
-- 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})
⊢ Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)
have refine_1 : ∀ (n : ℕ), Z (n + 1) ⊆ 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)
-- 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})
refine_1 : ∀ (n : ℕ), Z (n + 1) ⊆ Z n
⊢ Set.Nonempty.{u_1} (α := E) (⋂ (n : ℕ), Z n)
have refine_2 : ∀ (n : ℕ), (Z n).Nonempty
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)
-- 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 + 1) ⊆ Z n
have refine_1 : S (n + 1) ≤ S n
Tactic: refine Set.inter_subset_inter_left _ (SetLike.coe_subset_coe.mpr ?_)
-- 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 : ℕ
⊢ S (n + 1) ≤ S n
have refine_1 : 1 + u (n + 1) ≤ 1 + u n
Tactic: refine ConvexBody.smul_le_of_le K h_zero ?_
-- 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 + u (n + 1) ≤ 1 + u n
have refine_1 : u (n + 1) ≤ u n
Tactic: rw [add_le_add_iff_left]