ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>finrank R M = 0 ↔ Subsingleton M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>finrank R M = 0 ↔ ↑(finrank R M) = 0
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>h : IsClosed ↑A<VAR>f g : ↥A<GOAL>↑f ⊔ ↑g ∈ A
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>h : IsClosed ↑A<VAR>f g : ↥A<GOAL>A = A.topologicalClosure
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>h : IsClosed ↑A<VAR>f g : ↥A<GOAL>↑A = ↑A.topologicalClosure
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>h : IsClosed ↑A<VAR>f g : ↥A<GOAL>↑A.topologicalClosure = ↑A
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>h : IsClosed ↑A<VAR>f g : ↥A<GOAL>IsClosed ↑A.toSubsemiring
<VAR>n✝ n e : ℕ<GOAL>0 < e → n < 10 ^ e → n.repr.length ≤ e
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : PosMulMono α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>h1 : a < c<VAR>h2 : b < d<VAR>h3 : 0 ≤ a<VAR>h4 : 0 ≤ b<VAR>b0 : 0 = b<GOAL>a * b < c * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : PosMulMono α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>h1 : a < c<VAR>h2 : b < d<VAR>h3 : 0 ≤ a<VAR>h4 : 0 ≤ b<VAR>b0 : 0 = b<GOAL>0 < c * d
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<VAR>a b : α<GOAL>(fun x => x * b) '' t = (fun x => x * b⁻¹) ⁻¹' t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>a✝ : ℕ<GOAL>a✝ ∈ (p.scaleRoots s).support → a✝ ∈ p.support
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.46156, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X✝ Y✝ : (HomologicalComplex Vᵒᵖ c)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>i j : ι<VAR>x✝ : c.symm.Rel i j<GOAL>(fun i => (f.unop.f i).unop) i ≫ ((fun X => (unop X).unop) Y✝).d i j = ((fun X => (unop X).unop) X✝).d i j ≫ (fun i => (f.unop.f i).unop) j
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : StrongRankCondition R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module.Free R M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module.Free R M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module.Free R M₁<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Finite R M'<VAR>cond : finrank R M = finrank R M'<GOAL>lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℝ<GOAL>0 ≤ stieltjesFunctionAux f a r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℝ<VAR>this : Nonempty { r' // r < ↑r' }<GOAL>0 ≤ stieltjesFunctionAux f a r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>r : ℝ<VAR>this : Nonempty { r' // r < ↑r' }<GOAL>0 ≤ ⨅ q, f a ↑q
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>η : Type u_8<VAR>s : Set η<VAR>t : η → Set M<VAR>hs : DirectedOn (t ⁻¹'o fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, LinearIndependent R fun (x : ↑(t a)) => ↑x<GOAL>LinearIndependent R fun (x : ↑(⋃ a ∈ s, t a)) => ↑x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>η : Type u_8<VAR>s : Set η<VAR>t : η → Set M<VAR>hs : DirectedOn (t ⁻¹'o fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, LinearIndependent R fun (x : ↑(t a)) => ↑x<GOAL>LinearIndependent R fun (x : ↑(⋃ x, t ↑x)) => ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>ContinuousWithinAt (stieltjesFunctionAux f a) (Ici x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (sInf (stieltjesFunctionAux f a '' Ioi x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<GOAL>ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ a_1, stieltjesFunctionAux f a ↑a_1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<VAR>h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r<GOAL>ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ a_1, stieltjesFunctionAux f a ↑a_1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<VAR>h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r<VAR>h'' : ⨅ r, stieltjesFunctionAux f a ↑↑r = ⨅ r, f a ↑r<GOAL>ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ a_1, stieltjesFunctionAux f a ↑a_1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>x : ℝ<VAR>h' : ⨅ r, stieltjesFunctionAux f a ↑r = ⨅ r, stieltjesFunctionAux f a ↑↑r<VAR>h'' : ⨅ r, stieltjesFunctionAux f a ↑↑r = ⨅ r, f a ↑r<GOAL>stieltjesFunctionAux f a x = ⨅ r, f a ↑r
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>xn a1 (n * 0) ≡ xn a1 n ^ 0 [MOD yn a1 n ^ 2] ∧ yn a1 (n * 0) ≡ 0 * xn a1 n ^ (0 - 1) * yn a1 n [MOD yn a1 n ^ 3]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<VAR>hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]<VAR>hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]<GOAL>xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧ yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<VAR>hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]<VAR>hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]<VAR>L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]<GOAL>xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧ yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<VAR>hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]<VAR>hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]<VAR>L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]<VAR>R : xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]<GOAL>xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧ yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n k : ℕ<VAR>hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]<VAR>hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]<VAR>L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]<VAR>R : xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]<GOAL>xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n [MOD yn a1 n ^ 2] ∧ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_4, u_3} C<VAR>inst✝ : HasZeroMorphisms C<VAR>K L : HomologicalComplex C c'<VAR>e' : K ≅ L<VAR>e : c.Embedding c'<VAR>h : K.IsStrictlySupportedOutside e<VAR>i : ι<GOAL>K.ExactAt (e.f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_4, u_3} C<VAR>inst✝ : HasZeroMorphisms C<VAR>K L : HomologicalComplex C c'<VAR>e' : K ≅ L<VAR>e : c.Embedding c'<VAR>h : K.IsStrictlySupportedOutside e<VAR>i : ι<GOAL>(K.sc (e.f i)).Exact
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝² : DecidableRel r<VAR>inst✝¹ : IsTotal α r<VAR>inst✝ : IsTrans α r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>e : (a :: b :: l).split = (l₁, l₂)<GOAL>Sorted r (mergeSort r (a :: b :: l))
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝² : DecidableRel r<VAR>inst✝¹ : IsTotal α r<VAR>inst✝ : IsTrans α r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>e : (a :: b :: l).split = (l₁, l₂)<VAR>h₁ : l₁.length < (a :: b :: l).length<VAR>h₂ : l₂.length < (a :: b :: l).length<GOAL>Sorted r (mergeSort r (a :: b :: l))
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝² : DecidableRel r<VAR>inst✝¹ : IsTotal α r<VAR>inst✝ : IsTrans α r<VAR>a b : α<VAR>l l₁ l₂ : List α<VAR>e : (a :: b :: l).split = (l₁, l₂)<VAR>h₁ : l₁.length < (a :: b :: l).length<VAR>h₂ : l₂.length < (a :: b :: l).length<GOAL>Sorted r (merge (fun x x_1 => decide (r x x_1)) (mergeSort r l₁) (mergeSort r l₂))
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>x : R<VAR>s : ↥M<GOAL>mk' S x s ∈ Ideal.map (algebraMap R S) I ↔ ∃ s ∈ M, s * x ∈ I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>x : R<VAR>s : ↥M<GOAL>(∃ x_1, (algebraMap R S) x * (algebraMap R S) ↑x_1.2 = (algebraMap R S) ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsLocalization M S<VAR>I : Ideal R<VAR>x : R<VAR>s : ↥M<GOAL>(∃ x_1 c, ↑(c * x_1.2) * x = ↑c * ↑x_1.1) ↔ ∃ s ∈ M, s * x ∈ I
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<GOAL>a / c ≤ b / c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hab : a ≤ b<VAR>hc : 0 ≤ c<GOAL>a * (1 / c) ≤ b * (1 / c)
<VAR>x y : ℝ≥0∞<VAR>h : x < y<GOAL>(if x = 0 then ⊥ else if x = ⊤ then ⊤ else ↑(Real.log x.toReal)) < if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)
<VAR>y : ℝ≥0∞<VAR>h : 0 < y<GOAL>(if 0 = 0 then ⊥ else if 0 = ⊤ then ⊤ else ↑(Real.log (ENNReal.toReal 0))) < if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)
<VAR>y : ℝ≥0∞<VAR>h : ⊤ < y<GOAL>(if ⊤ = 0 then ⊥ else if ⊤ = ⊤ then ⊤ else ↑(Real.log ⊤.toReal)) < if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)
<VAR>x y : ℝ≥0∞<VAR>h : x < y<VAR>x_real : 0 < x.toReal<GOAL>(if x = 0 then ⊥ else if x = ⊤ then ⊤ else ↑(Real.log x.toReal)) < if y = 0 then ⊥ else if y = ⊤ then ⊤ else ↑(Real.log y.toReal)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)<GOAL>v ∈ LinearMap.ker ((aeval f) (p * q))
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)<VAR>x : M<VAR>hx : x ∈ LinearMap.ker ((aeval f) p)<VAR>y : M<VAR>hy : y ∈ LinearMap.ker ((aeval f) q)<VAR>hxy : x + y = v<GOAL>v ∈ LinearMap.ker ((aeval f) (p * q))
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)<VAR>x : M<VAR>hx : x ∈ LinearMap.ker ((aeval f) p)<VAR>y : M<VAR>hy : y ∈ LinearMap.ker ((aeval f) q)<VAR>hxy : x + y = v<VAR>h_eval_x : ((aeval f) (p * q)) x = 0<GOAL>v ∈ LinearMap.ker ((aeval f) (p * q))
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : M →ₗ[R] M<VAR>p q : R[X]<VAR>v : M<VAR>hv : v ∈ LinearMap.ker ((aeval f) p) ⊔ LinearMap.ker ((aeval f) q)<VAR>x : M<VAR>hx : x ∈ LinearMap.ker ((aeval f) p)<VAR>y : M<VAR>hy : y ∈ LinearMap.ker ((aeval f) q)<VAR>hxy : x + y = v<VAR>h_eval_x : ((aeval f) (p * q)) x = 0<VAR>h_eval_y : ((aeval f) (p * q)) y = 0<GOAL>v ∈ LinearMap.ker ((aeval f) (p * q))
<VAR>p q : ℚ≥0<VAR>hn : p.num = q.num<VAR>hd : p.den = q.den<GOAL>p = q
<VAR>p q : ℚ≥0<VAR>hn : p.num = q.num<VAR>hd : p.den = q.den<GOAL>(↑p).num = (↑q).num
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ last n<GOAL>(i.castPred h).castSucc = i
<VAR>n m : ℕ<VAR>y : Fin n<VAR>h : y.castSucc ≠ last n<GOAL>(y.castSucc.castPred h).castSucc = y.castSucc
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α✝<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u : Set α✝<VAR>α : Type u_1<VAR>s t : Set α<GOAL>¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>inst✝⁷ : SeminormedAddCommGroup E<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₂<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι : Type u_5<VAR>inst✝ : CompleteSpace E<VAR>g : ι → E →SL[σ₁₂] F<VAR>h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C<GOAL>∃ C', ∀ (i : ι), ‖g i‖ ≤ C'
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>inst✝⁷ : SeminormedAddCommGroup E<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₂<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι : Type u_5<VAR>inst✝ : CompleteSpace E<VAR>g : ι → E →SL[σ₁₂] F<VAR>h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C<GOAL>UniformEquicontinuous (DFunLike.coe ∘ g)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>inst✝⁷ : SeminormedAddCommGroup E<VAR>inst✝⁶ : SeminormedAddCommGroup F<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜₂<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι : Type u_5<VAR>inst✝ : CompleteSpace E<VAR>g : ι → E →SL[σ₁₂] F<VAR>h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C<VAR>x✝ : Fin 1<VAR>x : E<GOAL>BddAbove (range fun i => (normSeminorm 𝕜₂ F) ((g i) x))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>mapFun (⇑f) (x * y) = mapFun (⇑f) x * mapFun (⇑f) y
<VAR>x : ℝ<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<GOAL>a ≤ b ↔ ∃ c, b = c * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>g : α → (a : δ) → π a<GOAL>Measurable g ↔ ∀ (a : δ), Measurable fun x => g x a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L : List (List α)<GOAL>L.join.length = Nat.sum (map length L)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>C : ℝ<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>C c : ℝ<VAR>hc_mem : c ∈ Set.Ioo 0 1<VAR>hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), C ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>C c : ℝ<VAR>hc_mem : c ∈ Set.Ioo 0 1<VAR>hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)<VAR>n : ℕ<VAR>hn₁ : ⌈C / c⌉₊ ≤ n<VAR>hn₂ : ∀ (i : α), c * ↑n ≤ ↑(r i n)<GOAL>∀ (i : α), C ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>C c : ℝ<VAR>hc_mem : c ∈ Set.Ioo 0 1<VAR>hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)<VAR>n : ℕ<VAR>hn₁ : ⌈C / c⌉₊ ≤ n<VAR>hn₂ : ∀ (i : α), c * ↑n ≤ ↑(r i n)<VAR>h₁ : 0 < c<GOAL>∀ (i : α), C ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>C c : ℝ<VAR>hc_mem : c ∈ Set.Ioo 0 1<VAR>hc : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)<VAR>n : ℕ<VAR>hn₁ : ⌈C / c⌉₊ ≤ n<VAR>hn₂ : ∀ (i : α), c * ↑n ≤ ↑(r i n)<VAR>h₁ : 0 < c<VAR>i : α<GOAL>C ≤ ↑(r i n)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P R<VAR>t : x.Compatible<VAR>f : Y ⟶ X<VAR>hf : R f<GOAL>x.sieveExtend f ⋯ = x f hf
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>x : FamilyOfElements P R<VAR>t : x.Compatible<VAR>f : Y ⟶ X<VAR>hf : R f<VAR>h : ∃ h g, R g ∧ h ≫ g = f<GOAL>x.sieveExtend f ⋯ = x f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>a b : α<GOAL>(∀ c ∈ s(a, b), p c) ↔ p a ∧ p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>a b : α<VAR>h : p a ∧ p b<VAR>c : α<VAR>hc : c ∈ s(a, b)<GOAL>p c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>b c : α<VAR>h : p c ∧ p b<VAR>hc : c ∈ s(c, b)<GOAL>p c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>a c : α<VAR>h : p a ∧ p c<VAR>hc : c ∈ s(a, c)<GOAL>p c
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommRing R<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : DecidableEq n<VAR>A : (Matrix n n R)ˣ<GOAL>(↑A).rank = Fintype.card n
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommRing R<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : DecidableEq n<VAR>A : (Matrix n n R)ˣ<GOAL>Fintype.card n ≤ (↑A).rank
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype o<VAR>inst✝² : CommRing R<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : DecidableEq n<VAR>A : (Matrix n n R)ˣ<VAR>this : (↑A * ↑A⁻¹).rank ≤ (↑A).rank<GOAL>Fintype.card n ≤ (↑A).rank
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m * m < n * n ↔ m < n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<GOAL>(erase a f).update a b = f.update a b
<VAR>a b c : Ordinal.{u}<GOAL>b ♯ c ≤ a ↔ (∀ b' < b, b' ♯ c < a) ∧ ∀ c' < c, b ♯ c' < a
<VAR>a b c : Ordinal.{u}<GOAL>max (b.blsub fun a' x => a' ♯ c) (c.blsub fun b' x => b ♯ b') ≤ a ↔ (∀ b' < b, b' ♯ c < a) ∧ ∀ c' < c, b ♯ c' < a
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<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>τ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<GOAL>Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g : α → M<VAR>a✝ a : α<GOAL>s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ mulSupport f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>inst✝ : (x : α) → DecidablePred (p x)<VAR>N : ℕ<VAR>hN : ∀ k ≤ N, MeasurableSet {x | p x k}<GOAL>Measurable fun x => Nat.findGreatest (p x) N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>inst✝ : (x : α) → DecidablePred (p x)<VAR>N : ℕ<VAR>hN : ∀ k ≤ N, MeasurableSet {x | p x k}<VAR>k : ℕ<VAR>hk : k ≤ N<GOAL>MeasurableSet {x | Nat.findGreatest (p x) N = k}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>p : α → ℕ → Prop<VAR>inst✝ : (x : α) → DecidablePred (p x)<VAR>N : ℕ<VAR>hN : ∀ k ≤ N, MeasurableSet {x | p x k}<VAR>k : ℕ<VAR>hk : k ≤ N<GOAL>MeasurableSet ({a | k ≤ N} ∩ ((⋂ (_ : k ≠ 0), {x | p x k}) ∩ ⋂ i, ⋂ (_ : k < i), ⋂ (_ : i ≤ N), {a | p a i}ᶜ))
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : i < j<GOAL>i.cycleRange j = j
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : i < j<GOAL>j ∉ Set.range ⇑(castLEEmb ⋯)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>f g : R[X]<GOAL>(f - g).coeff n = f.coeff n - g.coeff n