ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>↑(↑(-θ).expMapCircle * (o.kahler x) y).arg = ↑((o.kahler x) y).arg - θ
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>-θ + ↑((o.kahler x) y).arg = ↑((o.kahler x) y).arg - θ
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>↑(-θ).expMapCircle ≠ 0
<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 Q : Fin 3 → F<VAR>n d : F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hd : d ≠ 0<GOAL>W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (n / (P z * Q z * d)) = (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 - Q x * P z ^ 2 * d ^ 2) / (P z * Q z * d) ^ 2
<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 Q : Fin 3 → F<VAR>n d : F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hd : d ≠ 0<GOAL>(((n ^ 2 * (P z * Q z * d) + W.toAffine.a₁ * n * (P z * Q z * d) ^ 2 - (P z * Q z * d) ^ 2 * (P z * Q z * d) * W.toAffine.a₂) * P z ^ 2 - (P z * Q z * d) ^ 2 * (P z * Q z * d) * P x) * Q z ^ 2 - (P z * Q z * d) ^ 2 * (P z * Q z * d) * P z ^ 2 * Q x) * (P z * Q z * d) ^ 2 = (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 - Q x * P z ^ 2 * d ^ 2) * ((P z * Q z * d) ^ 2 * (P z * Q z * d) * P z ^ 2 * Q z ^ 2)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>inst✝ : LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<VAR>x✝ : ℕ<GOAL>x✝ ∈ Nat.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉₊
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : β → α<VAR>x : Filter β<VAR>a : α<GOAL>Tendsto f x (𝓝 a) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>a : α<GOAL>ContinuousWithinAt f {a} a
<VAR>M : Type u<VAR>inst✝² : Monoid M<VAR>α : Type v<VAR>inst✝¹ : MulAction M α<VAR>β : Type u_1<VAR>inst✝ : MulAction M β<VAR>y : α × β<VAR>g : M<GOAL>((fun m => m • y) g).2 ∈ orbit M y.2
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<VAR>s : Set Ω<VAR>_s_mble : MeasurableSet s<GOAL>↑μ.normalize s = (μ.mass⁻¹ • ↑μ) s
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<VAR>s : Set Ω<VAR>_s_mble : MeasurableSet s<GOAL>↑μ.mass⁻¹ * ↑μ s = (μ.mass⁻¹ • ↑μ) s
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : Preadditive C<VAR>inst✝² : HasKernels C<VAR>X Y : C<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>f : X ⟶ Y<VAR>I : IsIso f<VAR>h : f = 0<GOAL>False
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : Preadditive C<VAR>inst✝² : HasKernels C<VAR>X Y : C<VAR>inst✝¹ : Simple X<VAR>inst✝ : Simple Y<VAR>f : X ⟶ Y<VAR>I : IsIso f<VAR>h : f = 0<GOAL>𝟙 X = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : CommRing A<VAR>inst✝ : CommRing B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>a : A<VAR>hp0 : ¬p = 0<GOAL>rootMultiplicity a p = rootMultiplicity (f a) (map f p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : CommRing A<VAR>inst✝ : CommRing B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>a : A<VAR>hp0 : ¬p = 0<GOAL>rootMultiplicity (f a) (map f p) ≤ rootMultiplicity a p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : CommRing A<VAR>inst✝ : CommRing B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>a : A<VAR>hp0 : ¬p = 0<GOAL>(X - C (f a)) ^ rootMultiplicity (f a) (map f p) ∣ map f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a b : α<GOAL>⇑e '' Ioo a b = Ioo (e a) (e b)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<GOAL>(coeff R n) (X ^ n) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : Countable G<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>hμ : μ ≠ 0<VAR>h : IsFundamentalDomain G s μ<GOAL>μ s ≠ 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : Countable G<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>hμ : μ ≠ 0<VAR>h : IsFundamentalDomain G s μ<VAR>hc : 0 < μ univ<GOAL>μ s ≠ 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : Countable G<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>hμ : μ ≠ 0<VAR>h : IsFundamentalDomain G s μ<VAR>hc : μ s = 0<GOAL>μ univ ≤ 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : Countable G<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>hμ : μ ≠ 0<VAR>h : IsFundamentalDomain G s μ<VAR>hc : μ s = 0<GOAL>μ (⋃ g, g • s) ≤ 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : Countable G<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>hμ : μ ≠ 0<VAR>h : IsFundamentalDomain G s μ<VAR>hc : μ s = 0<GOAL>∑' (i : G), μ (i • s) ≤ 0
<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>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.dblX P = (P x ^ 2) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : CompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : CompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Mf : Monotone f<VAR>fbot : f ⊥ = ⊥<GOAL>f (sSup s) = sSup (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : CompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : CompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Mf : Monotone f<VAR>fbot : f ⊥ = ⊥<VAR>h : s = ∅<GOAL>f (sSup s) = sSup (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁶ : CompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : CompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : Nonempty γ<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Mf : Monotone f<VAR>fbot : f ⊥ = ⊥<VAR>h : s.Nonempty<GOAL>f (sSup s) = sSup (f '' s)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>g : G<VAR>x : Quotient G α<GOAL>Set.MapsTo (fun x => g • x) x.orbit x.orbit
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>g : G<VAR>x : Quotient G α<GOAL>Set.MapsTo (fun x => g • x) (MulAction.orbit G (Quotient.out' x)) (MulAction.orbit G (Quotient.out' x))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>a✝ : Nontrivial A<GOAL>pb.minpolyGen = minpoly A pb.gen
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>a✝ : Nontrivial A<VAR>q : A[X]<VAR>hq : q.degree < pb.minpolyGen.degree<VAR>hn0 : ¬q = 0<VAR>h0 : (aeval pb.gen) q = 0<GOAL>False
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v r : ι → F<VAR>i : ι<VAR>x : F<VAR>hx : ∀ i ∈ s, x ≠ v i<GOAL>eval x ((interpolate s v) r) = eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v r : ι → F<VAR>i : ι<VAR>x : F<VAR>hx : ∀ i ∈ s, x ≠ v i<GOAL>∑ x_1 ∈ s, r x_1 * eval x (Lagrange.basis s v x_1) = ∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v r : ι → F<VAR>i✝ : ι<VAR>x : F<VAR>hx : ∀ i ∈ s, x ≠ v i<VAR>i : ι<VAR>hi : i ∈ s<GOAL>r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
<VAR>a : UnitAddCircle<VAR>r : ℝ<GOAL>(fun x => (ofReal' ∘ oddKernel a) x - 0) =O[atTop] fun x => x ^ r
<VAR>a : UnitAddCircle<VAR>r v : ℝ<VAR>hv : 0 < v<VAR>hv' : oddKernel a =O[atTop] fun x => rexp (-v * x)<GOAL>(fun x => (ofReal' ∘ oddKernel a) x - 0) =O[atTop] fun x => x ^ r
<VAR>a : UnitAddCircle<VAR>r v : ℝ<VAR>hv : 0 < v<VAR>hv' : (fun x => ‖oddKernel a x‖) =O[atTop] fun x => rexp (-v * x)<GOAL>(fun x => ‖(ofReal' ∘ oddKernel a) x - 0‖) =O[atTop] fun x => x ^ r
<VAR>a : UnitAddCircle<VAR>r v : ℝ<VAR>hv : 0 < v<VAR>hv' : (fun x => ‖oddKernel a x‖) =O[atTop] fun x => rexp (-v * x)<GOAL>(fun x => ‖oddKernel a x‖) =O[atTop] fun x => x ^ r
<VAR>a : UnitAddCircle<VAR>r : ℝ<GOAL>(fun x => (ofReal' ∘ sinKernel a) x - 0) =O[atTop] fun x => x ^ r
<VAR>a : UnitAddCircle<VAR>r v : ℝ<VAR>hv : 0 < v<VAR>hv' : sinKernel a =O[atTop] fun x => rexp (-v * x)<GOAL>(fun x => (ofReal' ∘ sinKernel a) x - 0) =O[atTop] fun x => x ^ r
<VAR>a : UnitAddCircle<VAR>r v : ℝ<VAR>hv : 0 < v<VAR>hv' : (fun x => ‖sinKernel a x‖) =O[atTop] fun x => rexp (-v * x)<GOAL>(fun x => ‖(ofReal' ∘ sinKernel a) x - 0‖) =O[atTop] fun x => x ^ r
<VAR>a : UnitAddCircle<VAR>r v : ℝ<VAR>hv : 0 < v<VAR>hv' : (fun x => ‖sinKernel a x‖) =O[atTop] fun x => rexp (-v * x)<GOAL>(fun x => ‖sinKernel a x‖) =O[atTop] fun x => x ^ r
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>(ofReal' ∘ oddKernel a) (1 / x) = (1 * ↑(x ^ (3 / 2))) • (ofReal' ∘ sinKernel a) x
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s✝ : Set α<VAR>inst✝ : IsFiniteMeasure ν<VAR>h₁ : ν ≤ μ<VAR>s : Set α<VAR>h_s_meas : MeasurableSet s<GOAL>(μ - ν + ν) s = μ s
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module A M₁<VAR>inst✝⁵ : SMulCommClass R A M₁<VAR>inst✝⁴ : SMulCommClass A R M₁<VAR>inst✝³ : IsScalarTower R A M₁<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Invertible 2<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm A M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>polarBilin (Q₁.tmul Q₂) = ⅟2 • (polarBilin Q₁).tmul (polarBilin Q₂)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : Module R M₁<VAR>inst✝⁶ : Module A M₁<VAR>inst✝⁵ : SMulCommClass R A M₁<VAR>inst✝⁴ : SMulCommClass A R M₁<VAR>inst✝³ : IsScalarTower R A M₁<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Invertible 2<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm A M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>2 • (associated Q₁).tmul (associated Q₂) = ⅟2 • 2 • 2 • (BilinMap.tensorDistrib R A) ((associatedHom A) Q₁ ⊗ₜ[R] (associatedHom R) Q₂)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : DecidableEq A<VAR>inst✝ : One B<VAR>a : A<VAR>b : B<VAR>h : b ≠ 1<VAR>x : A<VAR>hx : x = a<GOAL>x ∈ mulSupport (mulSingle a b)
<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>X Y : Submodule R M<VAR>x✝ : X ⋖ X ⊔ Y<GOAL>(↥(X, X ⊔ Y).2 ⧸ Submodule.comap (X, X ⊔ Y).2.subtype (X, X ⊔ Y).1) ≃ₗ[R] ↥(X ⊓ Y, Y).2 ⧸ Submodule.comap (X ⊓ Y, Y).2.subtype (X ⊓ Y, Y).1
<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>X Y : Submodule R M<VAR>x✝ : X ⋖ X ⊔ Y<GOAL>(↥(X, Y ⊔ X).2 ⧸ Submodule.comap (X, Y ⊔ X).2.subtype (X, Y ⊔ X).1) ≃ₗ[R] ↥(Y ⊓ X, Y).2 ⧸ Submodule.comap (Y ⊓ X, Y).2.subtype (Y ⊓ X, Y).1
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ (a : α), Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a)) → v.limRatio ρ a = AEMeasurable.mk (v.limRatio ρ) ⋯ a → Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatioMeas hρ a))
<VAR>C : Type u<VAR>motive : {X Y : F C} → (X ⟶ Y) → Prop<VAR>X Y : F C<VAR>t : X ⟶ Y<VAR>id : ∀ (X : F C), motive (𝟙 X)<VAR>α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom<VAR>α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv<VAR>l_hom : ∀ (X : F C), motive (λ_ X).hom<VAR>l_inv : ∀ (X : F C), motive (λ_ X).inv<VAR>ρ_hom : ∀ (X : F C), motive (ρ_ X).hom<VAR>ρ_inv : ∀ (X : F C), motive (ρ_ X).inv<VAR>comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)<VAR>whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)<VAR>whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)<GOAL>motive t
<VAR>C : Type u<VAR>motive : {X Y : F C} → (X ⟶ Y) → Prop<VAR>X Y : F C<VAR>t : X ⟶ Y<VAR>id : ∀ (X : F C), motive (𝟙 X)<VAR>α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom<VAR>α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv<VAR>l_hom : ∀ (X : F C), motive (λ_ X).hom<VAR>l_inv : ∀ (X : F C), motive (λ_ X).inv<VAR>ρ_hom : ∀ (X : F C), motive (ρ_ X).hom<VAR>ρ_inv : ∀ (X : F C), motive (ρ_ X).inv<VAR>comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)<VAR>whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)<VAR>whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)<GOAL>∀ (a : X ⟶ᵐ Y), motive ⟦a⟧
<VAR>C : Type u<VAR>motive : {X Y : F C} → (X ⟶ Y) → Prop<VAR>X Y : F C<VAR>t : X ⟶ Y<VAR>id : ∀ (X : F C), motive (𝟙 X)<VAR>α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom<VAR>α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv<VAR>l_hom : ∀ (X : F C), motive (λ_ X).hom<VAR>l_inv : ∀ (X : F C), motive (λ_ X).inv<VAR>ρ_hom : ∀ (X : F C), motive (ρ_ X).hom<VAR>ρ_inv : ∀ (X : F C), motive (ρ_ X).inv<VAR>comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)<VAR>whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)<VAR>whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)<VAR>f : X ⟶ᵐ Y<GOAL>motive ⟦f⟧
<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>a a' : α<VAR>b : M<VAR>f : α → β<VAR>hf : Injective f<VAR>x z : α<VAR>y : M<GOAL>(single (f x) y) (f z) = (single x y) z
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>J : Type u_1<VAR>obj : J → Scheme<VAR>map : (i : J) → obj i ⟶ X<VAR>e₁ : J ≃ 𝒰.J<VAR>e₂✝ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)<VAR>e₂ : ∀ (i : J), map i = (e₂✝ i).hom ≫ 𝒰.map (e₁ i)<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ Set.range ⇑(map ((fun x => e₁.symm (𝒰.f x)) x)).val.base
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>J : Type u_1<VAR>obj : J → Scheme<VAR>map : (i : J) → obj i ⟶ X<VAR>e₁ : J ≃ 𝒰.J<VAR>e₂✝ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)<VAR>e₂ : ∀ (i : J), map i = (e₂✝ i).hom ≫ 𝒰.map (e₁ i)<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ Set.range ⇑(𝒰.map (𝒰.f x)).val.base
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>J : Type u_1<VAR>obj : J → Scheme<VAR>map : (i : J) → obj i ⟶ X<VAR>e₁ : J ≃ 𝒰.J<VAR>e₂✝ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)<VAR>e₂ : ∀ (i : J), map i = (e₂✝ i).hom ≫ 𝒰.map (e₁ i)<VAR>x : ↑↑X.toPresheafedSpace<GOAL>Function.Surjective ⇑(e₂✝ ((fun x => e₁.symm (𝒰.f x)) x)).hom.val.base
<VAR>R : Type u_1<VAR>inst✝¹ : MulZeroClass R<VAR>b : R<VAR>inst✝ : Nontrivial R<VAR>ra : IsRightRegular 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : MulZeroClass R<VAR>b : R<VAR>inst✝ : Nontrivial R<VAR>ra : IsRightRegular 0<VAR>x y : R<VAR>xy : x ≠ y<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : MulZeroClass R<VAR>b : R<VAR>inst✝ : Nontrivial R<VAR>ra : IsRightRegular 0<VAR>x y : R<VAR>xy : x ≠ y<GOAL>x * 0 = y * 0
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝ : DecidablePred p<VAR>i : Fin (n + 1)<VAR>hi : i ∈ Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i => some (i.castLT ⋯)<VAR>j : ℕ<VAR>hjn : j < n + 1<VAR>hj : ⟨j, hjn⟩ < i<VAR>hpj : p ⟨j, hjn⟩<GOAL>False
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝ : DecidablePred p<VAR>i : Fin (n + 1)<VAR>hi : i ∈ Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i => some (i.castLT ⋯)<VAR>j : ℕ<VAR>hjn : j < n + 1<VAR>hj : ⟨j, hjn⟩ < i<VAR>hpj : p ⟨j, hjn⟩<VAR>h : (find fun i => p (i.castLT ⋯)) = none<GOAL>False
<VAR>m n✝ n : ℕ<VAR>p : Fin (n + 1) → Prop<VAR>x✝ : DecidablePred p<VAR>i : Fin (n + 1)<VAR>hi : i ∈ Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i => some (i.castLT ⋯)<VAR>j : ℕ<VAR>hjn : j < n + 1<VAR>hj : ⟨j, hjn⟩ < i<VAR>hpj : p ⟨j, hjn⟩<VAR>k : Fin n<VAR>h : (find fun i => p (i.castLT ⋯)) = some k<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>a < b * (a / b) + b
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t => t ∈ s ∧ a ∈ t) id<VAR>t₁ : Set α<VAR>ht₁ : t₁ ∈ s<VAR>t₂ : Set α<VAR>ht₂ : t₂ ∈ s<VAR>x : α<VAR>hx : x ∈ t₁ ∩ t₂<GOAL>∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t => t ∈ s ∧ a ∈ t) id<VAR>x : α<GOAL>𝓝 x = 𝓝 x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>t : Set α<GOAL>μ t = ∑' (g : G), μ (g • t ∩ s)
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>n : ℤ<VAR>hn : 0 ≤ n<GOAL>‖↑n‖ = ↑n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<GOAL>a ∈ P.part a
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>y : 𝕜<GOAL>(fderiv 𝕜 f x) y = y • deriv f x
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>y : 𝕜<GOAL>(fderiv 𝕜 f x) y = (fderiv 𝕜 f x) (y • 1)
<VAR>m✝ n m : ℕ<GOAL>(m + 1) % 2 = 0 ↔ m % 2 = 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s : Multiset α<VAR>b : α<VAR>l : List α<GOAL>filter (fun x => x = b) ⟦l⟧ = replicate (count b ⟦l⟧) b
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s : Multiset α<VAR>b : α<VAR>l : List α<GOAL>↑(List.filter (fun b_1 => decide (b_1 = b)) l) = replicate (List.count b l) b
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : X → Prop<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝 (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝 x, p x