ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>inst✝¹ : CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>N : ℝ≥0<VAR>h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖<VAR>inst✝ : RingHomIsometric σ₁₂<GOAL>0 ≤ ↑N * ‖f‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>inst✝¹ : CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>N : ℝ≥0<VAR>h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖<VAR>inst✝ : RingHomIsometric σ₁₂<GOAL>Continuous fun x => ‖(f.extend e h_dense ⋯) x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>inst✝¹ : CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>N : ℝ≥0<VAR>h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖<VAR>inst✝ : RingHomIsometric σ₁₂<GOAL>Continuous fun x => ↑N * ‖f‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedAddCommGroup G<VAR>inst✝⁹ : NormedAddCommGroup Fₗ<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜₃ G<VAR>inst✝² : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>inst✝¹ : CompleteSpace F<VAR>e : E →L[𝕜] Fₗ<VAR>h_dense : DenseRange ⇑e<VAR>N : ℝ≥0<VAR>h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>x : E<GOAL>‖(f.extend e h_dense ⋯) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C<VAR>J : Type<VAR>hJ : SmallCategory J<VAR>hhJ : FinCategory J<VAR>this : HasColimitsOfShape (ULiftHom (ULift.{w, 0} J)) C<VAR>l : J ≌ ULiftHom (ULift.{?u.2350, 0} J)<GOAL>HasColimitsOfShape J C
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hne : s.Nonempty<VAR>hbdd : BddBelow s<VAR>hlim : ¬IsPredLimit (sInf s)<GOAL>sInf s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hne : s.Nonempty<VAR>hbdd : BddBelow s<VAR>hlim : ¬IsPredLimit (sInf s)<VAR>y : α<VAR>hy : sInf s ⋖ y<GOAL>sInf s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : ConditionallyCompleteLinearOrder α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hne : s.Nonempty<VAR>hbdd : BddBelow s<VAR>hlim : ¬IsPredLimit (sInf s)<VAR>y : α<VAR>hy : sInf s ⋖ y<VAR>i : α<VAR>his : i ∈ s<VAR>hi : i < y<GOAL>sInf s ∈ s
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ℚ<VAR>hε'0 : 0 < ↑ε'<VAR>hε' : ↑ε' < ε<GOAL>∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ℚ<VAR>hε' : ↑ε' < ε<VAR>hε'0 : 0 < ε'<GOAL>∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ℚ<VAR>hε' : ↑ε' < ε<VAR>hε'0 : 0 < ε'<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'<GOAL>∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ℚ<VAR>hε' : ↑ε' < ε<VAR>hε'0 : 0 < ε'<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'<GOAL>∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ℚ<VAR>hε' : ↑ε' < ε<VAR>hε'0 : 0 < ε'<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r : R<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>ε' : ℚ<VAR>hε' : ↑ε' < ε<VAR>hε'0 : 0 < ε'<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ↑ε'
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>p' : Filter β<GOAL>TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>p' : Filter β<VAR>H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<GOAL>∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε✝ ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>p' : Filter β<VAR>H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε<VAR>u : Set (α × α)<VAR>hu : u ∈ 𝓤 α<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ u<GOAL>∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>ζ : K<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>Splits (RingHom.id K) (X ^ n - C 1)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>s : Set 𝕜<VAR>h0 : 0 ∈ s<VAR>f : C(↑s, 𝕜)<VAR>hf : f ∈ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})<GOAL>f ∈ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.41105, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>inst✝² : Preregular C<VAR>inst✝¹ : FinitaryExtensive C<VAR>inst✝ : ∀ (X : C), Projective X<GOAL>IsSheaf (coherentTopology C) F ↔ Nonempty (PreservesFiniteProducts F)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>R : Type u_3<VAR>α : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSemiring α<VAR>f g : ι → α<VAR>a a₁ a₂✝ a₂ : α<VAR>hf : HasSum f a₁<GOAL>HasSum (fun i => f i * a₂) (a₁ * a₂)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : AddGroup N<VAR>f f₁ f₂ g g₁ g₂ : α →₀ N<GOAL>(f + g).neLocus f = g.support
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → ℂ<VAR>x : ℝ<VAR>f' : ℂ<VAR>h₁ : HasDerivAt f f' x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasDerivAt (fun t => log (f t)) (f' / f x) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>(C a * p).comp r = C a * p.comp r
<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>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K I < volume (convexBodyLT' K f w₀)<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
<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>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K I < volume (convexBodyLT' K f w₀)<VAR>h_fund : IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup) (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
<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>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K I < volume (convexBodyLT' K f w₀)<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 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
<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>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K I < volume (convexBodyLT' K f w₀)<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⟩ ∈ convexBodyLT' K f w₀<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
<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>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K I < volume (convexBodyLT' K f w₀)<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✝⟩ ∈ convexBodyLT' K f w₀<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
<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>w₀ : { w // w.IsComplex }<VAR>h : minkowskiBound K I < volume (convexBodyLT' K f w₀)<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⟩ ∈ convexBodyLT' K f w₀<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeas E' 𝕜 m p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0<GOAL>↑↑↑f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeas E' 𝕜 m p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0<VAR>g : α → E'<VAR>hg_sm : FinStronglyMeasurable g (μ.trim hm)<VAR>hfg : ↑↑↑f =ᶠ[ae μ] g<GOAL>↑↑↑f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeas E' 𝕜 m p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0<VAR>g : α → E'<VAR>hg_sm : FinStronglyMeasurable g (μ.trim hm)<VAR>hfg : ↑↑↑f =ᶠ[ae μ] g<GOAL>g =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeas E' 𝕜 m p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0<VAR>g : α → E'<VAR>hg_sm : FinStronglyMeasurable g (μ.trim hm)<VAR>hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x<GOAL>g =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeas E' 𝕜 m p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0<VAR>g : α → E'<VAR>hg_sm : FinStronglyMeasurable g (μ.trim hm)<VAR>hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeas E' 𝕜 m p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0<VAR>g : α → E'<VAR>hg_sm : FinStronglyMeasurable g (μ.trim hm)<VAR>hfg : ∀ᵐ (x : α) ∂μ, ↑↑↑f x = g x<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>σ : α → Type u_4<VAR>a : α<VAR>s : Multiset α<VAR>t : (a : α) → Multiset (σ a)<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<GOAL>((↑l₁).sigma fun a => ↑(l₂ a)) = ↑(l₁.sigma l₂)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>σ : α → Type u_4<VAR>a : α<VAR>s : Multiset α<VAR>t : (a : α) → Multiset (σ a)<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<GOAL>((↑l₁).bind fun a => map (Sigma.mk a) ↑(l₂ a)) = (↑l₁).bind fun a => ↑(List.map (Sigma.mk a) (l₂ a))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f' : Y → X<VAR>h : Continuous f'<VAR>l_inv : LeftInverse f f'<VAR>r_inv : Function.RightInverse f f'<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsClosed (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f' : Y → X<VAR>h : Continuous f'<VAR>l_inv : LeftInverse f f'<VAR>r_inv : Function.RightInverse f f'<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsClosed (f' ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>x : Set α<VAR>y : Set β<GOAL>∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : SigmaFinite μ<VAR>hf : Integrable (fun x => rexp (f x)) μ<GOAL>(fun x => log ((μ.tilted f).rnDeriv μ x).toReal) =ᶠ[ae μ] fun x => f x - log (∫ (x : α), rexp (f x) ∂μ)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : PointClass F<VAR>a✝¹ : Fin 3 → F<VAR>hP : W.NonsingularLift (Quot.mk Setoid.r a✝¹)<VAR>a✝ : Fin 3 → F<VAR>hQ : W.NonsingularLift (Quot.mk Setoid.r a✝)<GOAL>W.NonsingularLift (W.addMap (Quot.mk Setoid.r a✝¹) (Quot.mk Setoid.r a✝))
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>pa : ¬p a = true<GOAL>a ∈ eraseP p l ↔ a ∈ l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>pa : ¬p a = true<VAR>al : a ∈ l<GOAL>a ∈ eraseP p l
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<GOAL>R[X]⁰ ≤ Submonoid.comap { toFun := ⇑(taylor r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } R[X]⁰
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : CommSemiring α<VAR>inst✝⁴ : LinearOrder α<VAR>a✝ b✝ c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>2 * a * b ≤ a ^ 2 + b ^ 2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : L<VAR>D₁ D₂ : LieDerivation R L L<VAR>y : L<GOAL>⁅x, ⁅D₁, D₂⁆⁆ y = (⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆) y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>δ : Type u_3<VAR>inst✝ : CommGroup δ<VAR>f : ℕ → δ<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(∏ k ∈ Ico m n, f k) * ∏ k ∈ range m, f k = ∏ k ∈ range n, f k
<VAR>n : ℕ<VAR>c : Char<GOAL>(replicate n c).length = n
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>P X✝ Y Z : C<VAR>fst : P ⟶ X✝<VAR>snd : P ⟶ Y<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>s : Cone (cospan (𝟙 X) 0)<GOAL>∀ (j : WalkingCospan), (fun s => 0) s ≫ (PullbackCone.mk 0 0 ⋯).π.app j = s.π.app j
<VAR>d a b : ℤ<GOAL>↑a ∣ ↑b ↔ a ∣ b
<VAR>d a b : ℤ<GOAL>a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ ≤ y ^ 1 ↔ x ≤ y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q n : ℕ<GOAL>(P q ≫ P q).f n = (P q).f n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b n : α<VAR>a_nonneg : 0 ≤ a<VAR>a_lt_n : a < n<VAR>b_nonneg : 0 ≤ b<VAR>b_lt_n : b < n<GOAL>|a - b| < n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b n : α<VAR>a_nonneg : 0 ≤ a<VAR>a_lt_n : a < n<VAR>b_nonneg : 0 ≤ b<VAR>b_lt_n : b < n<GOAL>a < n + b ∧ b < n + a
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>p : Fin (n + 1)<VAR>a : α p<VAR>f : (i : Fin n) → α (p.succAbove i)<VAR>g : (j : Fin (n + 1)) → α j<GOAL>g = p.insertNth a f ↔ g p = a ∧ p.removeNth g = f