ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>h : p.natDegree = q.natDegree<VAR>n : ℕ<GOAL>(p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n) * r ^ (p.natDegree - (p + q).natDegree) = (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>h : p.natDegree = q.natDegree<VAR>n : ℕ<GOAL>(p.coeff n + q.coeff n) * r ^ ((p + q).natDegree - n + (p.natDegree - (p + q).natDegree)) = (p.coeff n + q.coeff n) * r ^ (p.natDegree - n)
<VAR>n : ℕ<VAR>hn0 : n ≠ 0<GOAL>∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
<VAR>n : ℕ<VAR>hn0 : n ≠ 0<VAR>h : 511 < n<GOAL>∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
<VAR>n : ℕ<VAR>hn0 : n ≠ 0<VAR>h : n ≤ 511<GOAL>∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
<VAR>n : ℕ<VAR>hn0 : n ≠ 0<GOAL>n < 521 → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((PreservesCoequalizer.iso (tensorLeft R.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫ colimMap (parallelPairHom (R.X ◁ R.mul ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ R.mul ▷ R.X ▷ P.X) ((α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X) ⋯ ⋯)) ≫ coequalizer.desc P.actLeft ⋯ = R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(tensorLeft R.X).map (coequalizer.π ({ X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷ P.X) ((α_ { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X R.X P.X).hom ≫ { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁ P.actLeft)) ≫ ((PreservesCoequalizer.iso (tensorLeft R.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫ colimMap (parallelPairHom (R.X ◁ R.mul ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ R.mul ▷ R.X ▷ P.X) ((α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X) ⋯ ⋯)) ≫ coequalizer.desc P.actLeft ⋯ = (tensorLeft R.X).map (coequalizer.π ({ X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷ P.X) ((α_ { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X R.X P.X).hom ≫ { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁ P.actLeft)) ≫ R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>R.X ◁ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ ((PreservesCoequalizer.iso (tensorLeft R.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫ colimMap (parallelPairHom (R.X ◁ R.mul ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ R.mul ▷ R.X ▷ P.X) ((α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X) ⋯ ⋯)) ≫ coequalizer.desc P.actLeft ⋯ = R.X ◁ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X) ≫ P.actLeft = R.X ◁ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft = R.X ◁ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫ R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft = R.X ◁ P.actLeft ≫ P.actLeft
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<GOAL>seminormFromConst' hf1 hc hpm 1 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<GOAL>seminormFromConst_seq c f 1 =ᶠ[atTop] fun x => 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<GOAL>∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f 1 b = 1
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Z.Opens<VAR>V : X.Opens<VAR>e : V ≤ (f ≫ g) ⁻¹ᵁ U<GOAL>Hom.appLE (f ≫ g) U V e = Hom.app g U ≫ Hom.appLE f (g ⁻¹ᵁ U) V e
<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 : f₁ =ᶠ[𝓝 x] f<GOAL>fderiv 𝕜 f₁ x = fderiv 𝕜 f x
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PosMulMono α<VAR>ha : 0 ≤ a<VAR>h : 1 ≤ b<GOAL>a ≤ a * b
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<GOAL>∑ x ∈ antidiagonal (p.natDegree + q.natDegree), p.coeff x.1 * q.coeff x.2 = p.coeff p.natDegree * q.coeff q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<GOAL>∀ b ∈ antidiagonal (p.natDegree + q.natDegree), b ≠ (p.natDegree, q.natDegree) → p.coeff b.1 * q.coeff b.2 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<GOAL>(p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree) → p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f✝ : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α β<VAR>f : β → γ<VAR>g : β → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>x : α<VAR>s : Set δ<VAR>hs : MeasurableSet s<GOAL>((κ.map (fun x => (f x, g x)) ⋯).snd x) s = ((κ.map g hg) x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f✝ : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α β<VAR>f : β → γ<VAR>g : β → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>x : α<VAR>s : Set δ<VAR>hs : MeasurableSet s<GOAL>(κ x) ((fun x => (f x, g x)) ⁻¹' {p | p.2 ∈ s}) = (κ x) (g ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f✝ : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α β<VAR>f : β → γ<VAR>g : β → δ<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>x : α<VAR>s : Set δ<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.2 ∈ s}
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ : α → ℝ<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>f : α → ℝ<VAR>s : Set α<GOAL>(μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>0 < (a * a₁⁻¹).x
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>d * (a.y * a₁.y) < a.x * a₁.x
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.x * (d * (a.y * a₁.y)) < a.x * (a.x * a₁.x)
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>d * a.y * (a.x * a₁.y) < a.x * (a.x * a₁.x)
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>d * a.y * (a.y * a₁.x) < a.x * (a.x * a₁.x)
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>0 < a.x * (a.x * a₁.x) - (a.x ^ 2 - 1) * a₁.x
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>0 < a₁.x
<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>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>(monomial (s + Finsupp.single n e)) a = (monomial s) a * X n ^ e
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>hf : UniformContinuous f<VAR>g : SeparationQuotient α → SeparationQuotient β<VAR>comm : mk ∘ f = g ∘ mk<VAR>x✝ : SeparationQuotient α<VAR>a : α<GOAL>map f (Quot.mk Setoid.r a) = g (Quot.mk Setoid.r a)
<VAR>α : Type u<VAR>β : Type v<VAR>r✝ : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>¬Bounded r s ↔ Unbounded r s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>vanishingIdeal ∅ = ⊤
<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✝² : Zero N<VAR>inst✝¹ : DecidableEq M<VAR>inst✝ : Zero M<VAR>f g : α →₀ N<VAR>F : N → M<VAR>F0 : F 0 = 0<VAR>x : α<GOAL>x ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → x ∈ f.neLocus g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>sup f = 0 ↔ ∀ (i : ι), f i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : sup f = 0<VAR>i : ι<GOAL>f i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : sup f = 0<VAR>i : ι<GOAL>f i ≤ sup f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Subsingleton B<VAR>a✝ : Nontrivial A<GOAL>minpoly A x = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Subsingleton B<VAR>a✝ : Nontrivial A<VAR>this : (minpoly A x).degree ≤ degree 1<GOAL>minpoly A x = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Subsingleton B<VAR>a✝ : Nontrivial A<VAR>this : (minpoly A x).degree ≤ 0<GOAL>minpoly A x = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Subsingleton B<VAR>a✝ : Nontrivial A<VAR>this : (minpoly A x).degree ≤ 0<VAR>h : (minpoly A x).degree ≤ 0<GOAL>minpoly A x = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Subsingleton B<VAR>a✝ : Nontrivial A<VAR>this : (minpoly A x).degree ≤ 0<VAR>h : 0 < (minpoly A x).degree<GOAL>minpoly A x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t✝ s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>m : ℕ → Measure α<VAR>hv : ∀ (n : ℕ), (m n) t ≠ ⊤<VAR>hμ : μ = sum m<GOAL>μ (toMeasurable μ t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t✝ s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>m : ℕ → Measure α<VAR>hv : ∀ (n : ℕ), (m n) t ≠ ⊤<VAR>hμ : μ = sum m<VAR>A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)<GOAL>μ (toMeasurable μ t ∩ s) = μ (t ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t✝ s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>m : ℕ → Measure α<VAR>hv : ∀ (n : ℕ), (m n) t ≠ ⊤<VAR>hμ : μ = sum m<VAR>A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)<GOAL>μ ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t then h.choose else if h' : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ ∀ (u : Set α), MeasurableSet u → μ (t_1 ∩ u) = μ (t ∩ u) then h'.choose else ⋯.choose) ∩ s) = μ (t ∩ s)
<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>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)<GOAL>HasStrictFDerivAt (fun f => f i) (proj i) f
<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>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)<VAR>h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f<GOAL>HasStrictFDerivAt (fun f => f i) (proj i) f
<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>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)<VAR>h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f<VAR>h' : (proj i).comp id' = proj i<GOAL>HasStrictFDerivAt (fun f i' => f i') id' f
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>f ∈ degreeLT R n ↔ f.degree < ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>(∀ (i : ℕ), f ∈ ⨅ (_ : i ≥ n), LinearMap.ker (lcoeff R i)) ↔ f.degree < ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>(∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ f.degree < ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>(∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ f.support.sup WithBot.some < ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>(∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ b ∈ f.support, ↑b < ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>⊥ < ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>f : R[X]<GOAL>(∀ i ≥ n, f ∈ LinearMap.ker (lcoeff R i)) ↔ ∀ (b : ℕ), n ≤ b → f.coeff b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice β<VAR>S : Set (Set α)<VAR>f : α → β<GOAL>⨆ x ∈ ⋃₀ S, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<VAR>M : Type v<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>Mono f ↔ Function.Injective ⇑f
<VAR>y : ℝ<VAR>h : 0 < y<VAR>x : ℝ≥0<GOAL>ContinuousAt (fun a => a ^ y) ↑x
<VAR>y : ℝ<VAR>h : 0 < y<VAR>x : ℝ≥0<GOAL>ContinuousAt ((fun a => a ^ y) ∘ ofNNReal) x
<VAR>y : ℝ<VAR>h : 0 < y<VAR>x : ℝ≥0<GOAL>(fun a => a ^ y) ∘ ofNNReal = ofNNReal ∘ fun z => z ^ y
<VAR>y : ℝ<VAR>h : 0 < y<VAR>x✝ x : ℝ≥0<GOAL>((fun a => a ^ y) ∘ ofNNReal) x = (ofNNReal ∘ fun z => z ^ y) x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>ab : a ≠ b<VAR>c d : α<VAR>cd : c ≠ d<VAR>ac : ¬a = c<GOAL>swap a b * swap c d ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>ab : a ≠ b<VAR>c d : α<VAR>cd : c ≠ d<VAR>ac : ¬a = c<VAR>h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)<GOAL>swap a b * swap c d ∈ closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>ab : a ≠ b<VAR>c d : α<VAR>cd : c ≠ d<VAR>ac : ¬a = c<VAR>h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)<GOAL>swap a b * swap a c * (swap c a * swap c d) ∈ closure {σ | σ.IsThreeCycle}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<GOAL>finrank K ↥V = (charpoly φ).natTrailingDegree
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<GOAL>finrank K ↥V = (charpoly φ).natTrailingDegree
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<GOAL>finrank K ↥V = (charpoly φ).natTrailingDegree
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>M : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : IsDomain R<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module K M<VAR>inst✝ : Module.Finite K M<VAR>φ : Module.End K M<VAR>V : Submodule K M := φ.maxGenEigenspace 0<VAR>hV : V = ⨆ n, ker (φ ^ n)<VAR>W : Submodule K M := ⨅ n, range (φ ^ n)<VAR>hVW : IsCompl V W<VAR>hφV : ∀ x ∈ V, φ x ∈ V<VAR>hφW : ∀ x ∈ W, φ x ∈ W<GOAL>finrank K ↥V = (charpoly φ).natTrailingDegree