ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℤ<VAR>help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1<GOAL>χ₄ ↑(n % ↑4) = if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁴ : OrderedRing α<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>ha : a < 0<GOAL>a • b₁ < a • b₂ ↔ b₂ < b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁴ : OrderedRing α<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : PosSMulStrictMono α β<VAR>inst✝ : PosSMulReflectLT α β<VAR>ha : a < 0<GOAL>-a • b₂ < -a • b₁ ↔ b₂ < b₁
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>hg : Embedding ⇑g<VAR>H : Set.range ⇑f ⊆ Set.range ⇑g<GOAL>IsIso (pullback.fst f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>hg : Embedding ⇑g<VAR>H : Set.range ⇑f ⊆ Set.range ⇑g<VAR>esto : ↑(pullback f g) ≃ₜ ↑X := (Homeomorph.ofEmbedding ⇑(pullback.fst f g) ⋯).trans { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>IsIso (pullback.fst f g)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →ₗ[R] P<VAR>x✝ : DirectLimit G f<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : G i<GOAL>((fun i => F ∘ₗ of R ι G f i) j) ((f i j hij) x) = ((fun i => F ∘ₗ of R ι G f i) i) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →ₗ[R] P<VAR>x✝ : DirectLimit G f<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : G i<GOAL>F ((of R ι G f i) x) = ((fun i => F ∘ₗ of R ι G f i) i) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →ₗ[R] P<VAR>x : DirectLimit G f<GOAL>F x = (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →ₗ[R] P<VAR>x : DirectLimit G f<VAR>h✝ : IsEmpty ι<GOAL>F x = (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>ι : Type v<VAR>inst✝⁶ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁵ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁴ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝³ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝² : AddCommGroup P<VAR>inst✝¹ : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →ₗ[R] P<VAR>x : DirectLimit G f<VAR>h✝ : Nonempty ι<GOAL>F x = (lift R ι G f (fun i => F ∘ₗ of R ι G f i) ⋯) x
<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>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>ν : Measure β<VAR>f : α ≃ᵐ β<VAR>μ : Measure α<VAR>s : Set β<GOAL>s ∈ Filter.map (⇑f) (ae μ) ↔ s ∈ ae (Measure.map (⇑f) μ)
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>f : R' →+* R''<VAR>hf : Function.Injective ⇑f<VAR>χ : MulChar R R'<GOAL>χ.ringHomComp f = ringHomComp 1 f ↔ χ = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : x ∉ closure s<GOAL>𝓝[s] x = ⊥
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>y : ℝ<GOAL>Measure.map (fun ω => y + X ω) ℙ = gaussianReal (μ + y) v
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>y : ℝ<GOAL>Measure.map (fun ω => X ω + y) ℙ = gaussianReal (μ + y) v
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s₁ s₂ : Simplex ℝ P n<VAR>h : Set.range s₁.points = Set.range s₂.points<GOAL>s₁.circumcenter = s₂.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s₁ s₂ : Simplex ℝ P n<VAR>h : Set.range s₁.points = Set.range s₂.points<VAR>hs : s₁.circumcenter ∈ affineSpan ℝ (Set.range s₂.points)<GOAL>s₁.circumcenter = s₂.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s₁ s₂ : Simplex ℝ P n<VAR>h : Set.range s₁.points = Set.range s₂.points<VAR>hs : s₁.circumcenter ∈ affineSpan ℝ (Set.range s₂.points)<VAR>hr : ∀ (i : Fin (n + 1)), dist (s₂.points i) s₁.circumcenter = s₁.circumradius<GOAL>s₁.circumcenter = s₂.circumcenter
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b : R<GOAL>gcd a b = a * gcdA a b + b * gcdB a b
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b : R<VAR>this : EuclideanDomain.P a b (xgcdAux a 1 0 b 0 1)<GOAL>gcd a b = a * gcdA a b + b * gcdB a b
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<GOAL>dlookup a (kinsert a b l) = some b
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>Antitone (lowerCentralSeries G)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ lowerCentralSeries G (n + 1)<GOAL>x ∈ lowerCentralSeries G n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}<GOAL>x ∈ lowerCentralSeries G n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}<GOAL>∀ x ∈ {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}, x ∈ lowerCentralSeries G n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}<VAR>y z : G<VAR>hz : z ∈ lowerCentralSeries G n<VAR>a : G<VAR>ha : z * a * z⁻¹ * a⁻¹ = y<GOAL>y ∈ lowerCentralSeries G n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>n : ℕ<VAR>x : G<VAR>hx : x ∈ closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q, p * q * p⁻¹ * q⁻¹ = x}<VAR>y z : G<VAR>hz : z ∈ lowerCentralSeries G n<VAR>a : G<VAR>ha : z * a * z⁻¹ * a⁻¹ = y<GOAL>z * (a * z⁻¹ * a⁻¹) ∈ lowerCentralSeries G n
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>i✝ i : ℕ<VAR>f : E → F<GOAL>iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>i✝ i : ℕ<VAR>f : E → F<GOAL>iteratedFDerivWithin 𝕜 i (-f) univ x = -iteratedFDerivWithin 𝕜 i f univ x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>r : R<GOAL>nthRoots 2 r = 0 ↔ ¬IsSquare r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : ι →₀ α<VAR>t : ι → Finset α<GOAL>f ∈ s.finsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : ι →₀ α<VAR>t : ι → Finset α<GOAL>(∃ a ∈ s.pi t, { toFun := indicator s, inj' := ⋯ } a = f) → f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : ι →₀ α<VAR>t : ι → Finset α<GOAL>(f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) → ∃ a ∈ s.pi t, { toFun := indicator s, inj' := ⋯ } a = f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Ring k<VAR>inst✝ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i✝ j : ι<VAR>e : ι ≃ ι'<VAR>i : ι<GOAL>(b.coord i) (b i) = 1
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>m : Fin (n + 1) →₀ ℕ<GOAL>m ∈ Finset.image (cons i) (((finSuccEquiv R n) f).coeff i).support ↔ m ∈ Finset.filter (fun m => m 0 = i) f.support
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>m : Fin (n + 1) →₀ ℕ<GOAL>(∃ a ∈ (((finSuccEquiv R n) f).coeff i).support, cons i a = m) ↔ coeff m f ≠ 0 ∧ m 0 = i
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<VAR>m : Fin (n + 1) →₀ ℕ<GOAL>(∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ m 0 = i
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} 𝒳<VAR>inst✝ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>f : p.obj a ⟶ p.obj b<VAR>h : CommSq (p.map φ) (eqToHom ⋯) (eqToHom ⋯) f<GOAL>p.IsHomLift f φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} 𝒳<VAR>inst✝ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>h : CommSq (p.map φ) (eqToHom ⋯) (eqToHom ⋯) (p.map φ)<GOAL>p.IsHomLift (p.map φ) φ
<VAR>R : Type u<VAR>inst₁ inst₂ : Ring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h₁ : toSemiring = toSemiring<VAR>h₂ : toNonAssocRing = toNonAssocRing<GOAL>inst₁ = inst₂
<VAR>R : Type u<VAR>inst₁ inst₂ : Ring R<VAR>h_add : HAdd.hAdd = HAdd.hAdd<VAR>h_mul : HMul.hMul = HMul.hMul<VAR>h₁ : toSemiring = toSemiring<VAR>h₂ : toNonAssocRing = toNonAssocRing<VAR>h₃ : AddGroup.toSubNegMonoid = AddGroup.toSubNegMonoid<GOAL>inst₁ = inst₂
<VAR>α : Type u_1<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>a : α<VAR>ha : a < 0<GOAL>sign a = -1
<VAR>x y : EReal<GOAL>(x * y).abs = x.abs * y.abs
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<VAR>degree_g_lt : g.degree < ↑s.card<VAR>eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g<GOAL>f = g
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f.degree < ↑s.card<VAR>degree_g_lt : g.degree < ↑s.card<VAR>eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g<GOAL>(f - g).degree < ↑s.card
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>ι : Type u_2<VAR>v : ι → R<VAR>s : Finset ι<VAR>hvs : Set.InjOn v ↑s<VAR>degree_f_lt : f ∈ degreeLT R s.card<VAR>degree_g_lt : g ∈ degreeLT R s.card<VAR>eval_fg : ∀ i ∈ s, eval (v i) f = eval (v i) g<GOAL>f - g ∈ degreeLT R s.card
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<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✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>f : M →ₗ[R] M'<VAR>this : (p : Submodule R M) → DecidableEq (M ⧸ p)<GOAL>lift.{u, v} (Module.rank R ↥(LinearMap.range f)) + lift.{v, u} (Module.rank R ↥(LinearMap.ker f)) = lift.{v, u} (Module.rank R M)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>C : (r : A) → r ∈ M * N → Prop<VAR>mem_mul_mem : ∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N), C (m * n) ⋯<VAR>add : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) ⋯<VAR>r : A<VAR>hr : r ∈ M * N<GOAL>C r hr
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>C : (r : A) → r ∈ M * N → Prop<VAR>mem_mul_mem : ∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N), C (m * n) ⋯<VAR>add : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) ⋯<VAR>r : A<VAR>hr : r ∈ M * N<GOAL>∃ (x : r ∈ M * N), C r x
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<GOAL>a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀
<VAR>x : ℚ<VAR>x✝ : ∃ q, q * q = x<VAR>n : ℚ<VAR>hn : n * n = x<GOAL>sqrt x * sqrt x = x
<VAR>x : ℕ<VAR>h : ↑x = ⊤<GOAL>¬(↑x).Dom = ⊤.Dom
<VAR>x : ℕ<VAR>h : ↑x = ⊤<GOAL>¬True = ⊤.Dom
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : CommSemiring A'<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R A'<VAR>inst✝² : Algebra R B<VAR>p✝ q : R[X]<VAR>x✝ : A<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Algebra R S<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : S<GOAL>(aeval x) p = ∑ i ∈ range n, p.coeff i • x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : CommSemiring A'<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R A'<VAR>inst✝² : Algebra R B<VAR>p✝ q : R[X]<VAR>x✝ : A<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Algebra R S<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<VAR>x : S<GOAL>(aeval x) p = ∑ x_1 ∈ range n, (algebraMap R S) (p.coeff x_1) * x ^ x_1
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>f : (i : ι) → κ i → α<GOAL>Disjoint (⨆ i, ⨆ j, f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>c : K[X]ˣ<GOAL>LinearMap.ker ((aeval f) ↑c) = ⊥
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>c : K[X]ˣ<GOAL>LinearMap.ker ((aeval f) (C ((↑c).coeff 0))) = ⊥
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>c : K[X]ˣ<GOAL>LinearMap.ker ((algebraMap K (End K V)) ((↑c).coeff 0)) = ⊥
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>c : K[X]ˣ<GOAL>(↑c).coeff 0 ≠ 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>g : F ≃ₗᵢ[𝕜] G<VAR>f : E → F<VAR>x : E<VAR>i : ℕ<GOAL>‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>g : F ≃ₗᵢ[𝕜] G<VAR>f : E → F<VAR>x : E<VAR>i : ℕ<GOAL>‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ x‖
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>h : ⊤.FG<GOAL>S.FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>h : ⊤.FG<GOAL>(map S.val ⊤).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>h : S.FG<GOAL>(map S.val ⊤).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>h : S.FG<GOAL>S.FG
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.coeff n ≠ 0<GOAL>n ≤ p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.coeff n ≠ 0<GOAL>p ≠ 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m✝ : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSimpleModule R M<VAR>m : M<VAR>hm : m ≠ 0<GOAL>Function.Surjective ⇑(toSpanSingleton R M m)
<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✝⁴ : SeminormedGroup E<VAR>inst✝³ : SeminormedGroup F<VAR>inst✝² : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : T0Space E<VAR>a : E<GOAL>‖a‖ ≤ 0 ↔ a = 1
<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✝⁴ : SeminormedGroup E<VAR>inst✝³ : SeminormedGroup F<VAR>inst✝² : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : T0Space E<VAR>a : E<VAR>this : NormedGroup E := let __src := inst✝⁴; NormedGroup.mk ⋯<GOAL>‖a‖ ≤ 0 ↔ a = 1
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) 1
<VAR>a : UnitAddCircle<GOAL>DifferentiableAt ℂ (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ + hurwitzZetaOdd a s) 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s✝¹ t : Set α<VAR>p q : α → Prop<VAR>s : Set (Set α)<VAR>hs : s.Finite<VAR>a✝ : Set α<VAR>s✝ : Set (Set α)<VAR>x✝¹ : a✝ ∉ s✝<VAR>x✝ : s✝.Finite<VAR>his : ⋃₀ s✝ ∈ f ↔ ∃ t ∈ s✝, t ∈ f<GOAL>⋃₀ insert a✝ s✝ ∈ f ↔ ∃ t ∈ insert a✝ s✝, t ∈ f
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>(-x).Equiv (-y) ↔ x.Equiv y
<VAR>x : ℝ≥0∞<GOAL>↑x = 1 ↔ x = 1
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>x : ι → α<VAR>f : Filter α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f<GOAL>Tendsto x l f
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>x : ι → α<VAR>f : Filter α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>hxy : ¬Tendsto x l f<GOAL>∃ ns, Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun n => x (ns (ms n))) atTop f
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>x : ι → α<VAR>f : Filter α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>hxy : ¬Tendsto x l f<VAR>s : Set α<VAR>hs : s ∈ f<VAR>hfreq : ∃ᶠ (n : ι) in l, x n ∉ s<GOAL>∃ ns, Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun n => x (ns (ms n))) atTop f
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>x : ι → α<VAR>f : Filter α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>hxy : ¬Tendsto x l f<VAR>s : Set α<VAR>hs : s ∈ f<VAR>hfreq : ∃ᶠ (n : ι) in l, x n ∉ s<VAR>y : ℕ → ι<VAR>hy_tendsto : Tendsto y atTop l<VAR>hy_freq : ∀ (n : ℕ), x (y n) ∉ s<GOAL>∃ ns, Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun n => x (ns (ms n))) atTop f
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>x : ι → α<VAR>f : Filter α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>hxy : ¬Tendsto x l f<VAR>s : Set α<VAR>hs : s ∈ f<VAR>hfreq : ∃ᶠ (n : ι) in l, x n ∉ s<VAR>y : ℕ → ι<VAR>hy_tendsto : Tendsto y atTop l<VAR>hy_freq : ∀ (n : ℕ), x (y n) ∉ s<VAR>ms : ℕ → ℕ<VAR>hms_tendsto : Tendsto (fun n => x (y (ms n))) atTop f<GOAL>False