ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>hab : a ≤ b<GOAL>IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioo a b) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<GOAL>{x | l.formPerm x ≠ x} ≤ ↑l.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<GOAL>↑(l.toFinset ⊔ l.tail.toFinset) ≤ ↑l.toFinset
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<GOAL>(hasseDeriv 0) f = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : iUnion U = univ<GOAL>Bijective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>U : ι → Set β<VAR>hU : iUnion U = univ<GOAL>((∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ ∀ (i : ι), Surjective ((U i).restrictPreimage f)) ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), x i + ε < y i<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), x i + ε < y i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : dist x z < ε<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), x i + ε < y i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), x i + ε < y i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz : ∀ (i : ι), z i < y i<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), x i + ε < y i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz✝ : ∀ (i : ι), z i < y i<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hyz : ∀ (i : ι), z i + δ < y i<GOAL>y ∈ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), x i + ε < y i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz✝ : ∀ (i : ι), z i < y i<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hyz : ∀ (i : ι), z i + δ < y i<GOAL>ball y δ ⊆ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), x i + ε < y i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz✝ : ∀ (i : ι), z i < y i<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hyz : ∀ (i : ι), z i + δ < y i<VAR>w : ι → ℝ<VAR>hw : w ∈ ball y δ<VAR>i : ι<GOAL>z i ≤ w i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>hs : IsUpperSet s<VAR>hx : x ∈ closure s<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hxy : ∀ (i : ι), x i + ε < y i<VAR>z : ι → ℝ<VAR>hz : z ∈ s<VAR>hxz : ∀ (b : ι), dist (x b) (z b) < ε<VAR>hyz✝ : ∀ (i : ι), z i < y i<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>hyz : ∀ (i : ι), z i + δ < y i<VAR>w : ι → ℝ<VAR>i : ι<VAR>hw : w ∈ univ.pi fun b => Ioo (y b - δ) (y b + δ)<GOAL>z i ≤ w i
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J × K ⥤ C<VAR>inst✝³ : HasLimitsOfShape J C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : Small.{v, u₁} J<VAR>inst✝ : Small.{v, u₂} K<VAR>F : J × K ⥤ Type v<VAR>j : J<VAR>k : K<VAR>f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k<GOAL>limit.π (curry.obj F ⋙ colim) j (limit.lift (curry.obj F ⋙ colim) { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim), π := { app := fun j => colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) { pt := colimit ((curry.obj F).obj j), ι := { app := fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k, naturality := ⋯ } }, naturality := ⋯ } } (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) = colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J × K ⥤ C<VAR>inst✝³ : HasLimitsOfShape J C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : Small.{v, u₁} J<VAR>inst✝ : Small.{v, u₂} K<VAR>F : J × K ⥤ Type v<VAR>j : J<VAR>k : K<VAR>f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k<GOAL>{ pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim), π := { app := fun j => colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) { pt := colimit ((curry.obj F).obj j), ι := { app := fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k, naturality := ⋯ } }, naturality := ⋯ } }.π.app j (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f) = colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J × K ⥤ C<VAR>inst✝³ : HasLimitsOfShape J C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : Small.{v, u₁} J<VAR>inst✝ : Small.{v, u₂} K<VAR>F : J × K ⥤ Type v<VAR>j : J<VAR>k : K<VAR>f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k<GOAL>colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) { pt := colimit ((curry.obj F).obj j), ι := { app := fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k, naturality := ⋯ } } (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f) = colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
<VAR>J : Type u₁<VAR>K : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J × K ⥤ C<VAR>inst✝³ : HasLimitsOfShape J C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : Small.{v, u₁} J<VAR>inst✝ : Small.{v, u₂} K<VAR>F : J × K ⥤ Type v<VAR>j : J<VAR>k : K<VAR>f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k<GOAL>{ pt := colimit ((curry.obj F).obj j), ι := { app := fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k, naturality := ⋯ } }.ι.app k f = colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : InfSet α<VAR>inst✝ : InfSet β<VAR>f : ι → α × β<GOAL>(iInf f).swap = ⨅ i, (f i).swap
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : β<VAR>p : Fin n → β<GOAL>insertNth 0 x p = cons x p
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharZero R<VAR>u : Rˣ<GOAL>u ≠ -u
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s✝ : Set F<VAR>L : Filter F<VAR>frechet : F →L[𝕜] 𝕜<VAR>s : Set F<GOAL>HasFDerivWithinAt f frechet s x ↔ HasGradientWithinAt f ((toDual 𝕜 F).symm frechet) s x
<VAR>x : ℝ<GOAL>Tendsto (fun y => Icc x y) (𝓝[>] x) ((vitaliFamily volume 1).filterAt x)
<VAR>x : ℝ<GOAL>∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ∈ (vitaliFamily volume 1).setsAt x
<VAR>x : ℝ<GOAL>∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.185407, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain K F m<VAR>β : Cochain K G n<VAR>h : n + 1 = m<VAR>p₁ p₂ : ℤ<VAR>h₁₂ : p₁ + n = p₂<GOAL>(liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (snd φ).v p₂ p₂ ⋯ = β.v p₁ p₂ h₁₂
<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>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>this : Invertible 1<GOAL>(fromBlocks 1 B C D).det = (D - C * B).det
<VAR>α : Type u<VAR>inst✝ : EMetricSpace α<VAR>s : Set α<GOAL>Continuous fun p => infEdist p.1 ↑p.2
<VAR>α : Type u<VAR>inst✝ : EMetricSpace α<VAR>s : Set α<GOAL>∀ (x y : α × Closeds α), infEdist x.1 ↑x.2 ≤ infEdist y.1 ↑y.2 + 2 * edist x y
<VAR>α : Type u<VAR>inst✝ : EMetricSpace α<VAR>s✝ : Set α<VAR>x : α<VAR>s : Closeds α<VAR>y : α<VAR>t : Closeds α<GOAL>infEdist (x, s).1 ↑(x, s).2 ≤ infEdist (y, t).1 ↑(y, t).2 + 2 * edist (x, s) (y, t)
<VAR>z : ℤ<VAR>h : 0 ≤ z<GOAL>normalize z = z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>f : E ≃ₗᵢ[ℝ] ℂ<VAR>hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : E<GOAL>(o.areaForm x) y = ((starRingEnd ℂ) (f x) * f y).im
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>f : E ≃ₗᵢ[ℝ] ℂ<VAR>hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x y : E<GOAL>(o.areaForm x) y = (o.areaForm (f.symm (f x))) (f.symm (f y))
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>arccos (⟪x, r • y⟫_ℝ / (‖x‖ * ‖r • y‖)) = arccos (⟪x, y⟫_ℝ / (‖x‖ * ‖y‖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf : _root_.Continuous f<GOAL>Continuous' f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf : _root_.Continuous f<VAR>h : Monotone f<GOAL>Continuous' f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf : _root_.Continuous f<VAR>h : Monotone f<VAR>c : Chain (Scott α)<VAR>z : Scott β<GOAL>{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf✝ : _root_.Continuous f<VAR>h : Monotone f<VAR>c : Chain (Scott α)<VAR>z : Scott β<VAR>hf : Monotone fun x => x ∈ f ⁻¹' notBelow z<VAR>hf' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf }<GOAL>{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf✝ : _root_.Continuous f<VAR>h : Monotone f<VAR>c : Chain (Scott α)<VAR>z : Scott β<VAR>hf : Monotone fun x => x ∈ f ⁻¹' notBelow z<VAR>hf' : { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf } (ωSup c) = ωSup (c.map { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf })<GOAL>{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf✝ : _root_.Continuous f<VAR>h : Monotone f<VAR>c : Chain (Scott α)<VAR>z : Scott β<VAR>hf : Monotone fun x => x ∈ f ⁻¹' notBelow z<VAR>hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })<GOAL>{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf✝ : _root_.Continuous f<VAR>h : Monotone f<VAR>c : Chain (Scott α)<VAR>z : Scott β<VAR>hf : Monotone fun x => x ∈ f ⁻¹' notBelow z<VAR>hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })<GOAL>¬{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ¬ωSup (c.map { toFun := f, monotone' := h }) ≤ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : OmegaCompletePartialOrder α<VAR>inst✝ : OmegaCompletePartialOrder β<VAR>f : Scott α → Scott β<VAR>hf✝ : _root_.Continuous f<VAR>h : Monotone f<VAR>c : Chain (Scott α)<VAR>z : Scott β<VAR>hf : Monotone fun x => x ∈ f ⁻¹' notBelow z<VAR>hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })<GOAL>(∃ a, (∃ y, ¬f (c y) ≤ z ↔ a) ∧ a) ↔ ∃ x, ¬f (c x) ≤ z
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>T : Subalgebra R B<VAR>hS : S.FG<VAR>hT : T.FG<GOAL>(S.prod T).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>T : Subalgebra R B<VAR>hS : S.FG<VAR>hT : T.FG<VAR>s : Set A<VAR>hs : s.Finite ∧ Algebra.adjoin R s = S<GOAL>(S.prod T).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>T : Subalgebra R B<VAR>hS : S.FG<VAR>hT : T.FG<VAR>s : Set A<VAR>hs : s.Finite ∧ Algebra.adjoin R s = S<VAR>t : Set B<VAR>ht : t.Finite ∧ Algebra.adjoin R t = T<GOAL>(S.prod T).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>T : Subalgebra R B<VAR>hS : S.FG<VAR>hT : T.FG<VAR>s : Set A<VAR>hs : s.Finite ∧ Algebra.adjoin R s = S<VAR>t : Set B<VAR>ht : t.Finite ∧ Algebra.adjoin R t = T<GOAL>((Algebra.adjoin R s).prod (Algebra.adjoin R t)).FG
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>(eval P) W.polynomialX = W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>(eval P) (C W.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W.a₂) * X 0 * X 2 + C W.a₄ * X 2 ^ 2)) = W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<VAR>f' : L<VAR>hfα : f' ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f' ≠ 0<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<VAR>f' : L<VAR>hfα : f' ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f' ≠ 0<VAR>hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<VAR>f' : L<VAR>hfα : f' ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f' ≠ 0<VAR>hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H := ⟨⁅e, f'⁆, ⋯⟩<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<VAR>f' : L<VAR>hfα : f' ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f' ≠ 0<VAR>hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H := ⟨⁅e, f'⁆, ⋯⟩<VAR>hh : α h ≠ 0<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<VAR>f' : L<VAR>hfα : f' ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f' ≠ 0<VAR>hef : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H := ⟨⁅e, f'⁆, ⋯⟩<VAR>hh : α h ≠ 0<VAR>f : L := (2 * (α h)⁻¹) • f'<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<VAR>f' : L<VAR>hfα : f' ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f' ≠ 0<VAR>hef✝ : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H := ⟨⁅e, f'⁆, ⋯⟩<VAR>hh : α h ≠ 0<VAR>f : L := (2 * (α h)⁻¹) • f'<VAR>hef : ⁅⁅e, f⁆, e⁆ = 2 • e<GOAL>∃ h e f, IsSl2Triple h e f ∧ e ∈ rootSpace H ⇑α ∧ f ∈ rootSpace H (-⇑α)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<VAR>f' : L<VAR>hfα : f' ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f' ≠ 0<VAR>hef✝ : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H := ⟨⁅e, f'⁆, ⋯⟩<VAR>hh : α h ≠ 0<VAR>f : L := (2 * (α h)⁻¹) • f'<VAR>hef : ⁅⁅e, f⁆, e⁆ = 2 • e<VAR>contra : ⁅e, f⁆ = 0<GOAL>False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>e : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>he₀ : e ≠ 0<VAR>f' : L<VAR>hfα : f' ∈ rootSpace H (-⇑α)<VAR>hf : ((killingForm K L) e) f' ≠ 0<VAR>hef✝ : ⁅e, f'⁆ = ((killingForm K L) e) f' • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))<VAR>h : ↥H := ⟨⁅e, f'⁆, ⋯⟩<VAR>hh : α h ≠ 0<VAR>f : L := (2 * (α h)⁻¹) • f'<VAR>hef : ⁅⁅e, f⁆, e⁆ = 2 • e<GOAL>⁅⁅e, f⁆, f⁆ = -(2 • f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity f<GOAL>ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<VAR>hs : s ⟂ₘ ν<VAR>hadd : μ = s + ν.withDensity (AEMeasurable.mk f hf)<GOAL>ν.withDensity (AEMeasurable.mk f hf) = ν.withDensity (μ.rnDeriv ν)
<VAR>F : Type u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ≥0<VAR>x : α<GOAL>f x ≤ nndist f 0
<VAR>F : Type u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ≥0<VAR>x : α<VAR>key : nndist (f x) (0 x) ≤ nndist f 0<GOAL>f x ≤ nndist f 0
<VAR>F : Type u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵇ ℝ≥0<VAR>x : α<VAR>key : nndist (f x) 0 ≤ nndist f 0<GOAL>f x ≤ nndist f 0