ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommSemiring R₁<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H✝ H : B.IsRefl<VAR>h : ker B = ⊥<VAR>x✝ : M₁<VAR>hx : B.flip x✝ = 0<GOAL>B x✝ = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommSemiring R₁<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H✝ H : B.IsRefl<VAR>h : ker B = ⊥<VAR>x✝¹ : M₁<VAR>hx : B.flip x✝¹ = 0<VAR>x✝ : M₁<GOAL>(B x✝¹) x✝ = 0 x✝
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_3<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : Away r S<GOAL>(IsLocalization.Away.auxHom S r).comp (IsLocalization.Away.auxInv S r) = RingHom.id S
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_3<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : Away r S<GOAL>((IsLocalization.Away.auxHom S r).comp (IsLocalization.Away.auxInv S r)).comp (algebraMap R S) = (RingHom.id S).comp (algebraMap R S)
<VAR>θ : Angle<GOAL>(-θ).sin = -θ.sin
<VAR>x✝ : ℝ<GOAL>(-↑x✝).sin = -(↑x✝).sin
<VAR>𝕂 : Type u_1<VAR>𝔸✝ : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝¹⁰ : RCLike 𝕂<VAR>inst✝⁹ : NormedRing 𝔸✝<VAR>inst✝⁸ : NormedAlgebra 𝕂 𝔸✝<VAR>inst✝⁷ : NormedRing 𝔹<VAR>inst✝⁶ : NormedAlgebra 𝕂 𝔹<VAR>inst✝⁵ : CompleteSpace 𝔸✝<VAR>ι : Type u_4<VAR>𝔸 : ι → Type u_5<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → NormedRing (𝔸 i)<VAR>inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)<VAR>inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)<VAR>x : (i : ι) → 𝔸 i<VAR>j : ι<VAR>xj : 𝔸 j<VAR>i : ι<GOAL>Function.update (exp 𝕂 x) j (exp 𝕂 xj) i = exp 𝕂 (Function.update x j xj) i
<VAR>𝕂 : Type u_1<VAR>𝔸✝ : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝¹⁰ : RCLike 𝕂<VAR>inst✝⁹ : NormedRing 𝔸✝<VAR>inst✝⁸ : NormedAlgebra 𝕂 𝔸✝<VAR>inst✝⁷ : NormedRing 𝔹<VAR>inst✝⁶ : NormedAlgebra 𝕂 𝔹<VAR>inst✝⁵ : CompleteSpace 𝔸✝<VAR>ι : Type u_4<VAR>𝔸 : ι → Type u_5<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → NormedRing (𝔸 i)<VAR>inst✝¹ : (i : ι) → NormedAlgebra 𝕂 (𝔸 i)<VAR>inst✝ : ∀ (i : ι), CompleteSpace (𝔸 i)<VAR>x : (i : ι) → 𝔸 i<VAR>j : ι<VAR>xj : 𝔸 j<VAR>i : ι<GOAL>Function.update (fun i => exp 𝕂 (x i)) j (exp 𝕂 xj) i = exp 𝕂 (Function.update x j xj i)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>s : Set (Sym2 V)<GOAL>Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁷ : Fintype l<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>inst✝ : Invertible D<GOAL>IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C)
<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>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>h : f =O[l] g<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f 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>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>h : f =O[l] g<VAR>c : ℝ<VAR>h₀ : c ≥ 0<VAR>hc : IsBigOWith c l f g<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖f 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>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>h : f =O[l] g<VAR>c : ℝ<VAR>h₀ : c ≥ 0<VAR>hc : IsBigOWith c l f g<VAR>x : α<VAR>hx : ‖f x‖ ≤ c * ‖g x‖<GOAL>(fun x x_1 => x ≤ x_1) ‖f x / g x‖ c
<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>α : Type u_17<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>h : f =O[l] g<VAR>c : ℝ<VAR>h₀ : c ≥ 0<VAR>hc : IsBigOWith c l f g<VAR>x : α<VAR>hx : ‖f x‖ ≤ c * ‖g x‖<GOAL>(fun x x_1 => x ≤ x_1) (‖f x‖ / ‖g x‖) c
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁ : b ≤ 1<GOAL>Antitone fun x => b ^ x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>b : ℝ<VAR>hb₀ : 0 < b<VAR>hb₁✝ : b ≤ 1<VAR>hb₁ : b < 1<GOAL>Antitone fun x => b ^ x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hb₀ : 0 < 1<VAR>hb₁ : 1 ≤ 1<GOAL>Antitone fun x => 1 ^ x
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r✝ : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>n : ℕ<VAR>x : Fin n → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>dimH (Metric.ball x r) = ↑n
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f : E → ℝ<GOAL>StrongConvexOn s m f ↔ ConvexOn ℝ s fun x => f x - m / 2 * ‖x‖ ^ 2
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝³ y✝ : E<VAR>f : E → ℝ<VAR>x✝² : Convex ℝ s<VAR>x : E<VAR>x✝¹ : x ∈ s<VAR>y : E<VAR>x✝ : y ∈ s<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (a • x + b • y) ≤ a • f x + b • f y - a * b * (fun r => m / 2 * r ^ 2) ‖x - y‖ ↔ (fun x => f x - m / 2 * ‖x‖ ^ 2) (a • x + b • y) ≤ a • (fun x => f x - m / 2 * ‖x‖ ^ 2) x + b • (fun x => f x - m / 2 * ‖x‖ ^ 2) y
<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<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : CommSemiring A<VAR>inst✝³ : CommSemiring B<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : Algebra S B<VAR>g : R →ₐ[S] A<VAR>y x✝ : σ → A<VAR>i✝ : σ<GOAL>(aevalTower (Algebra.ofId S A) x✝) (X i✝) = (aeval x✝) (X i✝)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f g : R⟦X⟧<GOAL>trunc n (↑(trunc n f) * ↑(trunc n g)) = trunc n (f * g)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ -y ≠ 0<GOAL>Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>u : M<GOAL>∑ i : ι, b.equivFun u i • b i = u
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹² : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : InnerProductSpace ℝ F'<VAR>inst✝³ : Fintype ι<VAR>V : Type u_8<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace 𝕜 V<VAR>inst✝ : FiniteDimensional 𝕜 V<VAR>S : Submodule 𝕜 V<VAR>L✝ L : ↥S →ₗᵢ[𝕜] V<VAR>s : ↥S<GOAL>L.extend ↑s = L s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹² : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : InnerProductSpace ℝ F'<VAR>inst✝³ : Fintype ι<VAR>V : Type u_8<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace 𝕜 V<VAR>inst✝ : FiniteDimensional 𝕜 V<VAR>S : Submodule 𝕜 V<VAR>L✝ L : ↥S →ₗᵢ[𝕜] V<VAR>s : ↥S<VAR>this : CompleteSpace ↥S<GOAL>L.extend ↑s = L s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹² : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : InnerProductSpace ℝ F'<VAR>inst✝³ : Fintype ι<VAR>V : Type u_8<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace 𝕜 V<VAR>inst✝ : FiniteDimensional 𝕜 V<VAR>S : Submodule 𝕜 V<VAR>L✝ L : ↥S →ₗᵢ[𝕜] V<VAR>s : ↥S<VAR>this : CompleteSpace ↥S<GOAL>(L.toLinearMap ∘ₗ ↑(orthogonalProjection S) + ((LinearMap.range L.toLinearMap)ᗮ.subtypeₗᵢ.comp ((stdOrthonormalBasis 𝕜 ↥Sᗮ).repr.trans ((stdOrthonormalBasis 𝕜 ↥(LinearMap.range L.toLinearMap)ᗮ).reindex (finCongr ⋯)).repr.symm).toLinearIsometry).toLinearMap ∘ₗ ↑(orthogonalProjection Sᗮ)) ↑s = L.toLinearMap s
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s<VAR>s : Set α<VAR>n : ℕ<VAR>a : α<GOAL>enumerate sel s (n + 1) = some a → a ∈ s
<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✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>x : E<VAR>U : Set E<GOAL>U ∈ 𝓝 x ↔ ∃ s, ∃ r > 0, (s.sup p).ball x r ⊆ U
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹² : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : GroupWithZero G<VAR>inst✝⁶ : SmoothInv₀ I G<VAR>inst✝⁵ : SmoothMul I G<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_7<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H' M<VAR>f g : M → G<VAR>s : Set M<VAR>a : M<VAR>n : ℕ∞<VAR>hf : ContMDiff I' I n f<VAR>hg : ContMDiff I' I n g<VAR>h₀ : ∀ (x : M), g x ≠ 0<GOAL>ContMDiff I' I n (f / g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>d : ℝ≥0∞<GOAL>s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
<VAR>m : ℕ∞<GOAL>0 = m ↔ m = 0
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y✝<VAR>inst✝ : TopologicalSpace Z<VAR>p✝ : X → Prop<VAR>Y : Type u_5<VAR>p : X → Prop<VAR>l : Filter Y<VAR>f : Y → Subtype p<VAR>a : X<VAR>ha : p a<GOAL>Tendsto f l (𝓝 ⟨a, ha⟩) ↔ Tendsto (fun x => ↑(f x)) l (𝓝 ↑⟨a, ha⟩)
<VAR>X : Type u<VAR>Y✝ : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y✝<VAR>inst✝ : TopologicalSpace Z<VAR>p✝ : X → Prop<VAR>Y : Type u_5<VAR>p : X → Prop<VAR>l : Filter Y<VAR>f : Y → Subtype p<VAR>a : X<VAR>ha : p a<GOAL>Tendsto (Subtype.val ∘ f) l (𝓝 a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝 ↑⟨a, ha⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>r' : β → β → Prop<VAR>t : Set α<VAR>a b : α<VAR>inst✝ : Preorder α<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) {a} ∧ IsGreatest {a} a
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>inst✝ : IsIso g<VAR>H : P (f ≫ g)<GOAL>P f
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>inst✝ : IsIso g<VAR>H : P (f ≫ g)<GOAL>f = (asIso g).symm.commRingCatIsoToRingEquiv.toRingHom.comp (f ≫ g)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>interior s = ∅ ↔ Dense sᶜ
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>hι : #ι < c.cof<GOAL>Cardinal.lift.{u, u} #ι < c.cof
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L M : Sublattice α<VAR>f : LatticeHom α β<VAR>s t : Set α<VAR>a : α<GOAL>↑L = univ ↔ L = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>hs : NullMeasurableSet s μ<VAR>c : ℝ≥0∞<GOAL>∫⁻ (a : α), s.indicator (fun x => c) a ∂μ = c * μ s
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<VAR>h : ∀ᵐ (x : Ω) ∂μ, ((condexpKernel μ m) x) t = 0 ∨ ((condexpKernel μ m) x) t = 1<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<VAR>h : ∀ᵐ (x : Ω) ∂μ, ((condexpKernel μ m) x) t = 0 ∨ ((condexpKernel μ m) x) t = 1<VAR>ht : MeasurableSet t<GOAL>∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<VAR>h : ∀ᵐ (x : Ω) ∂μ, ((condexpKernel μ m) x) t = 0 ∨ ((condexpKernel μ m) x) t = 1<VAR>ht : MeasurableSet t<VAR>ω : Ω<VAR>hω_eq : (((condexpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω<VAR>hω : ((condexpKernel μ m) ω) t = 0 ∨ ((condexpKernel μ m) ω) t = 1<GOAL>(μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm : m ≤ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iCondIndep m hm s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<VAR>h : ∀ᵐ (x : Ω) ∂μ, ((condexpKernel μ m) x) t = 0 ∨ ((condexpKernel μ m) x) t = 1<VAR>ht : MeasurableSet t<VAR>ω : Ω<VAR>hω_eq : (((condexpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω<VAR>hω : ((condexpKernel μ m) ω) t = 0 ∨ ((condexpKernel μ m) ω) t = 1<GOAL>(((condexpKernel μ m) ω) t = 0 ∨ ((condexpKernel μ m) ω) t = ⊤) ∨ ((condexpKernel μ m) ω) t = 1
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = k
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>(∃ u, u.card = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s).card = k
<VAR>a b : ℕ<VAR>r : ℤ<VAR>ha : a % 2 = 1<VAR>hb : b % 4 = 1<VAR>hr : jacobiSymNat b a = r<GOAL>jacobiSymNat a b = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>a ∈ ⋂ i, ↑(f i) ↔ ∀ (i : ι), a ∈ f i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : HomogeneousLocalization 𝒜 x<GOAL>(y1 - y2).val = y1.val - y2.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : HomogeneousLocalization 𝒜 x<GOAL>(y1 - y2).val = (y1 + -y2).val
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<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>k✝ : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<VAR>h : N₁.normalizer = N₁<VAR>k : ℕ<GOAL>ucs k ⊥ ≤ N₁