ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁷ : Monoid α<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : MulAction α β<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : SMulPosMono α β<VAR>inst✝ : SMulPosReflectLE α β<VAR>hb : 0 < b<GOAL>a • b ≤ b ↔ a • b ≤ 1 • b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : OrderedCommGroup α<VAR>inst✝ : OrderedCommGroup β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<GOAL>AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<GOAL>Tendsto (fun a => ‖a‖) (𝓝 1) (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>g : α → β<VAR>f : Filter α<GOAL>(pure g).seq f = map g f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>g : α → β<VAR>f : Filter α<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>g '' s ∈ (pure g).seq f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>g : α → β<VAR>f : Filter α<VAR>s : Set (α → β)<VAR>hs : s ∈ pure g<VAR>t : Set α<VAR>ht : t ∈ f<GOAL>s.seq t ∈ map g f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>x₀ : β<GOAL>EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>F : ι → β → α<VAR>x₀ : β<GOAL>(∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<VAR>h : x ≠ z<GOAL>min (firstDiff x y) (firstDiff y z) ≤ firstDiff x z
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<VAR>h : x ≠ z<VAR>H : firstDiff x z < min (firstDiff x y) (firstDiff y z)<GOAL>False
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<VAR>h : x ≠ z<VAR>H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z<GOAL>False
<VAR>E : ℕ → Type u_1<VAR>x y z : (n : ℕ) → E n<VAR>h : x ≠ z<VAR>H : firstDiff x z < firstDiff x y ∧ firstDiff x z < firstDiff y z<GOAL>x (firstDiff x z) = z (firstDiff x z)
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>hx' : x ≤ π / 2<GOAL>2 / π * x ≤ sin x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>hx' : x ≤ π / 2<GOAL>(π / 2)⁻¹ * x ≤ sin x
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>α : Type u_2<VAR>i : α → Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : (a : α) → Mul (i a)<GOAL>commProb ((a : α) → i a) = ∏ a : α, commProb (i a)
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>α : Type u_2<VAR>i : α → Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : (a : α) → Mul (i a)<GOAL>↑(Nat.card { p // ∀ (a : α), (p.1 * p.2) a = (p.2 * p.1) a }) / ↑(Nat.card ((a : α) → i a)) ^ 2 = ↑(Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })) / ↑(Nat.card ((a : α) → i a)) ^ 2
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>α : Type u_2<VAR>i : α → Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : (a : α) → Mul (i a)<GOAL>Nat.card { p // ∀ (a : α), (p.1 * p.2) a = (p.2 * p.1) a } = Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝³ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : DecidableEq M<VAR>x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)<GOAL>(coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun x x_1 => ↑x_1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p₁ p₂ p₃ : P<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p₁ p₂ p₃ : P<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hv : vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}<GOAL>Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(a ∈ s.sup fun b => {f b}) ↔ a ∈ image f s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(∃ v ∈ s, a ∈ {f v}) ↔ ∃ a_1 ∈ s, f a_1 = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∉ s<VAR>r : β → β → Prop<VAR>f : α → β<GOAL>_root_.Pairwise (r on fun a_1 => f ↑a_1) ↔ _root_.Pairwise (r on fun a => f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∉ s<VAR>r : β → β → Prop<VAR>f : α → β<GOAL>(↑s).Pairwise (r on f) → ((∀ b ∈ s, a ≠ b → (r on f) a b ∧ (r on f) b a) ↔ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a))
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>inst✝³ : Preorder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : IsLower α<VAR>s : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<GOAL>Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Ici a)
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>inst✝² : Preorder α<VAR>s : Set α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : β → α<VAR>inst✝ : IsLower α<GOAL>Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Ici a)
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<GOAL>IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>ι : Sort u_3<VAR>t : ι → TopologicalSpace X<VAR>h : ∀ (i : ι), SequentialSpace X<VAR>this : TopologicalSpace X := ⨆ i, t i<GOAL>SequentialSpace X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>ι : Sort u_3<VAR>t : ι → TopologicalSpace X<VAR>h : ∀ (i : ι), SequentialSpace X<VAR>this : TopologicalSpace X := ⨆ i, t i<VAR>s : Set X<VAR>hs : IsSeqClosed s<VAR>i : ι<GOAL>IsClosed s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>ι : Sort u_3<VAR>t : ι → TopologicalSpace X<VAR>h : ∀ (i : ι), SequentialSpace X<VAR>this✝ : TopologicalSpace X := ⨆ i, t i<VAR>s : Set X<VAR>hs : IsSeqClosed s<VAR>i : ι<VAR>this : TopologicalSpace X := t i<GOAL>IsClosed s
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q b a : ℝ≥0<VAR>ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤<VAR>hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0<VAR>h'a : ¬a = 0<VAR>h'b : ¬b = 0<GOAL>(↑a * ↑b)⁻¹ = (↑a)⁻¹ * (↑b)⁻¹
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q b a : ℝ≥0<VAR>ha : ↑a ≠ 0 ∨ ↑b ≠ ⊤<VAR>hb : ↑a ≠ ⊤ ∨ ↑b ≠ 0<VAR>h'a : ¬a = 0<VAR>h'b : ¬b = 0<GOAL>a * b ≠ 0
<VAR>G : Type u<VAR>H : Type v<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>f : H →ₙ* G<VAR>hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d<VAR>inst✝ : UniqueProds G<VAR>A B : Finset H<VAR>A0 : A.Nonempty<VAR>B0 : B.Nonempty<GOAL>∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<VAR>h : a - ↑⌊a⌋ = b - ↑⌊b⌋<GOAL>a - b = ↑(⌊a⌋ - ⌊b⌋)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ a b : α<VAR>z : ℤ<VAR>hz : a - b = ↑z<GOAL>fract a = fract b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ a b : α<VAR>z : ℤ<VAR>hz : a - b = ↑z<GOAL>a - fract b = ↑(z + ⌊b⌋)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ a b : α<VAR>z : ℤ<VAR>hz : a - b = ↑z<GOAL>b + ↑z - fract b = ↑z + ↑⌊b⌋
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>j j' : J<VAR>x : F.obj j<VAR>x' : F.obj j'<VAR>w : colimit.ι F j x = colimit.ι F j' x'<GOAL>EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', x'⟩
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : HasColimit F<VAR>j j' : J<VAR>x : F.obj j<VAR>x' : F.obj j'<VAR>w : colimit.ι F j x = colimit.ι F j' x'<GOAL>Quot.mk (Quot.Rel F) ⟨j, x⟩ = Quot.mk (Quot.Rel F) ⟨j', x'⟩
<VAR>q : ℚ<GOAL>(q * q).num = q.num * q.num
<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)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 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<VAR>hpos : 0 < (expSeries 𝕂 𝔸).radius<GOAL>HasFDerivAt (fun u => exp 𝕂 (u • x)) (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 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<VAR>hpos : 0 < (expSeries 𝕂 𝔸).radius<GOAL>(fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h) =o[𝓝 0] fun h => h
<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>hpos : 0 < (expSeries 𝕂 𝔸).radius<GOAL>(fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
<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>hpos : 0 < (expSeries 𝕂 𝔸).radius<VAR>this : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)<GOAL>(fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
<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>hpos : 0 < (expSeries 𝕂 𝔸).radius<VAR>this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)<VAR>this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>(fun h => exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h)) =ᶠ[𝓝 0] fun h => exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
<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>hpos : 0 < (expSeries 𝕂 𝔸).radius<VAR>this✝ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)<VAR>this : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>h : 𝕊<VAR>hh : h • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<GOAL>exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h) = exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
<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>hpos : 0 < (expSeries 𝕂 𝔸).radius<VAR>this✝¹ : Tendsto (fun h => h • x) (𝓝 0) (𝓝 0)<VAR>this✝ : ∀ᶠ (h : 𝕊) in 𝓝 0, h • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>h : 𝕊<VAR>hh : h • x ∈ EMetric.ball 0 (expSeries 𝕂 𝔸).radius<VAR>this : Commute (t • x) (h • x)<GOAL>exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 (0 • x) - (ContinuousLinearMap.smulRight 1 x) h) = exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x) - (exp 𝕂 (t • x) • ContinuousLinearMap.smulRight 1 x) h
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M : εNFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>s : σ<VAR>a : α<GOAL>s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs : List (α × α)<VAR>x y z : α<GOAL>applyId ((y, z) :: xs) x = if y = x then z else applyId xs x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Sort w<VAR>inst✝ : DecidableEq α<VAR>xs : List (α × α)<VAR>x y z : α<GOAL>(if h : y = x then some z else dlookup x (map Prod.toSigma xs)).getD x = if y = x then z else (dlookup x (map Prod.toSigma xs)).getD x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : s.sym n = ∅<GOAL>s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>a b : α<VAR>n : ℕ<VAR>h : ¬(s.sym n).Nonempty<GOAL>¬s.Nonempty
<GOAL>(fun i => (fastGrowing 0)^[i] i) = fun n => 2 * n
<VAR>i : ℕ<GOAL>(fastGrowing 0)^[i] i = 2 * i
<VAR>i : ℕ<GOAL>Nat.succ^[i] i = i + i
<VAR>i a b : ℕ<GOAL>Nat.succ^[a] b = b + a
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ZMod p<GOAL>∃ a b, a ^ 2 + b ^ 2 = x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ZMod p<VAR>hp2 : p = 2<GOAL>∃ a b, a ^ 2 + b ^ 2 = x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ZMod p<VAR>hp_odd : p % 2 = 1<GOAL>∃ a b, a ^ 2 + b ^ 2 = x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ZMod p<VAR>hp_odd : p % 2 = 1<VAR>f : (ZMod p)[X] := X ^ 2<VAR>g : (ZMod p)[X] := X ^ 2 - C x<GOAL>∃ a b, a ^ 2 + b ^ 2 = x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ZMod p<VAR>hp_odd : p % 2 = 1<VAR>f : (ZMod p)[X] := X ^ 2<VAR>g : (ZMod p)[X] := X ^ 2 - C x<VAR>a b : ZMod p<VAR>hab : eval a f + eval b g = 0<GOAL>∃ a b, a ^ 2 + b ^ 2 = x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ZMod p<VAR>hp_odd : p % 2 = 1<VAR>f : (ZMod p)[X] := X ^ 2<VAR>g : (ZMod p)[X] := X ^ 2 - C x<VAR>a b : ZMod p<VAR>hab : eval a f + eval b g = 0<GOAL>a ^ 2 + b ^ 2 = x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ZMod p<VAR>hp_odd : p % 2 = 1<VAR>f : (ZMod p)[X] := X ^ 2<VAR>g : (ZMod p)[X] := X ^ 2 - C x<VAR>a b : ZMod p<VAR>hab : eval a f + eval b g = 0<GOAL>a ^ 2 + b ^ 2 - x = 0
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>h : Function.Surjective F.obj<VAR>X : C<GOAL>F.obj X ∈ F.essImage
<VAR>P : ℤ → Prop<VAR>inst✝ : DecidablePred P<VAR>b b' : ℤ<VAR>Hb : ∀ (z : ℤ), P z → b ≤ z<VAR>Hb' : ∀ (z : ℤ), P z → b' ≤ z<VAR>Hinh : ∃ z, P z<VAR>n : ℤ<VAR>hn : P n<VAR>h2n : ∀ (z : ℤ), P z → n ≤ z<VAR>n' : ℤ<VAR>hn' : P n'<VAR>h2n' : ∀ (z : ℤ), P z → n' ≤ z<GOAL>↑⟨n, ⋯⟩ = ↑⟨n', ⋯⟩
<VAR>a b c : Ordinal.{u}<VAR>n : ℕ<GOAL>↑n ♯ a = a + ↑n
<VAR>α : Type u_1<VAR>l : Lists' α true<GOAL>l ⊆ nil → l = nil
<VAR>α : Type u_1<VAR>l : Lists' α true<GOAL>ofList l.toList ⊆ nil → ofList l.toList = nil
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DistribLattice α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f✝ : ι → α<VAR>g : κ → α<VAR>a✝ : α<VAR>f : ι → α<VAR>a : α<GOAL>s.sup' hs f ⊓ a = s.sup' hs fun i => f i ⊓ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DistribLattice α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f✝ : ι → α<VAR>g : κ → α<VAR>a✝ : α<VAR>f : ι → α<VAR>a : α<GOAL>(s.sup' hs fun i => a ⊓ f i) = s.sup' hs fun i => f i ⊓ a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : CompleteSpace E<VAR>e : E<VAR>s : Set X<VAR>s_meas : MeasurableSet s<GOAL>∫ (x : X), s.indicator (fun x => e) x ∂μ = (μ s).toReal • e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g h : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hh : AEStronglyMeasurable h μ<GOAL>∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g h : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hh : AEStronglyMeasurable h μ<GOAL>∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g h : α → β<VAR>hf : AEStronglyMeasurable f μ<VAR>hh : AEStronglyMeasurable h μ<VAR>a : α<GOAL>edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>n : ℤ<GOAL>pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] (↑n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>n : ℤ<GOAL>pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] ↑(n + 1)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : PartialOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | τ ω = i} = {ω | τ ω ≤ i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < i), {ω | τ ω ≤ j}<GOAL>MeasurableSet ({ω | τ ω ≤ i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < i), {ω | τ ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : PartialOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | τ ω = i} = {ω | τ ω ≤ i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < i), {ω | τ ω ≤ j}<GOAL>MeasurableSet (⋃ j ∈ Set.range τ, ⋃ (_ : j < i), {ω | τ ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : PartialOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | τ ω = i} = {ω | τ ω ≤ i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < i), {ω | τ ω ≤ j}<VAR>j : ι<VAR>x✝ : j ∈ Set.range τ<GOAL>MeasurableSet (⋃ (_ : j < i), {ω | τ ω ≤ j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : PartialOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | τ ω = i} = {ω | τ ω ≤ i} \ ⋃ j ∈ Set.range τ, ⋃ (_ : j < i), {ω | τ ω ≤ j}<VAR>j : ι<VAR>x✝ : j ∈ Set.range τ<GOAL>MeasurableSet (if j < i then {ω | τ ω ≤ j} else ∅)
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>L₃ : Type w₁<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L₁<VAR>inst✝⁴ : LieRing L₂<VAR>inst✝³ : LieRing L₃<VAR>inst✝² : LieAlgebra R L₁<VAR>inst✝¹ : LieAlgebra R L₂<VAR>inst✝ : LieAlgebra R L₃<VAR>f_inv : L₂ → L₁<VAR>f : L₁ → L₂<VAR>map_add'✝¹ : ∀ (x y : L₁), f (x + y) = f x + f y<VAR>map_smul'✝¹ : ∀ (m : R) (x : L₁), { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x<VAR>map_lie'✝¹ : ∀ {x y : L₁}, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, y⁆ = ⁅{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun y⁆<VAR>left_inv✝¹ : LeftInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>right_inv✝¹ : Function.RightInverse f_inv (↑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ }).toFun<VAR>g_inv : L₂ → L₁<VAR>g : L₁ → L₂<VAR>map_add'✝ : ∀ (x y : L₁), g (x + y) = g x + g y<VAR>map_smul'✝ : ∀ (m : R) (x : L₁), { toFun := g, map_add' := map_add'✝ }.toFun (m • x) = (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x<VAR>map_lie'✝ : ∀ {x y : L₁}, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, y⁆ = ⁅{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun y⁆<VAR>left_inv✝ : LeftInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>right_inv✝ : Function.RightInverse g_inv (↑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }).toFun<VAR>h : { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toLinearEquiv = { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv, left_inv := left_inv✝, right_inv := right_inv✝ }.toLinearEquiv<GOAL>{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹, invFun := f_inv, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } = { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝, invFun := g_inv, left_inv := left_inv✝, right_inv := right_inv✝ }