ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁹ : NormedField 𝕜₁<VAR>inst✝⁸ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜₁ E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜₂ F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : T2Space F<VAR>𝔖 : Set (Set E)<VAR>h𝔖 : ⋃₀ 𝔖 = Set.univ<VAR>this : UniformSpace F := TopologicalAddGroup.toUniformSpace F<GOAL>T2Space (UniformConvergenceCLM σ F 𝔖)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁹ : NormedField 𝕜₁<VAR>inst✝⁸ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜₁ E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜₂ F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : T2Space F<VAR>𝔖 : Set (Set E)<VAR>h𝔖 : ⋃₀ 𝔖 = Set.univ<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>T2Space (UniformConvergenceCLM σ F 𝔖)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁹ : NormedField 𝕜₁<VAR>inst✝⁸ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜₁ E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜₂ F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : T2Space F<VAR>𝔖 : Set (Set E)<VAR>h𝔖 : ⋃₀ 𝔖 = Set.univ<VAR>this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this✝ : UniformAddGroup F<VAR>this : T2Space (E →ᵤ[𝔖] F)<GOAL>T2Space (UniformConvergenceCLM σ F 𝔖)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>x✝ : E<GOAL>x✝ ∈ a • ball b r ↔ x✝ ∈ ball (a • b) r
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y<GOAL>∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑1 * dist x y
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : Category.{?u.225, u_1} C<VAR>inst✝⁴ : Category.{?u.229, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>G : Type u_4<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : HasShift C G<VAR>sequence : M → C ⥤ A<VAR>isoZero : sequence 0 ≅ F<VAR>shiftIso : (n a a' : M) → n + a = a' → (shiftFunctor C n ⋙ sequence a ≅ sequence a')<VAR>shiftIso_zero : ∀ (a : M), shiftIso 0 a a ⋯ = isoWhiskerRight (shiftFunctorZero C M) (sequence a) ≪≫ (sequence a).leftUnitor<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>m + n + a = a''
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>inst✝ : DecidableEq σ<GOAL>(coeff R n) (φ * ψ) = ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>inst✝ : DecidableEq σ<GOAL>antidiagonal n = antidiagonal n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>f : α → Semiquot β<VAR>b : β<GOAL>b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>f : α → Semiquot β<VAR>b : β<GOAL>b ∈ q.bind f ↔ ∃ a, ∃ (_ : a ∈ q), b ∈ f a
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : MonoidalCategory C<VAR>P : C → Prop<VAR>inst✝² : MonoidalPredicate P<VAR>P' : C → Prop<VAR>inst✝¹ : MonoidalPredicate P'<VAR>inst✝ : BraidedCategory C<VAR>X Y : FullSubcategory P<GOAL>(fullMonoidalSubcategoryInclusion P).map (β_ X Y).hom = inv ((fullMonoidalSubcategoryInclusion P).μ X Y) ≫ (β_ ((fullMonoidalSubcategoryInclusion P).obj X) ((fullMonoidalSubcategoryInclusion P).obj Y)).hom ≫ (fullMonoidalSubcategoryInclusion P).μ Y X
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : MonoidalCategory C<VAR>P : C → Prop<VAR>inst✝² : MonoidalPredicate P<VAR>P' : C → Prop<VAR>inst✝¹ : MonoidalPredicate P'<VAR>inst✝ : BraidedCategory C<VAR>X Y : FullSubcategory P<GOAL>(fullMonoidalSubcategoryInclusion P).μ X Y ≫ (fullMonoidalSubcategoryInclusion P).map (β_ X Y).hom = (β_ ((fullMonoidalSubcategoryInclusion P).obj X) ((fullMonoidalSubcategoryInclusion P).obj Y)).hom ≫ (fullMonoidalSubcategoryInclusion P).μ Y X
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>1 < 0 ^ n ↔ 1 < 0
<VAR>a✝ b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : ℕ<GOAL>1 < (a + 2) ^ n ↔ 1 < a + 2
<VAR>x : ℝ<GOAL>cos (π / 6) ^ 2 = 3 / 4
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Primcodable β<VAR>inst✝³ : Primcodable γ<VAR>inst✝² : Primcodable δ<VAR>inst✝¹ : Primcodable σ<VAR>c : α → Prop<VAR>inst✝ : DecidablePred c<VAR>f g : α → σ<VAR>hc : PrimrecPred c<VAR>hf : Primrec f<VAR>hg : Primrec g<GOAL>Primrec fun a => if c a then f a else g a
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>hl : l.Sized<VAR>size✝ : ℕ<VAR>l✝ : Ordnode α<VAR>x✝ : α<VAR>r✝ : Ordnode α<VAR>hr : (node size✝ l✝ x✝ r✝).Sized<GOAL>(l.rotateL x (node size✝ l✝ x✝ r✝)).Sized
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>hl : l.Sized<VAR>size✝ : ℕ<VAR>l✝ : Ordnode α<VAR>x✝ : α<VAR>r✝ : Ordnode α<VAR>hr : (node size✝ l✝ x✝ r✝).Sized<GOAL>(if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).Sized
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>v : V<VAR>p : P<VAR>hp : p ∈ s<VAR>h : v +ᵥ p ∈ s<GOAL>v ∈ s.direction
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝¹ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h₁ : IsClosed s<VAR>h₂ : interior t = ∅<VAR>x : X<VAR>x✝ : x ∈ interior (s ∪ t)<VAR>u : Set X<VAR>hu₁ : IsOpen u<VAR>hu₂ : u ⊆ s ∪ t<VAR>hx₁ : x ∈ u<VAR>hx₂ : x ∉ s<VAR>this : u \ s ⊆ t<GOAL>u \ s ⊆ interior t
<VAR>X : Type u_1<GOAL>support 0 = ∅
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : G.toPresheaf ⟶ F'<VAR>h : Presieve.IsSheaf J F'<VAR>U : Cᵒᵖ<VAR>s : G.toPresheaf.obj U<GOAL>(homOfLe ⋯ ≫ G.sheafifyLift f h).app U s = f.app U s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : G.toPresheaf ⟶ F'<VAR>h : Presieve.IsSheaf J F'<VAR>U : Cᵒᵖ<VAR>s : G.toPresheaf.obj U<GOAL>∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop U⦄, (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows f_1 → F'.map f_1.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map f_1.op (f.app U s)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : G.toPresheaf ⟶ F'<VAR>h : Presieve.IsSheaf J F'<VAR>U : Cᵒᵖ<VAR>s : G.toPresheaf.obj U<VAR>V : C<VAR>i : V ⟶ unop U<VAR>hi : (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows i<GOAL>F'.map i.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map i.op (f.app U s)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>f : G.toPresheaf ⟶ F'<VAR>h : Presieve.IsSheaf J F'<VAR>U : Cᵒᵖ<VAR>s : G.toPresheaf.obj U<VAR>V : C<VAR>i : V ⟶ unop U<VAR>hi : (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows i<VAR>this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toPresheaf.obj X), f.app Y (G.toPresheaf.map f_1 x) = F'.map f_1 (f.app X x)<GOAL>F'.map i.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map i.op (f.app U s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>w✝ w₁✝ w₂✝ : ι → k<VAR>p✝ : ι → V<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>x✝ : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<GOAL>(affineCombination k s p) w ∈ affineSpan k {(affineCombination k s p) w₁, (affineCombination k s p) w₂} ↔ ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>w✝ w₁✝ w₂✝ : ι → k<VAR>p✝ : ι → V<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>x✝ : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<GOAL>(∃ r, ∀ i ∈ s, (w - w₁) i = r * (w₂ i - w₁ i)) ↔ ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>w✝ w₁✝ w₂✝ : ι → k<VAR>p✝ : ι → V<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>x✝ : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<GOAL>∑ i ∈ s, (w - w₁) i = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : Closeds α<GOAL>(Opens.compl ∘ ⇑ofDual) ((⇑toDual ∘ compl) s) = s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : (Opens α)ᵒᵈ<GOAL>(⇑toDual ∘ compl) ((Opens.compl ∘ ⇑ofDual) s) = s
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>n : ℕ<VAR>x y : α →₀ ℕ<GOAL>(x, y) ∈ antidiagonal (single a n) ↔ (x, y) ∈ map ({ toFun := single a, inj' := ⋯ }.prodMap { toFun := single a, inj' := ⋯ }) (antidiagonal n)
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>n : ℕ<VAR>x y : α →₀ ℕ<GOAL>x + y = single a n ↔ ∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>h_nz : ⟨x, hx⟩ ≠ 0<VAR>h_mem : ↑⟨x, hx⟩ ∈ convexBodySum K B<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx✝ : x ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>hx : x ∈ ⇑(mixedEmbedding K) '' ↑↑I<VAR>h_nz : ⟨x, hx✝⟩ ≠ 0<VAR>h_mem : ↑⟨x, hx✝⟩ ∈ convexBodySum K B<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>a : K<VAR>ha : a ∈ ↑↑I<VAR>hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0<VAR>h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B<GOAL>↑|(Algebra.norm ℚ) a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>a : K<VAR>ha : a ∈ ↑↑I<VAR>hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0<VAR>h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B<GOAL>↑(finrank ℚ K) * ↑|(Algebra.norm ℚ) a| ^ (↑(finrank ℚ K))⁻¹ ≤ B
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>a : K<VAR>ha : a ∈ ↑↑I<VAR>hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0<VAR>h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B<GOAL>↑(finrank ℚ K) * ↑|(Algebra.norm ℚ) a| ^ (↑(finrank ℚ K))⁻¹ ≤ ∑ w : InfinitePlace K, ↑w.mult * ↑w a
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>a : K<VAR>ha : a ∈ ↑↑I<VAR>hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0<VAR>h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B<GOAL>↑|(Algebra.norm ℚ) a| ^ (∑ x : InfinitePlace K, ↑x.mult)⁻¹ ≤ (∑ w : InfinitePlace K, ↑w.mult * ↑w a) / ∑ x : InfinitePlace K, ↑x.mult
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>a : K<VAR>ha : a ∈ ↑↑I<VAR>hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0<VAR>h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B<GOAL>↑|(Algebra.norm ℚ) a| ^ (∑ x : InfinitePlace K, ↑x.mult)⁻¹ ≤ (∏ i : InfinitePlace K, ↑i a ^ ↑i.mult) ^ (∑ i : InfinitePlace K, ↑i.mult)⁻¹
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I✝ : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>f : InfinitePlace K → ℝ≥0<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>B : ℝ<VAR>h : minkowskiBound K I ≤ volume (convexBodySum K B)<VAR>hB : 0 ≤ B<VAR>h1 : 0 < (↑(finrank ℚ K))⁻¹<VAR>h2 : 0 ≤ B / ↑(finrank ℚ K)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<VAR>this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>a : K<VAR>ha : a ∈ ↑↑I<VAR>hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup<VAR>h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0<VAR>h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B<GOAL>0 < ∑ i : InfinitePlace K, ↑i.mult
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>s✝ : Set α<GOAL>s✝ ∈ ae (c • μ) ↔ s✝ ∈ ae μ
<VAR>F✝ : Type u → Type w<VAR>G : Type v → Type u<VAR>inst✝⁴ : Applicative F✝<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulApplicative F✝<VAR>inst✝¹ : LawfulApplicative G<VAR>α β γ : Type v<VAR>F : Type u_1 → Type u_2<VAR>AF : Applicative F<VAR>inst✝ : LawfulApplicative F<VAR>α✝ β✝ : Type u_1<VAR>f : F (α✝ → β✝)<VAR>x : F α✝<GOAL>(Seq.seq (id <$> f) fun x_1 => x) = Seq.seq f fun x_1 => x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<GOAL>s1.direction ⊔ s2.direction < (s1 ⊔ s2).direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<GOAL>s1.direction ⊔ s2.direction ≤ (s1 ⊔ s2).direction ∧ ∃ x ∈ (s1 ⊔ s2).direction, x ∉ s1.direction ⊔ s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<GOAL>p2 -ᵥ p1 ∉ s1.direction ⊔ s2.direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<VAR>h : p2 -ᵥ p1 ∈ s1.direction ⊔ s2.direction<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<VAR>h : ∃ y ∈ s1.direction, ∃ z ∈ s2.direction, y + z = p2 -ᵥ p1<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<VAR>v1 : V<VAR>hv1 : v1 ∈ s1.direction<VAR>v2 : V<VAR>hv2 : v2 ∈ s2.direction<VAR>hv1v2 : v1 + v2 = p2 -ᵥ p1<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<VAR>v1 : V<VAR>hv1 : v1 ∈ s1.direction<VAR>v2 : V<VAR>hv2 : v2 ∈ s2.direction<VAR>hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2<GOAL>False
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<VAR>v1 : V<VAR>hv1 : v1 ∈ s1.direction<VAR>v2 : V<VAR>hv2 : v2 ∈ s2.direction<VAR>hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2<GOAL>(↑s1 ∩ ↑s2).Nonempty
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<VAR>v1 : V<VAR>hv1 : v1 ∈ s1.direction<VAR>v2 : V<VAR>hv2 : v2 ∈ s2.direction<VAR>hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2<GOAL>v1 +ᵥ p1 ∈ ↑s2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>he : ↑s1 ∩ ↑s2 = ∅<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s1<VAR>p2 : P<VAR>hp2 : p2 ∈ ↑s2<VAR>v1 : V<VAR>hv1 : v1 ∈ s1.direction<VAR>v2 : V<VAR>hv2 : v2 ∈ s2.direction<VAR>hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2<GOAL>-v2 +ᵥ p2 ∈ ↑s2