ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕂 : Type u_1<VAR>inst✝⁵ : RCLike 𝕂<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>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<VAR>this : hf.localInverse hf' hn (f a) = a<GOAL>HasFDerivAt (↑(toPartialHomeomorph f hf hf' hn)) (↑?m.32659) (↑(toPartialHomeomorph f hf hf' hn).symm (f a))
<VAR>𝕂 : Type u_1<VAR>inst✝⁵ : RCLike 𝕂<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>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<VAR>this : hf.localInverse hf' hn (f a) = a<GOAL>ContDiffAt 𝕂 n (↑(toPartialHomeomorph f hf hf' hn)) (↑(toPartialHomeomorph f hf hf' hn).symm (f a))
<VAR>𝕂 : Type u_1<VAR>inst✝⁵ : RCLike 𝕂<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>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕂] F<VAR>a : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕂 n f a<VAR>hf' : HasFDerivAt f (↑f') a<VAR>hn : 1 ≤ n<VAR>this : hf.localInverse hf' hn (f a) = a<GOAL>E ≃L[𝕂] F
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>inst✝ : Nonempty ι<VAR>a : ℝ≥0<VAR>g : ι → ℝ≥0<VAR>h : ℝ≥0<VAR>H : ∀ (i : ι), a ≤ g i * h<GOAL>a ≤ iInf g * h
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>inst✝ : Nonempty ι<VAR>a : ℝ≥0<VAR>g : ι → ℝ≥0<VAR>h : ℝ≥0<VAR>H : ∀ (i : ι), a ≤ g i * h<GOAL>a ≤ ⨅ i, g i * h
<VAR>α : Type u_1<VAR>b : Bool<VAR>a : Lists' α b<VAR>l : Lists' α true<GOAL>sizeOf ⟨b, a⟩ < sizeOf (a.cons' l)
<VAR>α : Type u_1<VAR>b : Bool<VAR>a : Lists' α b<VAR>l : Lists' α true<GOAL>0 < sizeOf l
<VAR>m n a b c d : ℕ<VAR>h₁ : c ≡ d [MOD n]<VAR>h₂ : a + c ≡ b + d [MOD n]<GOAL>a ≡ b [MOD n]
<VAR>m n a b c d : ℕ<VAR>h₁ : c ≡ d [MOD n]<VAR>h₂ : c + a ≡ d + b [MOD n]<GOAL>a ≡ b [MOD n]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : UniformSpace α<VAR>inst✝⁶ : Group α<VAR>inst✝⁵ : UniformGroup α<VAR>hom : Type u_3<VAR>inst✝⁴ : UniformSpace β<VAR>inst✝³ : Group β<VAR>inst✝² : UniformGroup β<VAR>inst✝¹ : FunLike hom α β<VAR>inst✝ : MonoidHomClass hom α β<VAR>f : hom<VAR>h : Continuous ⇑f<VAR>this : Tendsto (⇑f) (𝓝 1) (𝓝 (f 1))<GOAL>Tendsto (⇑f) (𝓝 1) (𝓝 1)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>b : Ordinal.{u}<VAR>a : Cardinal.{u}<VAR>H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = b<GOAL>a ≤ #ι
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>b : Ordinal.{u}<VAR>a : Cardinal.{u}<VAR>H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = b<VAR>r : ι → ι → Prop<VAR>hr : IsWellOrder ι r<VAR>hι' : (#ι).ord = type r<GOAL>a ≤ #ι
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>b : Ordinal.{u}<VAR>a : Cardinal.{u}<VAR>H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>r : ι → ι → Prop<VAR>hr : IsWellOrder ι r<VAR>hf : (type r).blsub (bfamilyOfFamily' r f) = b<VAR>hι' : (#ι).ord = type r<GOAL>a ≤ #ι
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>inst✝ : S.HasRightHomology<GOAL>h.rightHomologyIso.hom ≫ h.ι = S.rightHomologyι ≫ h.opcyclesIso.hom
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : r < 0<GOAL>Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I : Box ι<GOAL>volume.toBoxAdditive I = ∏ i : ι, (I.upper i - I.lower i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>h : a ∈ s<GOAL>s \ t.erase a = insert a (s \ t)
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>(∡ p₂ p₃ p₁).sign = (∡ p₁ p₂ p₃).sign
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>x y : R<VAR>r : ℝ<VAR>inst✝ : NonUnitalRing R<VAR>p : RingSeminorm R<GOAL>p ≠ 0 ↔ ∃ x, p x ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : Fintype β<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>↑s • Set.univ = Set.univ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : Multiset (Tropical R)<GOAL>untrop s.sum = (map untrop s).inf
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<GOAL>untrop (sum 0) = (map untrop 0).inf
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : Tropical R<VAR>x : Multiset (Tropical R)<VAR>IH : untrop x.sum = (map untrop x).inf<GOAL>untrop (s ::ₘ x).sum = (map untrop (s ::ₘ x)).inf
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a < b<GOAL>Ioc a b \ Ioo a b = {b}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>i j : ↥R⁰<GOAL>Submodule.span (R_hat R K) {↑↑i * ↑↑j} ≤ Submodule.span (R_hat R K) {↑↑i} ⊓ Submodule.span (R_hat R K) {↑↑j}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>i j : ↥R⁰<GOAL>(∃ a, a • ↑↑i = ↑↑i * ↑↑j) ∧ ∃ a, a • ↑↑j = ↑↑i * ↑↑j
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r : ↥R⁰<GOAL>∃ j, a • Submodule.span (R_hat R K) {↑↑j} ≤ Submodule.span (R_hat R K) {↑↑r}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<GOAL>∃ j, a • Submodule.span (R_hat R K) {↑↑j} ≤ Submodule.span (R_hat R K) {↑↑r}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<GOAL>a • Submodule.span (R_hat R K) {↑↑(r * b)} ≤ Submodule.span (R_hat R K) {↑↑r}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<VAR>m : FiniteAdeleRing R K<VAR>hm : m ∈ ↑(Submodule.span (R_hat R K) {↑↑(r * b)})<GOAL>(DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m ∈ Submodule.span (R_hat R K) {↑↑r}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<VAR>m : FiniteAdeleRing R K<VAR>hm : m ∈ Submodule.span (R_hat R K) {↑(↑r * ↑b)}<GOAL>(DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m ∈ Submodule.span (R_hat R K) {↑↑r}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<VAR>m : FiniteAdeleRing R K<VAR>hm : ∃ a, a • ↑(↑r * ↑b) = m<GOAL>∃ a_1, a_1 • ↑↑r = (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<VAR>n : R_hat R K<GOAL>∃ a_1, a_1 • ↑↑r = (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) (n • ↑(↑r * ↑b))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<VAR>n : R_hat R K<GOAL>∃ a_1, a_1 • ↑↑r = n • (a * ↑(↑r * ↑b))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<VAR>n : R_hat R K<GOAL>(n * c) • ↑↑r = n • (a * ↑(↑r * ↑b))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<VAR>n : R_hat R K<GOAL>(n * c) • ↑↑r = n • (a * (↑↑r * ↑↑b))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a : FiniteAdeleRing R K<VAR>r b : ↥R⁰<VAR>c : R_hat R K<VAR>h : a * ↑↑b = ↑c<VAR>n : R_hat R K<GOAL>Algebra.toRingHom (n * c) * ↑↑r = Algebra.toRingHom n * ↑c * ↑↑r
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : ↥R⁰<VAR>x : FiniteAdeleRing R K<VAR>hx : x ∈ ↑(Submodule.span (R_hat R K) {↑↑r}) * ↑(Submodule.span (R_hat R K) {↑↑r})<GOAL>x ∈ ↑(Submodule.span (R_hat R K) {↑↑r})
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : ↥R⁰<VAR>x : FiniteAdeleRing R K<VAR>hx : ∃ x_1 ∈ ↑(Submodule.span (R_hat R K) {↑↑r}), ∃ y ∈ ↑(Submodule.span (R_hat R K) {↑↑r}), x_1 * y = x<GOAL>x ∈ ↑(Submodule.span (R_hat R K) {↑↑r})
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : ↥R⁰<VAR>a : FiniteAdeleRing R K<VAR>ha : a ∈ ↑(Submodule.span (R_hat R K) {↑↑r})<VAR>b : FiniteAdeleRing R K<VAR>hb : b ∈ ↑(Submodule.span (R_hat R K) {↑↑r})<GOAL>a * b ∈ ↑(Submodule.span (R_hat R K) {↑↑r})
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : ↥R⁰<VAR>a b : FiniteAdeleRing R K<VAR>ha : ∃ a_1, a_1 • ↑↑r = a<VAR>hb : ∃ a, a • ↑↑r = b<GOAL>∃ a_1, a_1 • ↑↑r = a * b
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : ↥R⁰<VAR>m n : R_hat R K<GOAL>∃ a, a • ↑↑r = m • ↑↑r * n • ↑↑r
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : ↥R⁰<VAR>m n : R_hat R K<GOAL>(m * n * ↑↑r) • ↑↑r = m • ↑↑r * n • ↑↑r
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : ↥R⁰<VAR>m n : R_hat R K<GOAL>Algebra.toRingHom m * Algebra.toRingHom n * Algebra.toRingHom ↑↑r * ↑↑r = Algebra.toRingHom m * ↑↑r * (Algebra.toRingHom n * ↑↑r)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : ↥R⁰<VAR>m n : R_hat R K<GOAL>Algebra.toRingHom m * Algebra.toRingHom n * (Algebra.toRingHom ↑↑r * ↑↑r) = Algebra.toRingHom m * Algebra.toRingHom n * (↑↑r * ↑↑r)
<VAR>α : Type u_1<VAR>f : ℕ → ℝ≥0<VAR>k : ℕ<GOAL>(Summable fun i => f (i + k)) ↔ Summable f
<VAR>α : Type u_1<VAR>f : ℕ → ℝ≥0<VAR>k : ℕ<GOAL>(Summable fun a => ↑(f (a + k))) ↔ Summable fun a => ↑(f a)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>m n : ℕ<VAR>hn : n ≠ 0<GOAL>SMul.smul n (univ.piAntidiag m) = filter (fun f => ∀ (i : ι), n ∣ f i) (univ.piAntidiag (n * m))
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>m n : ℕ<VAR>hn : n ≠ 0<VAR>this : SMul.smul n (univ.piAntidiag m) = filter (fun f => ∀ i ∈ univ, n ∣ f i) (univ.piAntidiag (n * m))<GOAL>SMul.smul n (univ.piAntidiag m) = filter (fun f => ∀ (i : ι), n ∣ f i) (univ.piAntidiag (n * m))
<VAR>x y : ℂ<GOAL>cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cos x)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : FunLike F G G'<VAR>inst✝ : MonoidHomClass F G G'<VAR>f✝ : F<VAR>g₁ g₂ g₃ g : G<VAR>H₁ H₂ H₃ K₁ K₂ : Subgroup G<VAR>f : G →* G'<GOAL>map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : FunLike F G G'<VAR>inst✝ : MonoidHomClass F G G'<VAR>f✝ : F<VAR>g₁ g₂ g₃ g : G<VAR>H₁ H₂ H₃ K₁ K₂ : Subgroup G<VAR>f : G →* G'<GOAL>(∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧ ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : UniformSpace M<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group M<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : UniformGroup M<VAR>inst✝¹ : FunLike hom G M<VAR>inst✝ : MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : EquicontinuousAt (DFunLike.coe ∘ F) 1<GOAL>Equicontinuous (DFunLike.coe ∘ F)
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : UniformSpace M<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group M<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : UniformGroup M<VAR>inst✝¹ : FunLike hom G M<VAR>inst✝ : MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : EquicontinuousAt (DFunLike.coe ∘ F) 1<GOAL>Continuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : UniformSpace M<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group M<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : UniformGroup M<VAR>inst✝¹ : FunLike hom G M<VAR>inst✝ : MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1<GOAL>Continuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>hom : Type u_4<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : UniformSpace M<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group M<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : UniformGroup M<VAR>inst✝¹ : FunLike hom G M<VAR>inst✝ : MonoidHomClass hom G M<VAR>F : ι → hom<VAR>hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1<VAR>φ : G →* ι →ᵤ M := { toFun := swap (DFunLike.coe ∘ F), map_one' := ⋯, map_mul' := ⋯ }<GOAL>Continuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>sInf ∅ = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>k b : ℕ<VAR>x✝ : b ≥ 0<GOAL>b ≤ (fun a => a + k) b - k
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℕ → M<VAR>he : HasProd (fun k => f (2 * k)) m<VAR>ho : HasProd (fun k => f (2 * k + 1)) m'<GOAL>HasProd f (m * m')
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℕ → M<VAR>he : HasProd (fun k => f (2 * k)) m<VAR>ho : HasProd (fun k => f (2 * k + 1)) m'<VAR>this : Injective fun x => 2 * x<GOAL>HasProd f (m * m')
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℕ → M<VAR>he : HasProd (fun k => f (2 * k)) m<VAR>this : Injective fun x => 2 * x<VAR>ho : HasProd (fun x => f ↑x) m'<GOAL>HasProd f (m * m')
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℕ → M<VAR>he : HasProd (fun k => f (2 * k)) m<VAR>this : Injective fun x => 2 * x<VAR>ho : HasProd (fun x => f ↑x) m'<GOAL>IsCompl (Set.range fun x => 2 * x) (Set.range ((fun x => x + 1) ∘ fun x => 2 * x))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>h : S.RightHomologyData<GOAL>h.rightHomologyIso.hom ≫ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).inv = S.rightHomologyIso.hom
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X : T<VAR>f : Over X<VAR>X✝ Y✝ : Over f<VAR>κ : X✝ ⟶ Y✝<GOAL>κ.left.left ≫ Y✝.hom.left = X✝.hom.left
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X : T<VAR>f : Over X<VAR>X✝ Y✝ : Over f<VAR>κ : X✝ ⟶ Y✝<GOAL>κ.left.left ≫ Y✝.hom.left = (κ.left ≫ Y✝.hom).left
<VAR>α : Type u_1<VAR>inst✝² : Bornology α<VAR>s t : Set α<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Nonempty α<GOAL>IsOrderBornology α ↔ inst✝² = orderBornology
<VAR>α : Type u_1<VAR>inst✝² : Bornology α<VAR>s t : Set α<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Nonempty α<VAR>h : IsOrderBornology α<GOAL>inst✝² = orderBornology
<VAR>α : Type u_1<VAR>inst✝² : Bornology α<VAR>s✝ t : Set α<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Nonempty α<VAR>h : IsOrderBornology α<VAR>s : Set α<GOAL>s ∈ cobounded α ↔ s ∈ cobounded α
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>0 ≤ w D x
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>0 ≤ ((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>0 ≤ (∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>0 ≤ |D| ^ finrank ℝ E
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x c : ℂ<VAR>hf : HasDerivAt f f' x<VAR>hg : HasDerivAt g g' x<VAR>h0 : f x ∈ slitPlane<GOAL>HasDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>j : ι<GOAL>(Basis.ofEquivFun b.repr.toLinearEquiv) j = b j
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x - n • a) = f x - n • b
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>LiouvilleWith p (x * ↑n) ↔ LiouvilleWith p x
<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✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s✝ s₁ s₂ : Finset β<VAR>f✝ g : β → α<VAR>a✝ : α<VAR>s : Finset β<VAR>t : Finset γ<VAR>f : β × γ → α<VAR>a : α<GOAL>(s ×ˢ t).sup f ≤ a ↔ (s.sup fun i => t.sup fun i' => f (i, i')) ≤ a
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (Sigma σ)<GOAL>IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (Sigma σ)<GOAL>(∀ (i : ι), IsOpen s) ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝³ : CommSemiring S✝<VAR>inst✝² : Algebra R S✝<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>S : Type u_4<VAR>inst✝ : CommSemiring S<VAR>J : Ideal S<VAR>hJ : J.IsPrime<VAR>K : Ideal P<VAR>hK : K.IsPrime<VAR>f : R →+* S<VAR>hIJ : I = Ideal.comap f J<VAR>g : S →+* P<VAR>hJK : J = Ideal.comap g K<GOAL>I = Ideal.comap (g.comp f) K
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S✝ : Type u_2<VAR>inst✝³ : CommSemiring S✝<VAR>inst✝² : Algebra R S✝<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>S : Type u_4<VAR>inst✝ : CommSemiring S<VAR>J : Ideal S<VAR>hJ : J.IsPrime<VAR>K : Ideal P<VAR>hK : K.IsPrime<VAR>f : R →+* S<VAR>hIJ : I = Ideal.comap f J<VAR>g : S →+* P<VAR>hJK : J = Ideal.comap g K<VAR>r : R<GOAL>((localRingHom J K g hJK).comp (localRingHom I J f hIJ)) ((algebraMap R (Localization.AtPrime I)) r) = (algebraMap P (Localization.AtPrime K)) ((g.comp f) r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a \ b = ⊥ ↔ a ≤ b
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪o.rightAngleRotationAux₁ x, y⟫_ℝ = (o.areaForm x) y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪(InnerProductSpace.toDual ℝ E).symm (LinearMap.toContinuousLinearMap.symm.symm (o.areaForm x)), y⟫_ℝ = (o.areaForm x) y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(LinearMap.toContinuousLinearMap.symm.symm (o.areaForm x)) y = (o.areaForm x) y
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>min a b = a
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a = min a b