ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1<VAR>x : E<VAR>hx : ‖x‖ = 1<VAR>y : E<VAR>hy : ‖y‖ = 1<VAR>hne : x ≠ y<GOAL>∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1<VAR>x : E<VAR>hx : ‖x‖ = 1<VAR>y : E<VAR>hy : ‖y‖ = 1<VAR>hne : x ≠ y<VAR>a b : ℝ<VAR>hab : a + b = 1<VAR>hlt : ‖a • x + b • y‖ < 1<GOAL>∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1<VAR>x : E<VAR>hx : ‖x‖ = 1<VAR>y : E<VAR>hy : ‖y‖ = 1<VAR>hne : x ≠ y<VAR>a b : ℝ<VAR>hab : a + b = 1<VAR>hlt : ‖a • x + b • y‖ < 1<GOAL>(AffineMap.lineMap x y) b ∈ interior (closedBall 0 1)
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<VAR>s : ↥S<GOAL>mk' f m s = 0 ↔ ∃ s', s' • m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>R₃ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R₂<VAR>inst✝⁸ : Ring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>inst✝² : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u.comp f = v.comp f → u = v<GOAL>range f = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>R₃ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R₂<VAR>inst✝⁸ : Ring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>inst✝² : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u.comp f = v.comp f → u = v<VAR>h₁ : comp 0 f = 0<GOAL>range f = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>R₃ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R₂<VAR>inst✝⁸ : Ring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommGroup M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>inst✝² : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u.comp f = v.comp f → u = v<VAR>h₁ : comp 0 f = 0<GOAL>ker 0 = ⊤
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>hs : MeasurableSet s<GOAL>μ.restrict sᶜ + μ.restrict s = μ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l l' : List α<VAR>c : Composition l.length<VAR>h : l' ∈ l.splitWrtComposition c<GOAL>0 < l'.length
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l l' : List α<VAR>c : Composition l.length<VAR>h : l' ∈ l.splitWrtComposition c<VAR>this : l'.length ∈ map length (l.splitWrtComposition c)<GOAL>0 < l'.length
<VAR>n : ℕ<VAR>α : Type u_1<VAR>l l' : List α<VAR>c : Composition l.length<VAR>h : l' ∈ l.splitWrtComposition c<VAR>this : l'.length ∈ c.blocks<GOAL>0 < l'.length
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>x : E<VAR>hx : ¬x = 0<GOAL>IsConnected {y | SameRay ℝ x y}
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>x : E<VAR>hx : ¬x = 0<GOAL>IsConnected {y | ∃ r, 0 ≤ r ∧ r • x = y}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌊a⌋ ≤ z - 1 ↔ a < ↑z
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : UniqueFactorizationMonoid α<VAR>inst✝³ : DecidableEq (Associates α)<VAR>inst✝² : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>k ∣ p.count (a ^ k).factors
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : UniqueFactorizationMonoid α<VAR>inst✝³ : DecidableEq (Associates α)<VAR>inst✝² : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>k ∣ k * p.count a.factors
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>a : M<GOAL>a ^ 3 = a * a * a
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : Adapted ℱ f<VAR>hint : ∀ (i : ι), Integrable (f i) μ<VAR>hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>f i ≤ᶠ[ae μ] μ[f j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ι → Ω → ℝ<VAR>hadp : Adapted ℱ f<VAR>hint : ∀ (i : ι), Integrable (f i) μ<VAR>hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>0 ≤ᶠ[ae μ] μ[f j|↑ℱ i] - μ[f i|↑ℱ i]
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<GOAL>⇑f = toReal ∘ ⇑f.nnrealPart - toReal ∘ ⇑(-f).nnrealPart
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<VAR>x : α<GOAL>f x = (toReal ∘ ⇑f.nnrealPart - toReal ∘ ⇑(-f).nnrealPart) x
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ<VAR>x : α<GOAL>f x = max (f x) 0 - max (-f x) 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.δ ≫ S.L₃.f = 0
<VAR>x : ℝ<GOAL>arctan (-x) = -arctan x
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_5, u_4} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_3<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<VAR>this : HasShift D A := HasShift.induced F A s i<GOAL>(shiftFunctorAdd D a b).hom.app (F.obj X) = (i (a + b)).hom.app X ≫ F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<GOAL>⨅ n, ↑↑n ≠ ⊤ ↔ ∃ n, G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<GOAL>Nonempty ↑{m | G.Colorable m} ↔ ∃ n, G.Colorable n
<VAR>n k : ℕ<GOAL>1 * (k / 2 ^ n) + k % 2 ^ n = k / 2 ^ n + k % 2 ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>inst✝ : Unique ι<VAR>f : ι → α<GOAL>⨆ i, f i = f default
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S✝<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>ι : Sort u_2<VAR>hι : Nonempty ι<VAR>S : ι → NonUnitalSubsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S✝<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>ι : Sort u_2<VAR>hι : Nonempty ι<VAR>S : ι → NonUnitalSubsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i → ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S✝<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>ι : Sort u_2<VAR>hι : Nonempty ι<VAR>S : ι → NonUnitalSubsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>U : NonUnitalSubsemiring R := NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯<GOAL>x ∈ ⨆ i, S i → ∃ i, x ∈ S i
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S✝<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>ι : Sort u_2<VAR>hι : Nonempty ι<VAR>S : ι → NonUnitalSubsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>U : NonUnitalSubsemiring R := NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯<GOAL>⨆ i, S i ≤ U
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra F L<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>f : K →ₐ[F] L<VAR>x✝¹ : L<VAR>x✝ : x✝¹ ∈ f.fieldRange<VAR>x : K<VAR>hx : f.toRingHom x = x✝¹<GOAL>x✝¹ ∈ (minpoly F x).rootSet L
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P<VAR>hf : Function.Bijective ⇑f<VAR>this : Algebra R S := f.toAlgebra<GOAL>P f
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P<VAR>hf : Function.Bijective ⇑f<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : IsLocalization (Submonoid.powers 1) R<GOAL>P f
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>H : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P<VAR>hf : Function.Bijective ⇑f<VAR>this✝¹ : Algebra R S := f.toAlgebra<VAR>this✝ : IsLocalization (Submonoid.powers 1) R<VAR>this : IsLocalization (Submonoid.powers 1) S<GOAL>P f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝ : LT α<VAR>hM : M.BlockTriangular b<VAR>hN : N.BlockTriangular b<VAR>i j : m<VAR>h : b j < b i<GOAL>(M + N) i j = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x y : R<GOAL>seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x y : R<GOAL>∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<VAR>key : φ (l.lcm ↑n) ≤ FiniteDimensional.finrank ℚ K<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<VAR>key : φ (l.lcm ↑n) ≤ φ ↑n<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<VAR>key : φ (l.lcm ↑n) ≤ φ ↑n<VAR>r : ℕ<VAR>hr : GCDMonoid.lcm l ↑n = ↑n * r<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<VAR>key : φ (l.lcm ↑n) ≤ φ ↑n<VAR>r : ℕ<VAR>hr : GCDMonoid.lcm l ↑n = ↑n * r<VAR>ineq : φ ↑n * φ r ≤ φ (↑n * r)<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<VAR>key : φ (l.lcm ↑n) ≤ φ ↑n<VAR>r : ℕ<VAR>hr : GCDMonoid.lcm l ↑n = ↑n * r<VAR>ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<VAR>r : ℕ<VAR>hr : GCDMonoid.lcm l ↑n = ↑n * r<VAR>ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)<VAR>key : φ r ≤ 1<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<VAR>r : ℕ<VAR>hr : GCDMonoid.lcm l ↑n = ↑n * r<VAR>ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)<VAR>key : φ r ≤ 1<VAR>rpos : 0 < r<GOAL>l ∣ 2 * ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl✝ : l ≠ 0<VAR>hl : NeZero l<VAR>hroot : IsPrimitiveRoot (zeta n ℚ K) ↑n<VAR>r : ℕ<VAR>hr : GCDMonoid.lcm l ↑n = ↑n * r<VAR>ineq : φ ↑n * φ r ≤ φ (GCDMonoid.lcm l ↑n)<VAR>rpos : 0 < r<VAR>key : r = 1 ∨ r = 2<GOAL>l ∣ 2 * ↑n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : IsDomain B<VAR>inst✝⁵ : Algebra A B<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>S' : Type u_7<VAR>inst✝³ : CommRing S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : Algebra A S<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>e : S ≃ₐ[A] S'<GOAL>(pb.map e).minpolyGen = pb.minpolyGen
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Ring S<VAR>inst✝⁹ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : IsDomain B<VAR>inst✝⁵ : Algebra A B<VAR>K : Type u_6<VAR>inst✝⁴ : Field K<VAR>S' : Type u_7<VAR>inst✝³ : CommRing S'<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : Algebra A S<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>e : S ≃ₐ[A] S'<GOAL>X ^ pb.dim - ∑ i : Fin pb.dim, C (((pb.map e).basis.repr ((pb.map e).gen ^ pb.dim)) i) * X ^ ↑i = X ^ pb.dim - ∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x : F<GOAL>re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>a : α<VAR>ha : a ≤ sSup S<GOAL>∃ T ⊆ S, a = sSup T
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>C : Set α<VAR>hC : ∀ x ∈ C, IsCompactElement x<VAR>ha : sSup C ≤ sSup S<GOAL>∃ T ⊆ S, sSup C = sSup T
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>C : Set α<VAR>hC : ∀ x ∈ C, IsCompactElement x<VAR>ha : sSup C ≤ sSup S<VAR>aux : ∀ (b : α), IsCompactElement b → b ≤ sSup S → ∃ T ⊆ S, b = sSup T<GOAL>∃ T ⊆ S, sSup C = sSup T
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>C : Set α<VAR>hC : ∀ x ∈ C, IsCompactElement x<VAR>ha : sSup C ≤ sSup S<VAR>T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α<VAR>hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S<VAR>hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)<GOAL>∃ T ⊆ S, sSup C = sSup T
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>C : Set α<VAR>hC : ∀ x ∈ C, IsCompactElement x<VAR>ha : sSup C ≤ sSup S<VAR>T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α<VAR>hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S<VAR>hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)<GOAL>sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} ⊆ S ∧ sSup C = sSup (sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
<VAR>n : ℕ<GOAL>(fun b => succ.comp b)^[n] zero = Code.const n
<VAR>n✝ m n : ℕ<VAR>H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n<GOAL>m.Coprime n
<VAR>n✝ m n : ℕ<VAR>H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n<GOAL>m.gcd n = 1
<VAR>n✝ m n : ℕ<VAR>H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n<VAR>g2 : ¬m.gcd n = 1<GOAL>False
<VAR>n✝ m n : ℕ<VAR>H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n<VAR>g2 : ¬m.gcd n = 1<VAR>p : ℕ<VAR>hp : Prime p<VAR>hpdvd : p ∣ m.gcd n<GOAL>False
<VAR>n✝ m n : ℕ<VAR>H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n<VAR>g2 : ¬m.gcd n = 1<VAR>p : ℕ<VAR>hp : Prime p<VAR>hpdvd : p ∣ m.gcd n<GOAL>m.gcd n ∣ m
<VAR>n✝ m n : ℕ<VAR>H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n<VAR>g2 : ¬m.gcd n = 1<VAR>p : ℕ<VAR>hp : Prime p<VAR>hpdvd : p ∣ m.gcd n<GOAL>m.gcd n ∣ n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>hs : IsCompact s<GOAL>TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>hs : IsCompact s<VAR>this : CompactSpace ↑s<GOAL>TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>hs : IsCompact s<VAR>this : CompactSpace ↑s<VAR>h : TendstoLocallyUniformlyOn F f p s<GOAL>TendstoUniformlyOn F f p s
<VAR>n m : ℕ<VAR>i j : Fin n<GOAL>i.rev = j ↔ i = j.rev
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α → α<VAR>hassoc : Associative f<VAR>a b c : α<VAR>l : List α<GOAL>foldl f a (c :: l ++ [b]) = foldr f b (a :: c :: l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α → α<VAR>hassoc : Associative f<VAR>a b c : α<VAR>l : List α<GOAL>f (f a c) (foldr f b l) = f a (f c (foldr f b l))