ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>x : Ordinal.{u_1}<GOAL>x < b ^ succ (log b x)
<VAR>b : Ordinal.{u_1}<VAR>hb : 1 < b<GOAL>0 < b ^ succ (log b 0)
<VAR>b : Ordinal.{u_1}<VAR>hb : 1 < b<VAR>x : Ordinal.{u_1}<VAR>hx : x ≠ 0<GOAL>x < b ^ succ (log b x)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : k ≫ S.g = 0<VAR>inst✝ : S.HasLeftHomology<GOAL>S.f = 𝟙 S.X₁ ≫ S.f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝³ : SetLike S R<VAR>inst✝² : Monoid R<VAR>inst✝¹ : AddMonoid ι<VAR>A : ι → S<VAR>inst✝ : GradedMonoid A<VAR>ι' : Type u_4<VAR>l : List ι'<VAR>i : ι' → ι<VAR>r : ι' → R<VAR>h : ∀ j ∈ l, r j ∈ A (i j)<GOAL>(List.map r l).prod ∈ A (List.map i l).sum
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>S : Set α<GOAL>#↑S < (type r).cof → Bounded r S
<VAR>R✝ : Type u<VAR>S✝ : Type v<VAR>F : Type u_1<VAR>inst✝¹⁰ : Semiring R✝<VAR>inst✝⁹ : Semiring S✝<VAR>inst✝⁸ : FunLike F R✝ S✝<VAR>rc : RingHomClass F R✝ S✝<VAR>f : F<VAR>I✝ J : Ideal R✝<VAR>K L : Ideal S✝<VAR>G : Type u_2<VAR>inst✝⁷ : FunLike G S✝ R✝<VAR>rcg : RingHomClass G S✝ R✝<VAR>ι : Sort u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>M : Type u_6<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>I : Ideal R<VAR>N : Submodule S M<GOAL>Submodule.restrictScalars R (map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N
<VAR>R✝ : Type u<VAR>S✝ : Type v<VAR>F : Type u_1<VAR>inst✝¹⁰ : Semiring R✝<VAR>inst✝⁹ : Semiring S✝<VAR>inst✝⁸ : FunLike F R✝ S✝<VAR>rc : RingHomClass F R✝ S✝<VAR>f : F<VAR>I✝ J : Ideal R✝<VAR>K L : Ideal S✝<VAR>G : Type u_2<VAR>inst✝⁷ : FunLike G S✝ R✝<VAR>rcg : RingHomClass G S✝ R✝<VAR>ι : Sort u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>M : Type u_6<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>I : Ideal R<VAR>N : Submodule S M<GOAL>Submodule.restrictScalars R (⨆ b ∈ ↑I, (algebraMap R S) b • N) = ⨆ a ∈ ↑I, Submodule.restrictScalars R ((algebraMap R S) a • N)
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c✝ d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>c : 𝔸<VAR>hd : HasDerivWithinAt d d' s x<GOAL>HasDerivWithinAt (fun y => c * d y) (c * d') s x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c✝ d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>c : 𝔸<VAR>hd : HasDerivWithinAt d d' s x<GOAL>c * d' = 0 * d x + c * d'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<GOAL>(if h : (const abv 0).LimZero then 0 else (const abv 0).inv h) = const abv 0
<VAR>m n : ℕ<GOAL>m.gcd (n + m) = m.gcd (n + 1 * m)
<VAR>m n : Nat<VAR>h : m < n<GOAL>(range n).get? m = some m
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies<VAR>inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies<VAR>inst✝³ : F.Full<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.EffectivelyEnough<VAR>inst✝ : Precoherent D<VAR>X : C<VAR>S : Sieve X<GOAL>S ∈ (coherentTopology C).sieves X ↔ S ∈ (F.inducedTopology (coherentTopology D)).sieves X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies<VAR>inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies<VAR>inst✝³ : F.Full<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.EffectivelyEnough<VAR>inst✝ : Precoherent D<VAR>X : C<VAR>S : Sieve X<VAR>this : Precoherent C<GOAL>S ∈ (coherentTopology C).sieves X ↔ S ∈ (F.inducedTopology (coherentTopology D)).sieves X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies<VAR>inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies<VAR>inst✝³ : F.Full<VAR>inst✝² : F.Faithful<VAR>inst✝¹ : F.EffectivelyEnough<VAR>inst✝ : Precoherent D<VAR>X : C<VAR>S : Sieve X<VAR>this : Precoherent C<GOAL>S ∈ (coherentTopology C).sieves X ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ioo (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ioo b₁ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Ioo (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ioo b₁ b₂))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p✝ p : α → Bool<VAR>l l' : List α<VAR>h : l ⊆ l'<VAR>x : α<VAR>hx : x ∈ filter p l<GOAL>x ∈ filter p l'
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p✝ p : α → Bool<VAR>l l' : List α<VAR>h : l ⊆ l'<VAR>x : α<VAR>hx : x ∈ l ∧ p x = true<GOAL>x ∈ l' ∧ p x = true
<VAR>f g : CircleDeg1Lift<VAR>f₁ f₂ : CircleDeg1Liftˣ<VAR>h : τ ↑f₁ = τ ↑f₂<GOAL>∃ F, Semiconj ⇑F ⇑↑f₁ ⇑↑f₂
<VAR>α : Type u_1<VAR>f : α → α<VAR>m n : Nat<VAR>l : List α<VAR>h : m ≠ n<GOAL>(modifyNth f m l)[n]? = l[n]?
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x✝ : α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<GOAL>∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε✝ : ℝ<VAR>s t : Set α<VAR>x✝ : α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ε_lt : ENNReal.ofReal ε < infEdist x E<GOAL>∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s t : Set α<VAR>x✝ : α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ε_lt : ENNReal.ofReal ε < infEdist x E<VAR>δ : ℝ<VAR>hδ : δ < ε<GOAL>x ∉ cthickening δ E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s t : Set α<VAR>x✝ : α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>ε_lt : ENNReal.ofReal ε < infEdist x E<VAR>δ : ℝ<VAR>hδ : δ < ε<GOAL>ENNReal.ofReal δ < infEdist x E
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ snd X (Y ⊗ Z) ≫ fst Y Z = fst (X ⊗ Y) Z ≫ snd X Y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>Limits.BinaryFan.fst (product (product X Y).cone.pt Z).cone ≫ Limits.BinaryFan.snd (product X Y).cone = fst (X ⊗ Y) Z ≫ snd X Y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>I X : Set (ι × α)<GOAL>(∀ (i : ι), (M i).Basis (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I)) (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' X))) ↔ ∀ (i : ι), (M i).Basis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ ν : FiniteMeasure Ω<VAR>h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s<GOAL>↑μ = ↑ν
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>(pos p).succ'.pred'.toZNumNeg = ZNum.neg p
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>(pos p).toZNumNeg = ZNum.neg p
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>(ZNum.pos p).pred.succ = ZNum.pos p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>hC : IsExposed 𝕜 B C<VAR>hCA : C ⊆ A<GOAL>IsExposed 𝕜 (A ∩ B) C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>hC : IsExposed 𝕜 B C<VAR>hCA : C ⊆ A<GOAL>IsExposed 𝕜 (B ∩ A) C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝ : AddCommSemigroup α<VAR>h : Periodic f c<VAR>a x : α<GOAL>(fun x => f (x + a)) (x + c) = (fun x => f (x + a)) x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<GOAL>W'.Equation P ↔ P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>N : LieSubmodule R L M<GOAL>baseChange A ⊥ = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>N : LieSubmodule R L M<GOAL>{ toSubmodule := ⊥, lie_mem := ⋯ } = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h₁ : 0 < a<VAR>h₂ : a ≤ 1<GOAL>1 ≤ a⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : Nontrivial α<VAR>s : Set α<VAR>h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b<GOAL>Dense s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : Nontrivial α<VAR>s : Set α<VAR>h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b<VAR>U : Set α<VAR>U_open : IsOpen U<VAR>U_nonempty : U.Nonempty<GOAL>(U ∩ s).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : Nontrivial α<VAR>s : Set α<VAR>h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, a < c ∧ c < b<VAR>U : Set α<VAR>U_open : IsOpen U<VAR>U_nonempty : U.Nonempty<VAR>a b : α<VAR>hab : a < b<VAR>H : Ioo a b ⊆ U<GOAL>(U ∩ s).Nonempty
<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>Disjoint (frontier s) s ↔ IsOpen s
<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 - y) x = ↑(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 y x = ↑(π / 2)<GOAL>(-o).oangle x (x - y) = ↑(Real.arctan (‖y‖ / ‖x‖))
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ i j : ι<VAR>x : β i<VAR>h : i ≠ j<GOAL>erase j (single i x) = single i x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix m m R<VAR>C : Matrix n m R<VAR>D : Matrix n n R<GOAL>(fromBlocks A 0 C D).det = A.det * D.det
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤<VAR>hp1 : 1 ≤ p<GOAL>∫⁻ (a : α), (f + g) a ^ p ∂μ < ⊤
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤<VAR>hp1 : 1 ≤ p<VAR>hp0_lt : 0 < p<GOAL>∫⁻ (a : α), (f + g) a ^ p ∂μ < ⊤
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ⊤<VAR>hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ⊤<VAR>hp1 : 1 ≤ p<VAR>hp0_lt : 0 < p<VAR>hp0 : 0 ≤ p<GOAL>∫⁻ (a : α), (f + g) a ^ p ∂μ < ⊤
<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 p : MvPolynomial σ R<GOAL>p = 0 ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
<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 p : MvPolynomial σ R<GOAL>(∀ (m : σ →₀ ℕ), coeff m p = coeff m 0) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>W.ΨSq ↑n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddCommMonoidWithOne G<VAR>inst✝¹ : AddMonoid H<VAR>inst✝ : AddConstMapClass F G H 1 b<VAR>f : F<VAR>n : ℕ<VAR>x : G<GOAL>f (↑n + x) = f x + n • b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>p q : R[X]<GOAL>eval₂ (algebraMap R S) x (p * q) = eval₂ (algebraMap R S) x p * eval₂ (algebraMap R S) x q
<VAR>α : Type u_1<VAR>inst✝³ : MonoidWithZero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulMono α<VAR>a : α<VAR>H : 0 ≤ a<GOAL>0 ≤ a ^ 0
<VAR>α : Type u_1<VAR>inst✝³ : MonoidWithZero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulMono α<VAR>a : α<VAR>H : 0 ≤ a<GOAL>0 ≤ 1
<VAR>α : Type u_1<VAR>inst✝³ : MonoidWithZero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulMono α<VAR>a : α<VAR>H : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ (n + 1)
<VAR>α : Type u_1<VAR>inst✝³ : MonoidWithZero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulMono α<VAR>a : α<VAR>H : 0 ≤ a<VAR>n : ℕ<GOAL>0 ≤ a ^ n * a
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<GOAL>∫ (x : ℝ) in Iic b, deriv f x = f b
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<VAR>this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x<GOAL>∫ (x : ℝ) in Iic b, deriv f x = f b
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<VAR>this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x<GOAL>IntegrableOn (deriv f) (Iic b) volume
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<VAR>this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x<GOAL>Tendsto f atBot (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b✝ l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : f =ᶠ[cocompact ℝ] 0<VAR>b : ℝ<VAR>this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x<GOAL>Tendsto f atBot (𝓝 0)
<VAR>α : Type u_1<VAR>n : ZNum<GOAL>↑↑n = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioc a c ∪ Ioc b c = Ioc (min a b) c
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : Group G<VAR>inst✝² : AddGroup A<VAR>s : Set G<VAR>inst✝¹ : Monoid α<VAR>inst✝ : MulDistribMulAction α G<VAR>P H : Subgroup G<VAR>hP : P ≤ H<VAR>h : ↥H<GOAL>MulAut.conj h • P.subgroupOf H = (MulAut.conj ↑h • P).subgroupOf H
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : Group G<VAR>inst✝² : AddGroup A<VAR>s : Set G<VAR>inst✝¹ : Monoid α<VAR>inst✝ : MulDistribMulAction α G<VAR>P H : Subgroup G<VAR>hP : P ≤ H<VAR>h : ↥H<GOAL>MulAut.conj h • P.subgroupOf H ≤ (MulAut.conj ↑h • P).subgroupOf H
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : Group G<VAR>inst✝² : AddGroup A<VAR>s : Set G<VAR>inst✝¹ : Monoid α<VAR>inst✝ : MulDistribMulAction α G<VAR>P H : Subgroup G<VAR>hP : P ≤ H<VAR>h : ↥H<GOAL>(MulAut.conj ↑h • P).subgroupOf H ≤ MulAut.conj h • P.subgroupOf H
<VAR>num den : Int<GOAL>-num /. -den = num /. den
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<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>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s✝ : Set M<VAR>x : M<VAR>s : Set (M × M')<VAR>p : TangentBundle (I.prod I') (M × M')<VAR>hs : UniqueMDiffWithinAt (I.prod I') s p.proj<GOAL>{ proj := p.proj.1, snd := (mfderivWithin (I.prod I') I Prod.fst s p.proj) p.snd } = { proj := p.proj.1, snd := p.snd.1 }
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<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>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s✝ : Set M<VAR>x : M<VAR>s : Set (M × M')<VAR>p : TangentBundle (I.prod I') (M × M')<VAR>hs : UniqueMDiffWithinAt (I.prod I') s p.proj<GOAL>{ proj := p.proj.1, snd := (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj.1) (TangentSpace I' p.proj.2)) p.snd } = { proj := p.proj.1, snd := p.snd.1 }
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasExt C<VAR>X Y Z T : C<VAR>inst✝ : HasDerivedCategory C<VAR>f : X ⟶ Y<GOAL>(mk₀ f).hom = ShiftedHom.mk₀ ↑0 ⋯ ((DerivedCategory.singleFunctor C 0).map f)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁷ : NontriviallyNormedField 𝕂<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedRing 𝔹<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : NormedAlgebra 𝕂 𝔹<VAR>inst✝² : CompleteSpace 𝔸<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F 𝔸 𝔹<VAR>inst✝ : RingHomClass F 𝔸 𝔹<VAR>f : F<VAR>hf : Continuous ⇑f<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>f (exp 𝕂 x) = exp 𝕂 (f x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁷ : NontriviallyNormedField 𝕂<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedRing 𝔹<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : NormedAlgebra 𝕂 𝔹<VAR>inst✝² : CompleteSpace 𝔸<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F 𝔸 𝔹<VAR>inst✝ : RingHomClass F 𝔸 𝔹<VAR>f : F<VAR>hf : Continuous ⇑f<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>f ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x) = (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (f x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁷ : NontriviallyNormedField 𝕂<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedRing 𝔹<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : NormedAlgebra 𝕂 𝔹<VAR>inst✝² : CompleteSpace 𝔸<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F 𝔸 𝔹<VAR>inst✝ : RingHomClass F 𝔸 𝔹<VAR>f : F<VAR>hf : Continuous ⇑f<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>∑' (b : ℕ), (⇑f ∘ fun n => (↑n !)⁻¹ • x ^ n) b = (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (f x)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁷ : NontriviallyNormedField 𝕂<VAR>inst✝⁶ : NormedRing 𝔸<VAR>inst✝⁵ : NormedRing 𝔹<VAR>inst✝⁴ : NormedAlgebra 𝕂 𝔸<VAR>inst✝³ : NormedAlgebra 𝕂 𝔹<VAR>inst✝² : CompleteSpace 𝔸<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F 𝔸 𝔹<VAR>inst✝ : RingHomClass F 𝔸 𝔹<VAR>f : F<VAR>hf : Continuous ⇑f<VAR>x : 𝔸<VAR>hx : x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>∑' (b : ℕ), f ((↑b !)⁻¹ • x ^ b) = ∑' (n : ℕ), (↑n !)⁻¹ • f x ^ n