ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>f : p.obj a ⟶ p.obj b<VAR>φ : a ⟶ b<VAR>inst✝ : p.IsHomLift f φ<GOAL>f = p.map φ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>f : R[X]<VAR>inst✝² : Algebra R S<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>inst✝ : Algebra R T<VAR>hx' : (aeval x) f = 0<VAR>h : IsAdjoinRoot S f<GOAL>(liftHom x hx' h) h.root = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n<GOAL>Differentiable 𝕜 fun z => ∑' (n : α), g n z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n<VAR>hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y<GOAL>Differentiable 𝕜 fun z => ∑' (n : α), g n z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n<VAR>hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y<GOAL>∀ (n : α) (x : 𝕜), ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<GOAL>map (⇑h) (cocompact X) = cocompact Y
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp a (p + b) = toIocDiv hp a b + 1
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>F : C ⥤ Type v₁<VAR>hF : F.Corepresentable<VAR>X : C<VAR>f : F.coreprX ⟶ X<GOAL>(F.coreprW.app X).hom f = F.map f F.coreprx
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s✝ t : Set α<VAR>s : Finset α<GOAL>p.toOuterMeasure ↑s = ∑ x ∈ s, p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s✝ t : Set α<VAR>s : Finset α<GOAL>∀ b ∉ s, (↑s).indicator (⇑p) b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s✝ t : Set α<VAR>s : Finset α<GOAL>∑ b ∈ s, (↑s).indicator (⇑p) b = ∑ x ∈ s, p x
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝¹ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>inst✝ : DecidableEq I<GOAL>Pairwise (IsCoprime on fun i => s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝¹ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>inst✝ : DecidableEq I<VAR>hp : Pairwise (IsCoprime on fun i => s ↑i)<VAR>i : I<VAR>hi : i ∈ t<VAR>j : I<VAR>hj : j ∈ t \ {i}<GOAL>IsCoprime (s i) (s j)
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝¹ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>inst✝ : DecidableEq I<VAR>hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)<GOAL>Pairwise (IsCoprime on fun i => s ↑i)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<GOAL>volume (Ici a) = ⊤
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<GOAL>volume (Ioi a) = ⊤
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>inst✝ : DecidableEq I<GOAL>Pairwise (IsRelPrime on fun i => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>inst✝ : DecidableEq I<VAR>hp : Pairwise (IsRelPrime on fun i => s ↑i)<VAR>i : I<VAR>hi : i ∈ t<VAR>j : I<VAR>hj : j ∈ t \ {i}<GOAL>IsRelPrime (s i) (s j)
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>inst✝ : DecidableEq I<VAR>hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)<GOAL>Pairwise (IsRelPrime on fun i => s ↑i)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hg : MeromorphicAt g x<GOAL>MeromorphicAt (f - g) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hg : MeromorphicAt g x<GOAL>f - g = f + -g
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>x : 𝕜<VAR>hf : MeromorphicAt f x<VAR>hg : MeromorphicAt g x<VAR>z : 𝕜<GOAL>(f - g) z = (f + -g) z
<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>h : P.toPoly = Q.toPoly<GOAL>P.d = Q.d
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>HasFDerivAt (fun u => exp 𝕂 (u • x)) ((ContinuousLinearMap.smulRight 1 x).smulRight (exp 𝕂 (t • x))) t
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>(ContinuousLinearMap.smulRight 1 x).smulRight (exp 𝕂 (t • x)) = exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x
<VAR>𝕂 : Type u_1<VAR>𝕊 : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁹ : NontriviallyNormedField 𝕂<VAR>inst✝⁸ : CharZero 𝕂<VAR>inst✝⁷ : NormedCommRing 𝕊<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedSpace 𝕂 𝕊<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : Algebra 𝕊 𝔸<VAR>inst✝² : ContinuousSMul 𝕊 𝔸<VAR>inst✝¹ : IsScalarTower 𝕂 𝕊 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>x : 𝔸<VAR>t : 𝕊<VAR>htx : t • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>t' : 𝕊<GOAL>Commute (t' • x) (exp 𝕂 (t • x))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : MulOneClass M<VAR>l : List M<VAR>a : M<GOAL>(1 :: l).prod = l.prod
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : NontriviallyNormedField α<VAR>inst✝ : NormedAlgebra ℝ α<VAR>A : Matrix m n α<GOAL>‖A‖₊ = ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : NontriviallyNormedField α<VAR>inst✝ : NormedAlgebra ℝ α<VAR>A : Matrix m n α<VAR>N : ℝ≥0<VAR>hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊<GOAL>‖A‖₊ ≤ N
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : NontriviallyNormedField α<VAR>inst✝ : NormedAlgebra ℝ α<VAR>A : Matrix m n α<VAR>N : ℝ≥0<VAR>hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊<GOAL>(Finset.univ.sup fun i => ∑ j : n, ‖A i j‖₊) ≤ N
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : NontriviallyNormedField α<VAR>inst✝ : NormedAlgebra ℝ α<VAR>A : Matrix m n α<VAR>N : ℝ≥0<VAR>hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊<VAR>i : m<VAR>x✝ : i ∈ Finset.univ<GOAL>∑ j : n, ‖A i j‖₊ ≤ N
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : NontriviallyNormedField α<VAR>inst✝ : NormedAlgebra ℝ α<VAR>A : Matrix m n α<VAR>N : ℝ≥0<VAR>hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊<VAR>i : m<VAR>x✝ : i ∈ Finset.univ<VAR>h✝ : IsEmpty n<GOAL>∑ j : n, ‖A i j‖₊ ≤ N
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : NontriviallyNormedField α<VAR>inst✝ : NormedAlgebra ℝ α<VAR>A : Matrix m n α<VAR>N : ℝ≥0<VAR>hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊<VAR>i : m<VAR>x✝ : i ∈ Finset.univ<VAR>h✝ : Nonempty n<GOAL>∑ j : n, ‖A i j‖₊ ≤ N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>inst✝ : Std.Associative ga<VAR>h : Semiconj₂ f ga gb<VAR>h_surj : Surjective f<VAR>x₁ x₂ x₃ : α<GOAL>gb (gb (f x₁) (f x₂)) (f x₃) = gb (f x₁) (gb (f x₂) (f x₃))
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid 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>f : M →ₗ[R] M₂<VAR>g : M₃ →ₗ[R] M₄<VAR>x : M₃ × M₄<GOAL>x.2 = g x.1 ↔ -g x.1 + x.2 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Mul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<GOAL>a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Mul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<GOAL>a₂ < a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ < a₁ * b₁
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ' n).leadingCoeff = ↑(if Even n then n / 2 else n)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>z \ (x \ y ⊔ y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)
<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>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>f : M →ₗ⁅R,L⁆ M'<GOAL>map f N ≤ f.range
<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>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>f : M →ₗ⁅R,L⁆ M'<GOAL>map f N ≤ map f ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>x✝ : Fin n.succ<GOAL>x✝ ∈ ↑(Ioi 0) ↔ x✝ ∈ ↑(map (succEmb n) univ)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a : α<VAR>h : 0 < a<VAR>b c d : α<GOAL>(fun x => x + b) '' ((fun x => a * x) '' Icc c d) = Icc (a * c + b) (a * d + b)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>W.slope x₁ x₂ y₁ y₂ = -evalEval x₁ y₁ W.polynomialX / evalEval x₁ y₁ W.polynomialY
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>(3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / evalEval x₁ y₁ W.polynomialY
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>y₁ - W.negY x₁ y₁ = evalEval x₁ y₁ W.polynomialY
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) = 2 * y₁ + W.a₁ * x₁ + W.a₃
<VAR>p : Char → Bool<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝<GOAL>(x✝.takeWhile p).toString.data = List.takeWhile p x✝.toString.data
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>hf : Injective f<VAR>s t : Set α<VAR>h : f '' s = f '' t<GOAL>s = t
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>l.rotate n = [x] ↔ l = [x]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>h : Disjoint a b<GOAL>(a ⊔ b) \ b = a
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>m_empty : m ∅ = 0<VAR>m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t<VAR>m_subadd : ∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)<GOAL>(boundedBy m) s = m s
<VAR>R : Type u_1<VAR>inst✝ : NonAssocRing R<GOAL>ringChar R = 0 ↔ CharZero R
<VAR>u v : ℤˣ<GOAL>u ≠ v ↔ u = -v
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B✝ : Set (Set α)<VAR>s : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>B : Set (Set α)<VAR>hB : IsTopologicalBasis B<VAR>f : α → β<GOAL>IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B✝ : Set (Set α)<VAR>s : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>B : Set (Set α)<VAR>hB : IsTopologicalBasis B<VAR>f : α → β<VAR>hf : ∀ s ∈ B, IsOpen (f '' s)<VAR>o : Set α<VAR>ho : IsOpen o<GOAL>IsOpen (f '' o)
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B✝ : Set (Set α)<VAR>s : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>B : Set (Set α)<VAR>hB : IsTopologicalBasis B<VAR>f : α → β<VAR>hf : ∀ s ∈ B, IsOpen (f '' s)<VAR>o : Set α<VAR>ho : IsOpen o<GOAL>IsOpen (⋃ i, f '' ↑i)
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : Measure Ω<VAR>μ : autoParam (Measure E) _auto✝<VAR>hX : HasPDF X ℙ μ<VAR>s : Set E<VAR>hs : MeasurableSet s<GOAL>(map X ℙ) s = ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : PseudoEMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>h✝ : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤<GOAL>⋯.choose ≠ 0
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>α : Type v<VAR>C : G.Coloring α<VAR>c : V<GOAL>IsAntichain G.Adj {x | (Setoid.ker ⇑C).Rel x c}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<GOAL>p.toOuterMeasure.caratheodory = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<VAR>x : MeasurableSpace α<VAR>hx : x ∈ Set.range fun i => (p i • dirac i).caratheodory<GOAL>⊤ ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s t : Set α<VAR>x : MeasurableSpace α<VAR>hx : x ∈ Set.range fun i => (p i • dirac i).caratheodory<VAR>y : α<VAR>hy : (fun i => (p i • dirac i).caratheodory) y = x<GOAL>⊤ ≤ x
<VAR>x y : ℝ<VAR>f : CauSeq ℚ abs<GOAL>0 < mk f ↔ f.Pos
<VAR>x y : ℝ<VAR>f : CauSeq ℚ abs<GOAL>0 < f ↔ f.Pos
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>(p * p.mirror).coeff (p.natDegree + p.natTrailingDegree) = p.sum fun n x => x ^ 2
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>∑ k ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ, p.coeff (k, p.natDegree + p.natTrailingDegree - k).1 * p.mirror.coeff (k, p.natDegree + p.natTrailingDegree - k).2 = p.sum fun n x => x ^ 2
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ<GOAL>p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 * p.mirror.coeff (n, p.natDegree + p.natTrailingDegree - n).2 = p.coeff n ^ 2
<VAR>α✝ : Type u_1<VAR>l₁ l₂ : List α✝<VAR>x✝ : l₁ <:+ l₂<VAR>t : List α✝<VAR>h : t ++ l₁ = l₂<GOAL>t ++ l₁ ++ [] = l₂
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>a - a = 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x y : CoeSort.coe A<VAR>g : G<GOAL>(fun m g => (A.ρ g) m - m) (x + y) g = ((fun m g => (A.ρ g) m - m) x + (fun m g => (A.ρ g) m - m) y) g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x y : CoeSort.coe A<VAR>g : G<GOAL>(A.ρ g) x - x + ((A.ρ g) y - y) = ((fun g => (A.ρ g) x - x) + fun g => (A.ρ g) y - y) g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>r : k<VAR>x : CoeSort.coe A<VAR>g : G<GOAL>(A.ρ g) (r • x) - r • x = r • ((A.ρ g) x - x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>μ : M → N → N<VAR>r : N → N → Prop<VAR>mu : N → N → N<VAR>inst✝ : IsSymmOp N N mu<GOAL>Contravariant N N (flip mu) r ↔ Contravariant N N mu r
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝²¹ : Category.{u_4, u_1} C<VAR>inst✝²⁰ : Category.{u_5, u_2} D<VAR>inst✝¹⁹ : Category.{?u.362828, u_3} E<VAR>inst✝¹⁸ : HasShift C ℤ<VAR>inst✝¹⁷ : HasShift D ℤ<VAR>inst✝¹⁶ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹⁵ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝¹⁴ : G.CommShift ℤ<VAR>inst✝¹³ : HasZeroObject C<VAR>inst✝¹² : HasZeroObject D<VAR>inst✝¹¹ : HasZeroObject E<VAR>inst✝¹⁰ : Preadditive C<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : Preadditive E<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : ∀ (n : ℤ), (shiftFunctor E n).Additive<VAR>inst✝⁴ : Pretriangulated C<VAR>inst✝³ : Pretriangulated D<VAR>inst✝² : Pretriangulated E<VAR>inst✝¹ : F.IsTriangulated<VAR>inst✝ : F.mapArrow.EssSurj<VAR>T : Triangle D<VAR>hT : T ∈ distinguishedTriangles<GOAL>∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝²¹ : Category.{u_4, u_1} C<VAR>inst✝²⁰ : Category.{u_5, u_2} D<VAR>inst✝¹⁹ : Category.{?u.362828, u_3} E<VAR>inst✝¹⁸ : HasShift C ℤ<VAR>inst✝¹⁷ : HasShift D ℤ<VAR>inst✝¹⁶ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹⁵ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝¹⁴ : G.CommShift ℤ<VAR>inst✝¹³ : HasZeroObject C<VAR>inst✝¹² : HasZeroObject D<VAR>inst✝¹¹ : HasZeroObject E<VAR>inst✝¹⁰ : Preadditive C<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : Preadditive E<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : ∀ (n : ℤ), (shiftFunctor E n).Additive<VAR>inst✝⁴ : Pretriangulated C<VAR>inst✝³ : Pretriangulated D<VAR>inst✝² : Pretriangulated E<VAR>inst✝¹ : F.IsTriangulated<VAR>inst✝ : F.mapArrow.EssSurj<VAR>T : Triangle D<VAR>hT : T ∈ distinguishedTriangles<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>e₁ : F.obj X ≅ T.obj₁<VAR>e₂ : F.obj Y ≅ T.obj₂<VAR>w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁<GOAL>∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝²¹ : Category.{u_4, u_1} C<VAR>inst✝²⁰ : Category.{u_5, u_2} D<VAR>inst✝¹⁹ : Category.{?u.362828, u_3} E<VAR>inst✝¹⁸ : HasShift C ℤ<VAR>inst✝¹⁷ : HasShift D ℤ<VAR>inst✝¹⁶ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹⁵ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝¹⁴ : G.CommShift ℤ<VAR>inst✝¹³ : HasZeroObject C<VAR>inst✝¹² : HasZeroObject D<VAR>inst✝¹¹ : HasZeroObject E<VAR>inst✝¹⁰ : Preadditive C<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : Preadditive E<VAR>inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : ∀ (n : ℤ), (shiftFunctor E n).Additive<VAR>inst✝⁴ : Pretriangulated C<VAR>inst✝³ : Pretriangulated D<VAR>inst✝² : Pretriangulated E<VAR>inst✝¹ : F.IsTriangulated<VAR>inst✝ : F.mapArrow.EssSurj<VAR>T : Triangle D<VAR>hT : T ∈ distinguishedTriangles<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>e₁ : F.obj X ≅ T.obj₁<VAR>e₂ : F.obj Y ≅ T.obj₂<VAR>w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁<VAR>W : C<VAR>g : Y ⟶ W<VAR>h : W ⟶ (shiftFunctor C 1).obj X<VAR>H : Triangle.mk f g h ∈ distinguishedTriangles<GOAL>∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : r ↪r s<VAR>g : t ↪r u<GOAL>∀ {a b : α ⊕ γ}, Sum.Lex s u ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Sum.map ⇑f ⇑g, inj' := ⋯ } b) ↔ Sum.Lex r t a b
<VAR>x✝ y x : ℝ<VAR>hx : cos x ≠ 0<GOAL>tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2
<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 : M'<GOAL>m ∈ map f ⊥ ↔ m ∈ ⊥
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y : C<VAR>f g h k : X ⟶ Y<VAR>diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)<VAR>hd₁ : biprod.inl ≫ diag = biprod.lift f h<VAR>hd₂ : biprod.inr ≫ diag = biprod.lift g k<VAR>h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag<VAR>h₂ : diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)<GOAL>leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)