ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z = 0<VAR>hQz : Q z = 0<GOAL>P ≈ Q
<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>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z = 0<VAR>hQz : Q z = 0<VAR>hPx : IsUnit (P x)<GOAL>P ≈ Q
<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>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z = 0<VAR>hQz : Q z = 0<VAR>hPx : IsUnit (P x)<VAR>hPy : IsUnit (P y)<GOAL>P ≈ Q
<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>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z = 0<VAR>hQz : Q z = 0<VAR>hPx : IsUnit (P x)<VAR>hPy : IsUnit (P y)<VAR>hQx : IsUnit (Q x)<GOAL>P ≈ Q
<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>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z = 0<VAR>hQz : Q z = 0<VAR>hPx : IsUnit (P x)<VAR>hPy : IsUnit (P y)<VAR>hQx : IsUnit (Q x)<VAR>hQy : IsUnit (Q y)<GOAL>P ≈ Q
<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>hPz : P z = 0<VAR>hQz : Q z = 0<VAR>hPx : IsUnit (P x)<VAR>hPy : IsUnit (P y)<VAR>hQx : IsUnit (Q x)<VAR>hQy : IsUnit (Q y)<VAR>hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)<VAR>hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)<GOAL>P ≈ Q
<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>hPz : P z = 0<VAR>hQz : Q z = 0<VAR>hPx : IsUnit (P x)<VAR>hPy : IsUnit (P y)<VAR>hQx : IsUnit (Q x)<VAR>hQy : IsUnit (Q y)<VAR>hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)<VAR>hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)<GOAL>(fun m => m • Q) (hPy.unit / hPx.unit * (hQx.unit / hQy.unit)) = P
<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>hPz : P z = 0<VAR>hQz : Q z = 0<VAR>hPx : IsUnit (P x)<VAR>hPy : IsUnit (P y)<VAR>hQx : IsUnit (Q x)<VAR>hQy : IsUnit (Q y)<VAR>hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)<VAR>hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)<GOAL>![P y ^ 2 / P x ^ 2 * (Q x ^ 2 / Q y ^ 2) * Q x, P y ^ 3 / P x ^ 3 * (Q x ^ 3 / Q y ^ 3) * Q y, 0] = P
<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>hPz : P z = 0<VAR>hQz : Q z = 0<VAR>hPx : IsUnit (P x)<VAR>hPy : IsUnit (P y)<VAR>hQx : IsUnit (Q x)<VAR>hQy : IsUnit (Q y)<VAR>hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)<VAR>hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)<GOAL>![P y ^ 2 / P x ^ 2 * (Q x ^ 2 / Q y ^ 2) * Q x, P y ^ 3 / P x ^ 3 * (Q x ^ 3 / Q y ^ 3) * Q y, 0] = ![P x, P y, 0]
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>o.oangle x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>o.oangle x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>P : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔ (∀ᵐ (x : α) ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Ioc b a), P x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : HasContDiffBump E<VAR>inst✝ : MeasurableSpace E<VAR>c : E<VAR>f✝ : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>f : ContDiffBump 0<VAR>x : E<GOAL>f.normed μ (-x) = f.normed μ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>a b : α<VAR>H₁ : (Ioi a).Nonempty<VAR>H₂ : a ≤ b<GOAL>b ∈ closure (Ioi a)
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : IsEmpty V<GOAL>G.chromaticNumber = 0
<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G✝.Coloring α<VAR>G : SimpleGraph V<VAR>inst✝ : IsEmpty V<GOAL>G.Colorable 0
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>n : ℕ<VAR>IH : ∀ m < n, p.removeZero.rightInv i m = p.rightInv i m<GOAL>p.removeZero.rightInv i n = p.rightInv i n
<VAR>θ : ℂ<GOAL>sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑π
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x y : A<GOAL>(baseChange W B).toAffine.negY (f x) (f y) = f ((baseChange W A).toAffine.negY x y)
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x y : A<GOAL>(baseChange W B).toAffine.negY (f x) (f y) = (baseChange W B).toAffine.negY (f.toRingHom x) (f.toRingHom y)
<VAR>x z : EReal<VAR>h : x < z<GOAL>∃ y, x < ↑y ∧ ↑y < z
<VAR>x z : EReal<VAR>h : x < z<VAR>a : EReal<VAR>ha₁ : x < a<VAR>ha₂ : a < z<GOAL>∃ y, x < ↑y ∧ ↑y < z
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>x a : 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝¹ : NormedAddCommGroup 𝕜'<VAR>inst✝ : NormedSpace 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>hh : HasDerivAt h h' (x + a)<GOAL>HasDerivAt (fun x => h (x + a)) h' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₁ : f₁ =o[l] g₁<VAR>h₂ : f₂ =O[l] g₂<GOAL>(fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₂ : f₂ =O[l] g₂<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁<GOAL>∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₂ : f₂ =O[l] g₂<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁<VAR>c : ℝ<VAR>cpos : 0 < c<GOAL>IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → R<VAR>g₁ g₂ : α → 𝕜<VAR>h₂ : f₂ =O[l] g₂<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>c' : ℝ<VAR>c'pos : c' > 0<VAR>hc' : IsBigOWith c' l f₂ g₂<GOAL>IsBigOWith c l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l (𝓝 C)<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Tendsto f l atBot<VAR>hg : Tendsto g l (𝓝 C)<VAR>this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atTop<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>C : Set Code<VAR>H : ∀ (cf cg : Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)<GOAL>(ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype n<VAR>M : Matrix m n α<VAR>N N' : Matrix n o α<GOAL>M * (N - N') = M * N - M * N'
<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>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W.addX P Q = addU P Q ^ 2
<VAR>s : ℝ<GOAL>Tendsto (fun x => rexp x / x ^ s) atTop atTop
<VAR>s : ℝ<VAR>n : ℕ<VAR>hn : s < ↑n<GOAL>Tendsto (fun x => rexp x / x ^ s) atTop atTop
<VAR>s : ℝ<VAR>n : ℕ<VAR>hn : s < ↑n<GOAL>(fun x => rexp x / x ^ n) ≤ᶠ[atTop] fun x => rexp x / x ^ s
<VAR>s : ℝ<VAR>n : ℕ<VAR>hn : s < ↑n<VAR>x : ℝ<VAR>hx₀ : 0 < x<VAR>hx₁ : 1 ≤ x<GOAL>rexp x / x ^ n ≤ rexp x / x ^ s
<VAR>s : ℝ<VAR>n : ℕ<VAR>hn : s < ↑n<VAR>x : ℝ<VAR>hx₀ : 0 < x<VAR>hx₁ : 1 ≤ x<GOAL>x ^ s ≤ x ^ ↑n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝² : ι → Type u_4<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i j : ι<VAR>a : α i<VAR>β✝¹ : Type u_5<VAR>inst✝ : CompleteLattice β✝¹<VAR>β✝ : Type u_6<VAR>β : ι → Type u_7<GOAL>(insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>β✝² : ι → Type u_4<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i j : ι<VAR>a : α i<VAR>β✝¹ : Type u_5<VAR>inst✝ : CompleteLattice β✝¹<VAR>β✝ : Type u_6<VAR>β : ι → Type u_7<GOAL>α i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<GOAL>{s | IsPreconnected s} = range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪ (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<GOAL>range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪ (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}) ⊆ {s | IsPreconnected s}
<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>inst✝¹ : StrongRankCondition R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>h : 1 < Module.rank R M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>∃ y, LinearIndependent R ![x, y]
<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>inst✝¹ : StrongRankCondition R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>h : 1 < Module.rank R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>y : M<VAR>hy : LinearIndependent R (Fin.snoc ![x] y)<GOAL>∃ y, LinearIndependent R ![x, y]
<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>inst✝¹ : StrongRankCondition R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>h : 1 < Module.rank R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>y : M<VAR>hy : LinearIndependent R (Fin.snoc ![x] y)<VAR>this : Fin.snoc ![x] y = ![x, y]<GOAL>∃ y, LinearIndependent R ![x, y]
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>U : C<VAR>s : (forget A).obj (G.obj (op U))<VAR>V W : C<VAR>i : V ⟶ U<VAR>t : (forget A).obj (F.obj (op V))<VAR>ht : (f.app (op V)) t = (G.map i.op) s<VAR>j : W ⟶ V<GOAL>(f.app (op W)) ((F.map j.op) t) = (G.map (j ≫ i).op) s
<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>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<GOAL>IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
<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>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπS_pi : IsPiSystem πS<GOAL>IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
<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>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπS_pi : IsPiSystem πS<VAR>hπS_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πS<GOAL>IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
<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>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπS_pi : IsPiSystem πS<VAR>hπS_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πS<VAR>πTβ : Set (Set ((i : { x // x ∈ T }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i => f (↑i) a) ⁻¹' t = s}<GOAL>IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
<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>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπS_pi : IsPiSystem πS<VAR>hπS_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πS<VAR>πTβ : Set (Set ((i : { x // x ∈ T }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπT_pi : IsPiSystem πT<GOAL>IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
<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>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπS_pi : IsPiSystem πS<VAR>hπS_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πS<VAR>πTβ : Set (Set ((i : { x // x ∈ T }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπT_pi : IsPiSystem πT<VAR>hπT_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πT<GOAL>IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
<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>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>f✝ : Ω → β✝<VAR>g : Ω → β'<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>inst✝ : IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπS_pi : IsPiSystem πS<VAR>hπS_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πS<VAR>πTβ : Set (Set ((i : { x // x ∈ T }) → β ↑i)) := Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}<VAR>πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i => f (↑i) a) ⁻¹' t = s}<VAR>hπT_pi : IsPiSystem πT<VAR>hπT_gen : MeasurableSpace.comap (fun a i => f (↑i) a) pi = generateFrom πT<GOAL>IndepSets πS πT κ μ