ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<VAR>U : (OpenNhds x)ᵒᵖ<GOAL>colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ (forgetStalk IM I M R x).inv = (forget CommRingCat).map (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<VAR>U : (OpenNhds x)ᵒᵖ<GOAL>⇑(colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U) ≫ (forgetStalk IM I M R x).hom = ⇑(colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U) ≫ (forgetStalk IM I M R x).hom
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)<VAR>hg : ContDiffAt 𝕜 m g x₀<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (f x) (g x)) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)<VAR>hg : ContDiffAt 𝕜 m g x₀<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) univ (g x)) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)<VAR>hg : ContDiffAt 𝕜 m g x₀<VAR>hmn : m + 1 ≤ n<GOAL>univ ⊆ g ⁻¹' univ
<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>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hL : Tendsto h L L'<GOAL>HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L
<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>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hL : Tendsto h L L'<GOAL>HasDerivAtFilter (h₂ ∘ h) (h' * h₂') x L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝³ : CommRing α<VAR>inst✝² : StarRing α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m m α<VAR>hA : A.IsHermitian<GOAL>A⁻¹.IsHermitian
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : Group G<VAR>s : Subgroup G<VAR>t : Set (G ⧸ s)<GOAL>Nat.card ↑(mk ⁻¹' t) = Nat.card ↥s * Nat.card ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>c : Set (Set α)<GOAL>⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b ∈ c, a ∉ b
<VAR>f : ℕ → ℂ<VAR>s a : ℂ<VAR>hf : LSeriesHasSum f s a<GOAL>LSeriesHasSum (-f) s (-a)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.194255 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.199706 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄ = pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s, HasFDerivAt f✝ (f'✝ x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s) x<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hx : HasFDerivAt f' f'' x<VAR>v w : E<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s, HasFDerivAt f✝ (f'✝ x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s) x<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hx : HasFDerivAt f' f'' x<VAR>v w : E<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : Metric.ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x}<GOAL>(f'' v) w = (f'' w) v
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>s_conv : Convex ℝ s<VAR>f✝ : E → F<VAR>f'✝ : E → E →L[ℝ] F<VAR>f''✝ : E →L[ℝ] E →L[ℝ] F<VAR>hf✝ : ∀ x ∈ interior s, HasFDerivAt f✝ (f'✝ x) x<VAR>x : E<VAR>xs : x ∈ s<VAR>hx✝ : HasFDerivWithinAt f'✝ f''✝ (interior s) x<VAR>f : E → F<VAR>f' : E → E →L[ℝ] F<VAR>f'' : E →L[ℝ] E →L[ℝ] F<VAR>hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hx : HasFDerivAt f' f'' x<VAR>v w : E<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : Metric.ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x}<VAR>A : (interior (Metric.ball x ε)).Nonempty<GOAL>(f'' v) w = (f'' w) v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set α → Prop<VAR>s : Set α<VAR>h : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<GOAL>∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set α → Prop<VAR>s : Set α<VAR>h : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<VAR>S : Set (Set α)<VAR>hSc : S.Countable<VAR>hSp : ∀ s ∈ S, p s<VAR>hS : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y<GOAL>∃ t ⊆ s, t.Subsingleton ∧ t ∈ l
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>⌊√↑a⌋ = ↑a.sqrt
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>↑↑a.sqrt ≤ √↑a ∧ √↑a < ↑↑a.sqrt + 1
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
<VAR>z : ℂ<GOAL>jacobiTheta₂' z 0 = -2 * ↑π / (-I * 0) ^ (3 / 2) * jacobiTheta₂'' z (-1 / 0)
<VAR>z τ : ℂ<VAR>hτ : τ ≠ 0<GOAL>jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
<VAR>z τ : ℂ<VAR>hτ : τ ≠ 0<VAR>aux1 : -2 * ↑π / (2 * ↑π * I) = I<GOAL>jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)
<VAR>z τ : ℂ<VAR>hτ : τ ≠ 0<VAR>aux1 : -2 * ↑π / (2 * ↑π * I) = I<GOAL>1 / (-I * τ) ^ (3 / 2) * (-I * cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) = 1 / (-I * τ) ^ (3 / 2) * (-2 * ↑π * jacobiTheta₂'' z (-1 / τ))
<VAR>z τ : ℂ<VAR>hτ : τ ≠ 0<VAR>aux1 : -2 * ↑π / (2 * ↑π * I) = I<GOAL>-I * cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ)) = -2 * ↑π * jacobiTheta₂'' z (-1 / τ)
<VAR>z τ : ℂ<VAR>hτ : τ ≠ 0<VAR>aux1 : -2 * ↑π / (2 * ↑π * I) = I<GOAL>I * (cexp (-(↑π * I * z ^ 2 / τ)) * -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) = I * (cexp (-(↑π * I * z ^ 2 / τ)) * (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))
<VAR>z τ : ℂ<VAR>hτ : τ ≠ 0<VAR>aux1 : -2 * ↑π / (2 * ↑π * I) = I<GOAL>-(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) = -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>S T : NonUnitalSubalgebra R A<GOAL>∀ {x : A}, x ∈ S → x ∈ S ⊔ T
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>S T : NonUnitalSubalgebra R A<GOAL>S ≤ S ⊔ T
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ range (n + 1), ↑((n + 1).choose k) * bernoulli' k = ↑(n + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>(↑n + 1) * ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k = ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>∑ x ∈ range n, (↑n + 1) * (↑(n.choose x) / (↑n - ↑x + 1)) * bernoulli' x = ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n k : ℕ<VAR>hk : k ∈ range n<GOAL>(↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) * bernoulli' k = ↑(n.succ.choose k) * bernoulli' k
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n k : ℕ<VAR>hk : k ∈ range n<VAR>this : ↑(n - k) + 1 ≠ 0<GOAL>(↑n + 1) * (↑(n.choose k) / (↑n - ↑k + 1)) = ↑(n.succ.choose k)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n k : ℕ<VAR>hk : k ∈ range n<VAR>this : ↑(n - k) + 1 ≠ 0<GOAL>↑(n.choose k) * (↑n + 1) = ↑((n + 1).choose k) * (↑(n - k) + 1)
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<GOAL>vanishingIdeal (zeroLocus I) = I.radical
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<GOAL>vanishingIdeal (zeroLocus I) = I.jacobson
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<GOAL>∀ b ∈ {J | I ≤ J ∧ J.IsMaximal}, vanishingIdeal (zeroLocus I) ≤ b
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>p : MvPolynomial σ k<VAR>hp : p ∈ I.jacobson<VAR>x : σ → k<VAR>hx : x ∈ zeroLocus I<GOAL>(eval x) p = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.δ i.castSucc ≫ X.σ i = 𝟙 (X.obj [n])
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : NonTorsionWeight w<VAR>s : σ<VAR>h : w s = 0<GOAL>False
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : NonTorsionWeight w<VAR>s : σ<VAR>h : 1 • w s = 0<GOAL>False
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : NonTorsionWeight w<VAR>s : σ<VAR>h : 1 • w s = 0<GOAL>1 = 0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>θ : Real.Angle<GOAL>x = (o.rotation θ) x ↔ x = 0 ∨ θ = 0
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<VAR>x_out : x ∉ thickening δ E<GOAL>(thickenedIndicator δ_pos E) x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>n : Type u_3<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Fintype n<VAR>a : R<VAR>i : n<GOAL>∑ x : n, Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>S : Set (Submonoid M)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : β → α → β<VAR>b : β<VAR>a : α<VAR>l : List α<GOAL>(scanl f b l).get? 0 = some b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : LinearOrder M<VAR>inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>hl : l ≠ []<VAR>f g : ι → M<VAR>h : (map f l).prod ≤ (map g l).prod<GOAL>∃ x ∈ l, f x ≤ g x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : LinearOrder M<VAR>inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>hl : l ≠ []<VAR>f g : ι → M<VAR>h : ∀ x ∈ l, g x < f x<GOAL>(map g l).prod < (map f l).prod
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hι : Cardinal.lift.{v, u} #ι < c.ord.cof<VAR>hf : ∀ (i : ι), f i < c<GOAL>iSup f < c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hι : Cardinal.lift.{v, u} #ι < c.ord.cof<VAR>hf : ∀ (i : ι), f i < c<GOAL>⨆ i, (f i).ord < c.ord
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hι : Cardinal.lift.{v, u} #ι < c.ord.cof<VAR>hf : ∀ (i : ι), f i < c<VAR>i : ι<GOAL>(f i).ord < c.ord
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hι : Cardinal.lift.{v, u} #ι < c.ord.cof<VAR>hf : ∀ (i : ι), f i < c<VAR>i : ι<GOAL>f i < c
<VAR>p' : ℕ<VAR>h : sZMod (p' + 2) (p' + 2 - 2) = 0<GOAL>∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>h : ↑(s (p' + 2 - 2)) = 0<GOAL>∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>h : 2 ^ (p' + 2) - 1 ∣ s p'<GOAL>∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>h : s p' = (2 ^ (p' + 2) - 1) * k<GOAL>∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>h : s p' = (2 ^ (p' + 2) - 1) * k<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>h : ↑(s p') = ↑((2 ^ (p' + 2) - 1) * k)<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>h : ω ^ 2 ^ p' + ωb ^ 2 ^ p' = ↑((2 ^ (p' + 2) - 1) * k)<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)<VAR>t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>h : ω ^ 2 ^ (p' + 1) + 1 = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)<VAR>t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>h : ω ^ 2 ^ (p' + 1) + 1 = ↑(2 ^ (p' + 2) - 1) * ↑k * ω ^ 2 ^ p'<VAR>t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>h : ω ^ 2 ^ (p' + 1) + 1 = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p'<VAR>t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)<VAR>h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>p' : ℕ<VAR>k : ℤ<VAR>t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)<VAR>h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1<VAR>this : 1 ≤ 2 ^ (p' + 2)<GOAL>ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>hM : Finite R M<VAR>f : M →ₗ[R] N<VAR>hf : Surjective ⇑f<GOAL>⊤.FG
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>hM : Finite R M<VAR>f : M →ₗ[R] N<VAR>hf : Surjective ⇑f<GOAL>(map f ⊤).FG
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>↑(lowerClosure s) * t = ↑(lowerClosure (s * t))
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>t * ↑(lowerClosure s) = ↑(lowerClosure (t * s))
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : T35Space X<VAR>x y : X<VAR>x_ne_y : x ≠ y<GOAL>∃ f ∈ Continuous, f x ≠ f y
<VAR>X : Type u<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : T35Space X<VAR>x y : X<VAR>x_ne_y : x ≠ y<VAR>f : X → ↑I<VAR>f_cont : Continuous f<VAR>f_zero : f x = 0<VAR>f_one : EqOn f 1 {y}<GOAL>∃ f ∈ Continuous, f x ≠ f y
<VAR>T : ℝ<VAR>x : AddCircle T<GOAL>(fourier 1) x = ↑x.toCircle
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ⊓ b = a / (a / b)⁺ᵐ
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : Module R M'<VAR>ι : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>e : Basis ι R M<VAR>inst✝ : IsEmpty ι<VAR>v : ι → M<GOAL>e.det v = (AlternatingMap.constOfIsEmpty R M ι 1) v
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.48026, u_1} C<VAR>inst✝² : Category.{?u.48030, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<VAR>e₁ : S₁.X₁ ≅ S₂.X₁<VAR>e₂ : S₁.X₂ ≅ S₂.X₂<VAR>e₃ : S₁.X₃ ≅ S₂.X₃<VAR>comm₁₂ : autoParam (e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom) _auto✝<VAR>comm₂₃ : autoParam (e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom) _auto✝<GOAL>e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.48026, u_1} C<VAR>inst✝² : Category.{?u.48030, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<VAR>e₁ : S₁.X₁ ≅ S₂.X₁<VAR>e₂ : S₁.X₂ ≅ S₂.X₂<VAR>e₃ : S₁.X₃ ≅ S₂.X₃<VAR>comm₁₂ : autoParam (e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom) _auto✝<VAR>comm₂₃ : autoParam (e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom) _auto✝<GOAL>e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝² : DecidableEq o<VAR>inst✝¹ : Zero α<VAR>inst✝ : Zero β<VAR>i✝ : m × o<VAR>j✝ : n × o<GOAL>blockDiagonal 0 i✝ j✝ = 0 i✝ j✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b = a ⊔ b ↔ Disjoint a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<VAR>h : a ∆ b = a ⊔ b<GOAL>Disjoint a b