ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>gp : Pair K<VAR>nth_s_eq : (of v).s.get? n = some gp<VAR>ifp : IntFractPair K<VAR>stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp<VAR>this : gp = { a := 1, b := ↑ifp.b }<GOAL>gp.a = 1 ∧ ∃ z, gp.b = ↑z
<VAR>A : Type v<VAR>inst✝⁶ : Ring A<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Algebra R A<VAR>B : Type w<VAR>C : Type w₁<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring C<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : Algebra R C<VAR>f✝ : A →ₐ[R] B<VAR>g✝ : B →ₐ[R] C<VAR>f g : A →ₐ[R] B<VAR>h : f.toLieHom = g.toLieHom<VAR>a : A<GOAL>f a = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>inst✝ : Countable ι<VAR>κ : ι → Kernel α β<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum κ) a) s = ∑' (n : ι), ((κ n) a) s
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m<GOAL>(bind₁ (W_ R)) (xInTermsOfW p R n) = X n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m<GOAL>(W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))) * (algebraMap R (MvPolynomial ℕ R)) (⅟↑p ^ n) = X n * C (↑p ^ n) * C (⅟↑p ^ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m<GOAL>W_ R n - ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = X n * C (↑p ^ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m<GOAL>∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n - x) = ∑ x ∈ range n, (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m<GOAL>∀ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n - x) = (bind₁ (W_ R)) (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m<VAR>i : ℕ<VAR>h : i ∈ range n<GOAL>C (↑p ^ i) * X i ^ p ^ (n - i) = (bind₁ (W_ R)) (C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m<VAR>i : ℕ<VAR>h : i < n<GOAL>C (↑p ^ i) * X i ^ p ^ (n - i) = (bind₁ (W_ R)) (C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i))
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : T<VAR>p₁ p₂ : LocalizedModule S A<GOAL>p₁ * x • p₂ = x • (p₁ * p₂)
<VAR>R : Type u<VAR>inst✝⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>T : Type u_1<VAR>inst✝⁴ : CommSemiring T<VAR>inst✝³ : Algebra R T<VAR>inst✝² : IsLocalization S T<VAR>A : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : T<VAR>a₁ s₁ : A<VAR>a₂ s₂ : ↥S<GOAL>mk a₁ a₂ * x • mk s₁ s₂ = x • (mk a₁ a₂ * mk s₁ s₂)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>inst✝ : T2Space M<VAR>a b : ℝ<VAR>hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>hγ : IsIntegralCurve γ v<VAR>hγ' : IsIntegralCurve γ' v<VAR>h : γ t₀ = γ' t₀<VAR>t : ℝ<GOAL>γ t = γ' t
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>inst✝ : T2Space M<VAR>a b : ℝ<VAR>hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>hγ : IsIntegralCurve γ v<VAR>hγ' : IsIntegralCurve γ' v<VAR>h : γ t₀ = γ' t₀<VAR>t T : ℝ<VAR>ht₀ : t ∈ Ioo (-T) T<VAR>ht : t₀ ∈ Ioo (-T) T<GOAL>γ t = γ' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>x ∈ Ioc a b ∪ Ioi c ↔ x ∈ Ioi (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<GOAL>p = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<VAR>h : { center := p, radius := r }.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ Metric.sphere { center := p, radius := r }.center { center := p, radius := r }.radius → { center := p, radius := r } = s.circumsphere<GOAL>p = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<VAR>h : Set.range s.points ⊆ Metric.sphere p r → p = s.circumsphere.center ∧ r = s.circumsphere.radius<GOAL>p = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<VAR>h : (∀ p_1 ∈ Set.range s.points, p_1 ∈ { center := p, radius := r }) → p = s.circumsphere.center ∧ r = s.circumsphere.radius<GOAL>p = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<VAR>h : p = s.circumsphere.center ∧ r = s.circumsphere.radius<GOAL>p = s.circumcenter
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>proj : Z → B<VAR>e✝ : Pretrivialization F proj<VAR>x : Z<VAR>e f : Pretrivialization F proj<GOAL>f.target ∩ ↑f.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ univ
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : DifferentiableAt 𝕜 (fun y => -f y) x<GOAL>DifferentiableAt 𝕜 f x
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>m : M<VAR>v : Fin n → M<GOAL>(ι R) (Matrix.vecCons m v 0) * (ιMulti R n) (Matrix.vecTail (Matrix.vecCons m v)) = ((LinearMap.mulLeft R ((ι R) m)).compAlternatingMap (ιMulti R n)) v
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>m : M<VAR>v : Fin n → M<GOAL>(ι R) (Matrix.vecCons m v 0) * (ιMulti R n) v = ((LinearMap.mulLeft R ((ι R) m)).compAlternatingMap (ιMulti R n)) v
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>F✝ : Filter ι<VAR>inst✝⁷ : F✝.NeBot<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : OrderTopology R<VAR>inst✝³ : ConditionallyCompleteLinearOrder S<VAR>inst✝² : TopologicalSpace S<VAR>inst✝¹ : OrderTopology S<VAR>F : Filter R<VAR>inst✝ : F.NeBot<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>f_cont : ContinuousAt f F.limsSup<VAR>bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝<VAR>cobdd : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) F) _auto✝<GOAL>f F.limsSup = liminf f F
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>F✝ : Filter ι<VAR>inst✝⁷ : F✝.NeBot<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : OrderTopology R<VAR>inst✝³ : ConditionallyCompleteLinearOrder S<VAR>inst✝² : TopologicalSpace S<VAR>inst✝¹ : OrderTopology S<VAR>F : Filter R<VAR>inst✝ : F.NeBot<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>f_cont : ContinuousAt f F.limsSup<VAR>bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝<VAR>cobdd : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) F) _auto✝<GOAL>f F.limsSup ≤ liminf f F
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>F✝ : Filter ι<VAR>inst✝⁷ : F✝.NeBot<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : OrderTopology R<VAR>inst✝³ : ConditionallyCompleteLinearOrder S<VAR>inst✝² : TopologicalSpace S<VAR>inst✝¹ : OrderTopology S<VAR>F : Filter R<VAR>inst✝ : F.NeBot<VAR>f : R → S<VAR>f_decr : Antitone f<VAR>f_cont : ContinuousAt f F.limsSup<VAR>bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝<VAR>cobdd : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) F) _auto✝<GOAL>liminf f F ≤ f F.limsSup
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<GOAL>HasFDerivAt g (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<VAR>this : (fun x => g x - g a - f'.symm (x - a)) =O[𝓝 a] fun x => f' (g x - g a) - (x - a)<GOAL>HasFDerivAt g (↑f'.symm) a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<VAR>this : (fun x => g x - g a - f'.symm (x - a)) =O[𝓝 a] fun x => f' (g x - g a) - (x - a)<GOAL>(fun x => f' (g x - g a) - (x - a)) =o[𝓝 a] fun x' => x' - a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<GOAL>(fun x => f' (g x - g a) - (x - a)) =o[𝓝 a] fun x' => x' - a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<GOAL>∀ (x : F), f (g x) = x → (fun x => ↑f' (g x - g a) - (f (g x) - f (g a))) x = f' (g x - g a) - (x - a)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>g : F → E<VAR>a : F<VAR>hg : ContinuousAt g a<VAR>hf : HasFDerivAt f (↑f') (g a)<VAR>hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y<GOAL>((fun x' => x' - g a) ∘ g) =O[𝓝 a] fun x' => x' - a
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>x : M<GOAL>x ∈ f.eigenspace μ ↔ f x = μ • x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>W : α → Sort w<VAR>Z : β → Sort z<VAR>h₁ : α ≃ β<VAR>h₂ : (a : α) → W a ≃ Z (h₁ a)<VAR>f : (a : α) → W a<VAR>a : α<GOAL>(h₁.piCongr h₂) f (h₁ a) = (h₂ a) (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>v w : VectorMeasure α M<VAR>i j : Set α<VAR>hi : ¬MeasurableSet i<GOAL>restrict 0 i ≤ v.restrict i
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>#((n : ℕ) × L.Term (α ⊕ Fin n)) = max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>#((n : ℕ) × L.Term (α ⊕ Fin n)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<GOAL>max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>A : Type u_1<VAR>inst✝³ : Semiring A<VAR>inst✝² : Module A V<VAR>inst✝¹ : SMul K A<VAR>inst✝ : IsScalarTower K A V<VAR>h : finrank K V = 1<GOAL>IsSimpleOrder (Submodule A V)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>A : Type u_1<VAR>inst✝³ : Semiring A<VAR>inst✝² : Module A V<VAR>inst✝¹ : SMul K A<VAR>inst✝ : IsScalarTower K A V<VAR>h : finrank K V = 1<VAR>this : Nontrivial V<GOAL>IsSimpleOrder (Submodule A V)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>A : Type u_1<VAR>inst✝³ : Semiring A<VAR>inst✝² : Module A V<VAR>inst✝¹ : SMul K A<VAR>inst✝ : IsScalarTower K A V<VAR>h : finrank K V = 1<VAR>this : Nontrivial V<VAR>S : Submodule A V<VAR>hn : ¬S = ⊥<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>A : Type u_1<VAR>inst✝³ : Semiring A<VAR>inst✝² : Module A V<VAR>inst✝¹ : SMul K A<VAR>inst✝ : IsScalarTower K A V<VAR>h : finrank K V = 1<VAR>this : Nontrivial V<VAR>S : Submodule A V<VAR>hn : ¬restrictScalars K S = restrictScalars K ⊥<GOAL>restrictScalars K S = restrictScalars K ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>A : Type u_1<VAR>inst✝³ : Semiring A<VAR>inst✝² : Module A V<VAR>inst✝¹ : SMul K A<VAR>inst✝ : IsScalarTower K A V<VAR>h : finrank K V = 1<VAR>this✝ : Nontrivial V<VAR>S : Submodule A V<VAR>hn : ¬restrictScalars K S = restrictScalars K ⊥<VAR>this : FiniteDimensional K V<GOAL>restrictScalars K S = restrictScalars K ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>A : Type u_1<VAR>inst✝³ : Semiring A<VAR>inst✝² : Module A V<VAR>inst✝¹ : SMul K A<VAR>inst✝ : IsScalarTower K A V<VAR>h : finrank K V = 1<VAR>this✝ : Nontrivial V<VAR>S : Submodule A V<VAR>hn : ¬restrictScalars K S = restrictScalars K ⊥<VAR>this : FiniteDimensional K V<GOAL>finrank K V ≤ finrank K ↥(restrictScalars K S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>p : G.Walk a a<VAR>H : SimpleGraph β<VAR>f : G →g H<VAR>hf : Bijective ⇑f<VAR>hp : p.IsHamiltonianCycle<GOAL>((Walk.map f p).tail ⋯).IsHamiltonian
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>p : G.Walk a a<VAR>H : SimpleGraph β<VAR>f : G →g H<VAR>hf : Bijective ⇑f<VAR>hp : p.IsHamiltonianCycle<GOAL>∀ (x : α), (List.count x p.support - if f x = (List.map (⇑f) p.support).head ⋯ then 1 else 0) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>H : SimpleGraph β<VAR>f : G →g H<VAR>hf : Bijective ⇑f<VAR>x v✝ : α<VAR>y : G.Adj a v✝<VAR>p : G.Walk v✝ a<VAR>hp : (cons y p).IsHamiltonianCycle<GOAL>(List.count x (cons y p).support - if f x = (List.map (⇑f) (cons y p).support).head ⋯ then 1 else 0) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>H : SimpleGraph β<VAR>f : G →g H<VAR>hf : Bijective ⇑f<VAR>x v✝ : α<VAR>y : G.Adj a v✝<VAR>p : G.Walk v✝ a<VAR>hp : (cons y p).IsHamiltonianCycle<GOAL>List.count x p.support = 1
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b✝ c u a : αˣ<VAR>b : α<GOAL>↑a * (↑a⁻¹ * b) = b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>a ≤ |b| ↔ b ≤ -a ∨ a ≤ b
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NeZero 2<VAR>a b c x✝ : K<VAR>ha : a ≠ 0<VAR>s : K<VAR>h : discrim a b c = s * s<VAR>x : K<GOAL>a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NeZero 2<VAR>a b c x✝ : K<VAR>ha : a ≠ 0<VAR>s : K<VAR>h : discrim a b c = s * s<VAR>x : K<GOAL>s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NeZero 2<VAR>a b c x✝ : K<VAR>ha : a ≠ 0<VAR>s : K<VAR>h : discrim a b c = s * s<VAR>x : K<GOAL>s = 2 * a * x + b ∨ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b + s ∨ x * (2 * a) = -b - s
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NeZero 2<VAR>a b c x✝ : K<VAR>ha : a ≠ 0<VAR>s : K<VAR>h : discrim a b c = s * s<VAR>x : K<GOAL>s = 2 * a * x + b ↔ x * (2 * a) = -b + s
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NeZero 2<VAR>a b c x✝ : K<VAR>ha : a ≠ 0<VAR>s : K<VAR>h : discrim a b c = s * s<VAR>x : K<GOAL>s = -b + -(2 * a * x) ↔ x * (2 * a) = -b - s
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : G < 0<GOAL>False
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : G < 0<VAR>h' : -0 < -G<GOAL>False
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : G < 0<VAR>h' : 0 < G<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ f.range, (T (↑f ⁻¹' {x})) x = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>x✝ : x ∈ f.range<GOAL>(T (↑f ⁻¹' {x})) x = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>x✝ : x ∈ f.range<VAR>hx0 : ¬x = 0<GOAL>(T (↑f ⁻¹' {x})) x = 0
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>a : R<VAR>x✝ : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>({ toFinsupp := toFinsupp✝ }.update n a).coeff x✝ = Function.update { toFinsupp := toFinsupp✝ }.coeff n a x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m m' : MeasurableSpace α<VAR>hsep : CountablySeparated α<VAR>h : m ≤ m'<GOAL>CountablySeparated α