ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<GOAL>IsOpen (Iic a)ᶜ
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁸ : Nonempty ι<VAR>inst✝⁷ : Nonempty ι'<VAR>inst✝⁶ : NormedField 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : NormedField 𝕜₂<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : SeminormFamily 𝕜 E ι<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>e : ι' ≃ ι<GOAL>WithSeminorms (p ∘ ⇑e)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : MeasurableSpace Ω'<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω'<VAR>inst✝ : BorelSpace Ω'<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>Continuous fun ν => ν.map ⋯
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : MeasurableSpace Ω'<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω'<VAR>inst✝ : BorelSpace Ω'<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>∀ (x : ProbabilityMeasure Ω), ContinuousAt (fun ν => ν.map ⋯) x
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>hS : S ≤ IsUnit.submonoid M<VAR>x : ↥S<GOAL>↑x * ↑((S.leftInvEquiv hS).symm x) = 1
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>A B : StructuredArrow S T<VAR>f : A ⟶ B<GOAL>A.hom ≫ T.map f.right = B.hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>A B : StructuredArrow S T<VAR>f : A ⟶ B<VAR>this : (Functor.fromPUnit S).map f.left ≫ B.hom = A.hom ≫ T.map f.right<GOAL>A.hom ≫ T.map f.right = B.hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>Mem.other h ∈ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>z : Sym2 α<VAR>h : a ∈ z<GOAL>z = s(a, Mem.other h)
<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✝² : DecidableEq M<VAR>inst✝¹ : Zero M<VAR>inst✝ : Zero N<VAR>f g : α →₀ N<VAR>F : N → M<VAR>F0 : F 0 = 0<VAR>hF : Function.Injective F<VAR>a✝ : α<GOAL>a✝ ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a✝ ∈ f.neLocus g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s✝ t : Set α<VAR>s : Finset (α × β)<VAR>f : α × β → M<GOAL>∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a : ℝ≥0<VAR>g : ι → ℝ≥0<VAR>h : ℝ≥0<VAR>H : ∀ (i : ι), g i * h ≤ a<GOAL>iSup g * h ≤ a
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a : ℝ≥0<VAR>g : ι → ℝ≥0<VAR>h : ℝ≥0<VAR>H : ∀ (i : ι), g i * h ≤ a<GOAL>⨆ i, g i * h ≤ a
<VAR>n : ℕ<GOAL>Nat.shiftLeft' false 1 n = 2 ^ n
<VAR>a x✝ z x : ℂ<GOAL>((starRingEnd ℂ) x).arg = if x.arg = π then π else -x.arg
<VAR>a x✝ z x : ℂ<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : x.re < 0<VAR>hi : x.im < 0<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : x.re < 0<VAR>hi : x.im = 0<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : x.re < 0<VAR>hi : 0 < x.im<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : x.re = 0<VAR>hi : x.im < 0<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : x.re = 0<VAR>hi : x.im = 0<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : x.re = 0<VAR>hi : 0 < x.im<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : 0 < x.re<VAR>hi : x.im < 0<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : 0 < x.re<VAR>hi : x.im = 0<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>a x✝ z x : ℂ<VAR>hr : 0 < x.re<VAR>hi : 0 < x.im<GOAL>(if 0 ≤ x.re then -Real.arcsin (x.im / abs x) else if 0 ≤ -x.im then Real.arcsin (x.im / abs x) + π else Real.arcsin (x.im / abs x) - π) = if x.re < 0 ∧ x.im = 0 then π else -if 0 ≤ x.re then Real.arcsin (x.im / abs x) else if 0 ≤ x.im then -Real.arcsin (x.im / abs x) + π else -Real.arcsin (x.im / abs x) - π
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.neg P = ![P x, -P y, 0]
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<VAR>y : R<GOAL>(X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<VAR>y : R<VAR>H : ((expand R (p ^ n)) (X - C y)).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) (X - C y).roots<GOAL>(X ^ p ^ n - C y).roots = p ^ n • {(iterateFrobeniusEquiv R p n).symm y}
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : LieRing L<VAR>inst✝¹³ : LieAlgebra R L<VAR>inst✝¹² : LieRing L'<VAR>inst✝¹¹ : LieAlgebra R L'<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : LieRingModule L M'<VAR>inst✝³ : LieModule R L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N N₂ : LieSubmodule R L M<VAR>N' : LieSubmodule R L M'<VAR>M'' : Type u_1<VAR>inst✝² : AddCommGroup M''<VAR>inst✝¹ : Module R M''<VAR>inst✝ : LieRingModule L M''<VAR>g : M' →ₗ⁅R,L⁆ M''<GOAL>↑(map (g.comp f) N) = ↑(map g (map f N))
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : Subsingleton M<VAR>hI : I.IsPrime<VAR>x : M<VAR>hx : I = (Submodule.span R {x}).annihilator<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : Subsingleton M<VAR>hI : I.IsPrime<VAR>x : M<VAR>hx : I = (Submodule.span R {x}).annihilator<GOAL>I = ⊤
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r s : R<VAR>x y : M<GOAL>-r • -x = r • x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<GOAL>P.toPoly.natDegree = 0
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>(if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) } then if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l } else let_fun this := ⋯; { data := l ++ c :: m ++ r }.findAux p { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) else { byteIdx := utf8Len l }) = { byteIdx := utf8Len l + utf8Len (match !p c with | true => c :: List.takeWhile (fun x => !p x) m | false => []) }
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>(if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l } else let_fun this := ⋯; { data := l ++ c :: m ++ r }.findAux p { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })) = { byteIdx := utf8Len l + utf8Len (match !p c with | true => c :: List.takeWhile (fun x => !p x) m | false => []) }
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>h1 : { data := l ++ (c :: m ++ r) }.get { byteIdx := utf8Len l } = (c :: m ++ r).headD default<GOAL>(if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l } else let_fun this := ⋯; { data := l ++ c :: m ++ r }.findAux p { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })) = { byteIdx := utf8Len l + utf8Len (match !p c with | true => c :: List.takeWhile (fun x => !p x) m | false => []) }
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>h1 : { data := l ++ (c :: m ++ r) }.get { byteIdx := utf8Len l } = (c :: m ++ r).headD default<VAR>h2 : { data := l ++ c :: (m ++ r) }.next { byteIdx := utf8Len l } = { byteIdx := utf8Len l + c.utf8Size }<GOAL>(if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l } else let_fun this := ⋯; { data := l ++ c :: m ++ r }.findAux p { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })) = { byteIdx := utf8Len l + utf8Len (match !p c with | true => c :: List.takeWhile (fun x => !p x) m | false => []) }
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>h1 : { data := l ++ c :: (m ++ r) }.get { byteIdx := utf8Len l } = c<VAR>h2 : { data := l ++ c :: (m ++ r) }.next { byteIdx := utf8Len l } = { byteIdx := utf8Len l + c.utf8Size }<GOAL>(if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l } else let_fun this := ⋯; { data := l ++ c :: m ++ r }.findAux p { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })) = { byteIdx := utf8Len l + utf8Len (match !p c with | true => c :: List.takeWhile (fun x => !p x) m | false => []) }
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>h1 : { data := l ++ c :: (m ++ r) }.get { byteIdx := utf8Len l } = c<VAR>h2 : { data := l ++ c :: (m ++ r) }.next { byteIdx := utf8Len l } = { byteIdx := utf8Len l + c.utf8Size }<GOAL>(if p c = true then { byteIdx := utf8Len l } else { data := l ++ c :: (m ++ r) }.findAux p { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } { byteIdx := utf8Len l + c.utf8Size }) = { byteIdx := utf8Len l + utf8Len (match !p c with | true => c :: List.takeWhile (fun x => !p x) m | false => []) }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : DenselyOrdered (α ⊕ β)<VAR>a b : α<VAR>h : a < b<GOAL>∃ a_1, a < a_1 ∧ a_1 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : DenselyOrdered (α ⊕ β)<VAR>a b : α<VAR>h : a < b<VAR>c : α<VAR>ha : inl a < inl c<VAR>hb : inl c < inl b<GOAL>∃ a_1, a < a_1 ∧ a_1 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : DenselyOrdered (α ⊕ β)<VAR>a b : α<VAR>h : a < b<VAR>c : β<VAR>ha : inl a < inr c<VAR>hb : inr c < inl b<GOAL>∃ a_1, a < a_1 ∧ a_1 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : DenselyOrdered (α ⊕ β)<VAR>a b : β<VAR>h : a < b<GOAL>∃ a_1, a < a_1 ∧ a_1 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : DenselyOrdered (α ⊕ β)<VAR>a b : β<VAR>h : a < b<VAR>c : α<VAR>ha : inr a < inl c<VAR>hb : inl c < inr b<GOAL>∃ a_1, a < a_1 ∧ a_1 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>x✝ : DenselyOrdered (α ⊕ β)<VAR>a b : β<VAR>h : a < b<VAR>c : β<VAR>ha : inr a < inr c<VAR>hb : inr c < inr b<GOAL>∃ a_1, a < a_1 ∧ a_1 < b
<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 : R[X]<VAR>r : R<VAR>inst✝ : NoZeroDivisors R<VAR>a : R[X]<GOAL>p.scaleRoots r ∣ (p * a).scaleRoots r
<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 : R[X]<VAR>r : R<VAR>inst✝ : NoZeroDivisors R<VAR>a : R[X]<GOAL>p.scaleRoots r ∣ p.scaleRoots r * a.scaleRoots r
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : IsScalarTower F K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>h : Splits (RingHom.id K) f<GOAL>⊤ = ⊥
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : IsScalarTower F K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>h : Splits (RingHom.id K) f<GOAL>↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset ⊆ ↑⊥
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : IsScalarTower F K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>h : Splits (RingHom.id K) f<VAR>y : L<VAR>hy : y ∈ ↑(Multiset.map (⇑(algebraMap K L)) f.roots).toFinset<GOAL>y ∈ ↑⊥
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : IsScalarTower F K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>h : Splits (RingHom.id K) f<VAR>y : L<VAR>hy : ∃ a ∈ f.roots.toFinset, (algebraMap K L) a = y<GOAL>y ∈ ↑⊥
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : IsScalarTower F K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>h : Splits (RingHom.id K) f<VAR>y : L<VAR>x : K<VAR>hxy : (algebraMap K L) x = y<GOAL>(algebraMap K L) x ∈ ↑⊥
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : IsScalarTower F K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>h : ⊤ = ⊥<GOAL>Splits ((RingEquiv.ofBijective (algebraMap K L) ⋯).trans (RingEquiv.ofBijective (algebraMap K L) ⋯).symm).toRingHom f
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : IsScalarTower F K L<VAR>f : K[X]<VAR>inst✝ : IsSplittingField K L f<VAR>h : ⊤ = ⊥<GOAL>Splits ((RingEquiv.ofBijective (algebraMap K L) ⋯).symm.toRingHom.comp (RingEquiv.ofBijective (algebraMap K L) ⋯).toRingHom) f
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : Submartingale f 𝒢 μ<VAR>hτ : IsStoppingTime 𝒢 τ<GOAL>Submartingale (stoppedProcess f τ) 𝒢 μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : Submartingale f 𝒢 μ<VAR>hτ : IsStoppingTime 𝒢 τ<GOAL>∀ (τ_1 π : Ω → ℕ), IsStoppingTime 𝒢 τ_1 → IsStoppingTime 𝒢 π → τ_1 ≤ π → (∃ N, ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : Submartingale f 𝒢 μ<VAR>hτ : IsStoppingTime 𝒢 τ<GOAL>Adapted 𝒢 (stoppedProcess f τ)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : Submartingale f 𝒢 μ<VAR>hτ : IsStoppingTime 𝒢 τ<GOAL>∀ (i : ℕ), Integrable (stoppedProcess f τ i) μ
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>s : Set L<VAR>m : L<VAR>hm : m ∈ s<GOAL>m ∈ ↑(lieSpan R L s)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>s : Set L<VAR>m : L<VAR>hm : m ∈ s<GOAL>∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
<VAR>f : ℝ → ℝ<VAR>hf : Monotone f<GOAL>∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
<VAR>d₁ d₂ : Nat<VAR>n₁ n₂ : Int<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>inst✝ : Countable ι<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>i : ι<GOAL>aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>h : ∀ (x : K), 0 ≤ a * x * x + b * x + c<GOAL>b * b - 4 * a * c ≤ 0
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>h : ∀ (x : K), 0 ≤ a * x * x + b * x + c<VAR>ha : a < 0<GOAL>b * b - 4 * a * c ≤ 0
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>b c : K<VAR>h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c<GOAL>b * b - 4 * 0 * c ≤ 0
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>h : ∀ (x : K), 0 ≤ a * x * x + b * x + c<VAR>ha : 0 < a<GOAL>b * b - 4 * a * c ≤ 0
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>i : ι<VAR>paths : (i : ι) → Homotopic.Quotient (as i) (bs i)<GOAL>proj i (pi paths) = paths i
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>i : ι<VAR>a✝ : (i : ι) → Path (as i) (bs i)<GOAL>proj i (pi fun i => ⟦a✝ i⟧) = (fun i => ⟦a✝ i⟧) i
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>i : ι<VAR>a✝ : (i : ι) → Path (as i) (bs i)<GOAL>⟦(Path.pi a✝).map ⋯⟧ = (fun i => ⟦a✝ i⟧) i
<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>c c₁ c₂ p₁ p₂ : P<GOAL>perpBisector p₁ p₂ ≠ ⊥
<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>c c₁ c₂ p₁ p₂ : P<GOAL>(↑(perpBisector p₁ p₂)).Nonempty
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>f.val.base (genericPoint ↑↑X.toPresheafedSpace) = genericPoint ↑↑Y.toPresheafedSpace
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>IsGenericPoint (f.val.base (genericPoint ↑↑X.toPresheafedSpace)) ⊤
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>⊤ = closure (⇑f.val.base '' ⊤)
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>closure (⇑f.val.base '' ⊤) = ⊤
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>Set.univ ≤ closure (⇑f.val.base '' Set.univ)
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>⇑f.val.base '' Set.univ = Set.univ ∩ Set.range ⇑f.val.base
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>IsPreirreducible Set.univ
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>inst✝ : IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>(Set.univ ∩ Set.range ⇑f.val.base).Nonempty
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : CommRing R₁<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹¹ : CommSemiring R₂<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁸ : CommRing R₃<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂✝ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq n<VAR>B₂ : BilinForm R₂ (n → R₂)<GOAL>((BilinForm.toMatrixAux fun j => (LinearMap.stdBasis R₂ (fun x => R₂) j) 1) B₂).toBilin'Aux = B₂