ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : IsIrrefl α r<VAR>s' s t : Multiset α<VAR>a : α<GOAL>(∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a → (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : IsIrrefl α r<VAR>s' s t : Multiset α<VAR>a : α<GOAL>(∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t → (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a
<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>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>hn : 1 ≤ n<GOAL>MDifferentiableWithinAt I I' f s x
<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>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>hn : 1 ≤ n<GOAL>MDifferentiableWithinAt I I' f (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
<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>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>hn : 1 ≤ n<GOAL>ContinuousWithinAt f (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)) (↑(extChartAt I x) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>s : Set α<VAR>t : Set β<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>(μ ⊗ₘ κ) (s ×ˢ t) = ∫⁻ (a : α) in s, (κ a) t ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>s : Set α<VAR>t : Set β<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s ×ˢ t) ∂μ = ∫⁻ (a : α), s.indicator (fun a => (κ a) t) a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>s : Set α<VAR>t : Set β<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>a : α<GOAL>(κ a) (Prod.mk a ⁻¹' s ×ˢ t) = s.indicator (fun a => (κ a) t) a
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>IsUnit A.det
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>∃ b, A.det * b = 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>A.det * A.det = 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>(J l R).det * (A.det * A.det) = (J l R).det * 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A ∈ symplecticGroup l R<GOAL>(J l R).det * (A.det * A.det) = (J l R).det
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A * J l R * Aᵀ = J l R<GOAL>(J l R).det * (A.det * A.det) = (J l R).det
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : (A * J l R * Aᵀ).det = (J l R).det<GOAL>(J l R).det * (A.det * A.det) = (J l R).det
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : A.det * (J l R).det * A.det = (J l R).det<GOAL>(J l R).det * (A.det * A.det) = (J l R).det
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<VAR>hA : (J l R).det * (A.det * A.det) = (J l R).det<GOAL>(J l R).det * (A.det * A.det) = (J l R).det
<VAR>x : ℂ<GOAL>1 ^ x = 1
<VAR>x : ℂ<GOAL>(if 1 = 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : IsBigOWith c l f g<GOAL>f =O[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : IsBigOWith c l f g<GOAL>∃ c, IsBigOWith c l f g
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>sepDegree F F = 1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j = 𝟙 (pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>(t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) = pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>(t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) = pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)
<VAR>m n✝ n : ℕ<VAR>a : ℤ<VAR>inst✝ : NeZero n<GOAL>↑(↑a).val = a % ↑n
<VAR>m n✝ n : ℕ<VAR>a : ℤ<VAR>inst✝ : NeZero n<VAR>hle : 0 ≤ ↑(↑a).val<GOAL>↑(↑a).val = a % ↑n
<VAR>m n✝ n : ℕ<VAR>a : ℤ<VAR>inst✝ : NeZero n<VAR>hle : 0 ≤ ↑(↑a).val<VAR>hlt : ↑(↑a).val < ↑n<GOAL>↑(↑a).val = a % ↑n
<VAR>m n✝ n : ℕ<VAR>a : ℤ<VAR>inst✝ : NeZero n<VAR>hle : 0 ≤ ↑(↑a).val<VAR>hlt : ↑(↑a).val < ↑n<GOAL>↑(↑a).val % ↑n = a % ↑n
<VAR>α : Type u<VAR>β : Type u_1<VAR>t✝ : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ s t : Set α<GOAL>IsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t
<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>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s✝ t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>x₀ : 𝕜<VAR>s : Set 𝕜<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖deriv f x₀‖ ≤ ↑C
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝² : CommRing R<VAR>L : Type w<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>f : X → L<VAR>a b : lib R X<VAR>h : Rel R X a b<GOAL>(liftAux R f) a = (liftAux R f) b
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>x✝¹ x✝ : Fin (n + 1)<VAR>h : x✝¹.succAbove = x✝.succAbove<GOAL>x✝¹ = x✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝ : IsStrictOrder α r<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
<VAR>E : Type u_1<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>x : E<GOAL>gaugeRescale s t (c • x) = c • gaugeRescale s t x
<VAR>E : Type u_1<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>x : E<GOAL>(c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>c : F<VAR>hb : Tendsto f (cocompact E) (𝓝 c)<GOAL>f = const E c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>c : F<VAR>hb : Tendsto f (cocompact E) (𝓝 c)<VAR>h_bdd : Bornology.IsBounded (range f)<GOAL>f = const E c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>c : F<VAR>hb : Tendsto f (cocompact E) (𝓝 c)<VAR>h_bdd : Bornology.IsBounded (range f)<VAR>c' : F<VAR>hc' : f = const E c'<GOAL>f = const E c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>hf : Differentiable ℂ f<VAR>c : F<VAR>hb : Tendsto f (cocompact E) (𝓝 c)<VAR>h_bdd : Bornology.IsBounded (range f)<VAR>c' : F<VAR>hc' : f = const E c'<GOAL>c = c'
<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>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Algebra R 𝕜<VAR>p : 𝕜[X]<VAR>q : R[X]<VAR>x : 𝕜<GOAL>HasStrictDerivAt (fun x => (aeval x) q) ((aeval x) (derivative q)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<GOAL>Subsingleton (Quot r) ↔ EqvGen r = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<GOAL>(∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ EqvGen r i i_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>a : α<GOAL>(∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ EqvGen r a i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>a b : α<GOAL>mk r a = mk r b ↔ ⊤ ≤ EqvGen r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>a b : α<GOAL>EqvGen r a b ↔ ⊤ ≤ EqvGen r a b
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : NormedSpace ℝ 𝕜<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>Convex ℝ (p.closedBall x r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : NormedSpace ℝ 𝕜<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<GOAL>Convex ℝ (⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ)
<VAR>n k : ℕ<GOAL>(n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)
<VAR>n k : ℕ<GOAL>(n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace<VAR>x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).presheaf.obj (op U✝))<GOAL>(((sheafedSpaceMap (f ≫ g)).c ≫ whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf).app (op U✝)) x✝ = ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝)) x✝
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace<VAR>x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).presheaf.obj (op U✝))<GOAL>(comap (f ≫ g) (unop (op U✝)) ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ⋯ ≫ (sheafedSpaceObj T).presheaf.map ((𝟙 (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op).app (op U✝))) x✝ = ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝)) x✝
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace<VAR>x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).presheaf.obj (op U✝))<GOAL>((comap g ?w.w.V ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ?w.w.hVW).comp (comap f (unop (op U✝)) ?w.w.V ?w.w.hUV)) x✝ = ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝)) x✝
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace<VAR>x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).presheaf.obj (op U✝))<GOAL>TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑S)
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace<VAR>x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).presheaf.obj (op U✝))<GOAL>∀ p ∈ ?w.w.V, (PrimeSpectrum.comap f) p ∈ unop (op U✝)
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace<VAR>x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).presheaf.obj (op U✝))<GOAL>∀ p ∈ (TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝)), (PrimeSpectrum.comap g) p ∈ ?w.w.V
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>h : Fintype.card n = 0<VAR>M : Matrix n n R<GOAL>M.det = 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>h : IsEmpty n<VAR>M : Matrix n n R<GOAL>M.det = 1
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>κ : ι → Type u_2<VAR>t : (i : ι) → Set (κ i)<VAR>ht : ∀ (i : ι), (t i).Finite<GOAL>(univ.pi t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>κ : ι → Type u_2<VAR>t : (i : ι) → Set (κ i)<VAR>ht : ∀ (i : ι), (t i).Finite<VAR>val✝ : Fintype ι<GOAL>(univ.pi t).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>κ : ι → Type u_2<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Finset (κ i)<GOAL>(univ.pi fun i => ↑(t i)).Finite
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>ω ^ 2 ^ (p' + 2) = (ω ^ 2 ^ (p' + 1)) ^ 2
<VAR>p' : ℕ<VAR>h : lucasLehmerResidue (p' + 2) = 0<GOAL>(ω ^ 2 ^ (p' + 1)) ^ 2 = (-1) ^ 2
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝⁷ : MonoidWithZero M₀<VAR>inst✝⁶ : GroupWithZero G₀<VAR>inst✝⁵ : Nontrivial M₀<VAR>inst✝⁴ : MonoidWithZero M₀'<VAR>inst✝³ : FunLike F G₀ M₀<VAR>inst✝² : MonoidWithZeroHomClass F G₀ M₀<VAR>inst✝¹ : FunLike F' G₀ M₀'<VAR>f✝ : F<VAR>a : G₀<VAR>inst✝ : MonoidWithZeroHomClass F' G₀ M₀'<VAR>f g : F'<VAR>h : f a = g a<GOAL>f a⁻¹ = g a⁻¹
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝⁷ : MonoidWithZero M₀<VAR>inst✝⁶ : GroupWithZero G₀<VAR>inst✝⁵ : Nontrivial M₀<VAR>inst✝⁴ : MonoidWithZero M₀'<VAR>inst✝³ : FunLike F G₀ M₀<VAR>inst✝² : MonoidWithZeroHomClass F G₀ M₀<VAR>inst✝¹ : FunLike F' G₀ M₀'<VAR>f✝ : F<VAR>inst✝ : MonoidWithZeroHomClass F' G₀ M₀'<VAR>f g : F'<VAR>h : f 0 = g 0<GOAL>f 0⁻¹ = g 0⁻¹
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝⁷ : MonoidWithZero M₀<VAR>inst✝⁶ : GroupWithZero G₀<VAR>inst✝⁵ : Nontrivial M₀<VAR>inst✝⁴ : MonoidWithZero M₀'<VAR>inst✝³ : FunLike F G₀ M₀<VAR>inst✝² : MonoidWithZeroHomClass F G₀ M₀<VAR>inst✝¹ : FunLike F' G₀ M₀'<VAR>f✝ : F<VAR>a : G₀<VAR>inst✝ : MonoidWithZeroHomClass F' G₀ M₀'<VAR>f g : F'<VAR>h : f a = g a<VAR>ha : a ≠ 0<GOAL>f a⁻¹ = g 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 : α → β<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>a : α<GOAL>↑‖f a + g a‖₊ ≤ ↑‖f a‖₊ + ↑‖g a‖₊
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<GOAL>⇑(h.collectedBasis v) = fun a => ↑((v a.fst) a.snd)
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>a : (i : ι) × α i<GOAL>(h.collectedBasis v) a = ↑((v a.fst) a.snd)
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>a : (i : ι) × α i<GOAL>(toModule R ι M fun i => (A i).subtype) ((DFinsupp.mapRange.linearEquiv fun i => (v i).repr).symm (DFinsupp.single a.fst (Finsupp.single a.snd 1))) = ↑((v a.fst) a.snd)
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>a : (i : ι) × α i<GOAL>(toModule R ι M fun i => (A i).subtype) ((DFinsupp.mapRange.linearEquiv fun i => (v i).repr.symm) (DFinsupp.single a.fst (Finsupp.single a.snd 1))) = ↑((v a.fst) a.snd)
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>a : (i : ι) × α i<GOAL>(toModule R ι M fun i => (A i).subtype) (DFinsupp.mapRange (fun i x => (v i).repr.symm x) ⋯ (DFinsupp.single a.fst (Finsupp.single a.snd 1))) = ↑((v a.fst) a.snd)
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>a : (i : ι) × α i<GOAL>((DFinsupp.lsum ℕ) fun i => (A i).subtype) (DFinsupp.single a.fst ((v a.fst) a.snd)) = ↑((v a.fst) a.snd)
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A : ι → Submodule R M<VAR>h : IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>a : (i : ι) × α i<GOAL>(A a.fst).subtype ((v a.fst) a.snd) = ↑((v a.fst) a.snd)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>r r' : R<VAR>eq1 : r • y = r' • y<GOAL>(extendIdealTo i f h y) r = (extendIdealTo i f h y) r'