ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf✝ : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<VAR>x : α := fixedPoint f^[n] hf<VAR>hx : f^[n] x = x<VAR>this : ¬IsFixedPt f x<GOAL>↑K * dist x (f x) < dist x (f x)
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf✝ : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<VAR>x : α := fixedPoint f^[n] hf<VAR>hx : f^[n] x = x<VAR>this✝ : ¬IsFixedPt f x<VAR>this : 0 < dist x (f x)<GOAL>↑K * dist x (f x) < dist x (f x)
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>q : ℕ<VAR>x y : R<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(x + y) ^ q = x ^ q + y ^ q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>p✝ : PrimeSpectrum R<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>p : PrimeSpectrum R<GOAL>p ∈ support R A ↔ p ∈ PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>p✝ : PrimeSpectrum R<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>p : PrimeSpectrum R<GOAL>(∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (algebraMap R A) ≤ p.asIdeal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>p✝ : PrimeSpectrum R<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>p : PrimeSpectrum R<VAR>x✝ : ∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0<VAR>x : R<VAR>hx : x ∈ RingHom.ker (algebraMap R A)<VAR>m : A<VAR>hm : ∀ r ∉ p.asIdeal, ¬r • m = 0<VAR>hx' : x ∉ p.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>p✝ : PrimeSpectrum R<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>p : PrimeSpectrum R<VAR>H : RingHom.ker (algebraMap R A) ≤ p.asIdeal<VAR>r : R<VAR>hr : r ∉ p.asIdeal<VAR>e : r • 1 = 0<GOAL>False
<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>y : 𝕜<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>derivWithin f s x = derivWithin f t x
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>⊤ / a = if a = ⊤ then 0 else ⊤
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : NoMaxOrder β<VAR>u : α → β<VAR>h : Tendsto u atTop atTop<VAR>a : α<VAR>b : β<GOAL>∃ a' ≥ a, b < u a'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : NoMaxOrder β<VAR>u : α → β<VAR>h : Tendsto u atTop atTop<VAR>a : α<VAR>b b' : β<VAR>hb' : b < b'<GOAL>∃ a' ≥ a, b < u a'
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : NoMaxOrder β<VAR>u : α → β<VAR>h : Tendsto u atTop atTop<VAR>a : α<VAR>b b' : β<VAR>hb' : b < b'<VAR>a' : α<VAR>ha' : a' ≥ a<VAR>ha'' : b' ≤ u a'<GOAL>∃ a' ≥ a, b < u a'
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f : M →ₗ[R] M₂<VAR>x : M × M₂<GOAL>x ∈ range (inl R M M₂) ↔ x ∈ ker (snd R M M₂)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f : M →ₗ[R] M₂<VAR>x : M × M₂<GOAL>(∃ y, (inl R M M₂) y = x) ↔ (snd R M M₂) x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝² : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<VAR>a : α<GOAL>(∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, u x ∈ ball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε
<VAR>R : Type u_1<VAR>inst✝¹ : GroupWithZero R<VAR>inst✝ : StarMul R<VAR>U₁ U₂ : ↥(unitary R)<GOAL>↑(U₁ / U₂) = ↑U₁ / ↑U₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>x y : α<VAR>S U Z : Set α<VAR>h : IsGenericPoint x S<VAR>f : α → β<VAR>hf : Continuous f<GOAL>IsGenericPoint (f x) (closure (f '' S))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>x✝ : K<GOAL>x✝ ∈ A.valuation.valuationSubring ↔ x✝ ∈ A
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A : ValuationSubring K<VAR>x✝ : K<GOAL>x✝ ∈ A.valuation.valuationSubring ↔ A.valuation x✝ ≤ 1
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : List (Sigma β)<GOAL>lookup a s.toAList = dlookup a s
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<GOAL>Valued.v (↑K k) = v.valuation k
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>N M' : Matroid α<VAR>h : M ≤r M'<VAR>h' : M' ≤r M<GOAL>M = M'
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Linear R V<VAR>h : Homotopy f g<VAR>a : R<VAR>i j : ι<VAR>hij : ¬c.Rel j i<GOAL>a • h.hom i j = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Linear R V<VAR>h : Homotopy f g<VAR>a : R<VAR>i : ι<GOAL>a • f.f i = (C.dFrom i ≫ (fromNext i) fun i j => a • h.hom i j) + ((toPrev i) fun i j => a • h.hom i j) ≫ D.dTo i + a • g.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Linear R V<VAR>h : Homotopy f g<VAR>a : R<VAR>i : ι<GOAL>a • ((dNext i) h.hom + (prevD i) h.hom + g.f i) = (C.dFrom i ≫ (fromNext i) fun i j => a • h.hom i j) + ((toPrev i) fun i j => a • h.hom i j) ≫ D.dTo i + a • g.f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Linear R V<VAR>h : Homotopy f g<VAR>a : R<VAR>i : ι<GOAL>a • (C.dFrom i ≫ h.hom (c.next i) i + h.hom i (c.prev i) ≫ D.dTo i + g.f i) = C.dFrom i ≫ (a • h.hom (c.next i) i) + (a • h.hom i (c.prev i)) ≫ D.dTo i + a • g.f i
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>dual A K I ≠ 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>b : B<VAR>hb : b ∈ B⁰<VAR>hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)<GOAL>dual A K I ≠ 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>b : B<VAR>hb : b ∈ B⁰<VAR>hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)<GOAL>(algebraMap B L) b ∈ dual A K I
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>b : B<VAR>hb : b ∈ B⁰<VAR>hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)<GOAL>∀ a ∈ I, ((traceForm K L) ((algebraMap B L) b)) a ∈ (algebraMap A K).range
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>b : B<VAR>hb : b ∈ B⁰<VAR>hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)<VAR>a : L<VAR>ha : a ∈ I<GOAL>((traceForm K L) ((algebraMap B L) b)) a ∈ (algebraMap A K).range
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>b : B<VAR>hb : b ∈ B⁰<VAR>hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)<VAR>a : L<VAR>ha : a ∈ I<GOAL>IsIntegral A (((traceForm K L) ((algebraMap B L) b)) a)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>b : B<VAR>hb : b ∈ B⁰<VAR>hb' : ∀ b_1 ∈ ↑I, IsInteger B (b • b_1)<VAR>a : L<VAR>ha : a ∈ I<GOAL>IsIntegral A (((lmul K L).toLinearMap ((algebraMap B L) b)) a)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<GOAL>ContDiffOn ℝ ⊤ (stereoToFun v) {x | ((innerSL ℝ) v) x ≠ 1}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<GOAL>ContDiffOn ℝ ⊤ (fun x => 2 / (1 - ((innerSL ℝ) v) x)) {x | ((innerSL ℝ) v) x ≠ 1}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<GOAL>ContDiffOn ℝ ⊤ (fun x => 1 - ((innerSL ℝ) v) x) {x | ((innerSL ℝ) v) x ≠ 1}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<GOAL>∀ x ∈ {x | ((innerSL ℝ) v) x ≠ 1}, 1 - ((innerSL ℝ) v) x ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>m n : ℕ<GOAL>|↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>m : ℕ<GOAL>|↑m / ↑0 - ↑(round (↑m / ↑0))| = ↑(min (m % 0) (0 - m % 0)) / ↑0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>m n : ℕ<VAR>hn : n > 0<GOAL>|↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>m n : ℕ<VAR>hn : n > 0<VAR>hn' : 0 < ↑n<GOAL>|↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>x : F<VAR>hx : ¬x = 0<GOAL>IsSolvable (X ^ n - C x).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>x : F<VAR>hx : ¬x = 0<GOAL>Splits (algebraMap F (X ^ n - C x).SplittingField) (X ^ n - 1)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>x : F<VAR>hx : ¬x = 0<GOAL>IsSolvable (X ^ n - 1).Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>n : ℕ<VAR>x : F<VAR>hx : ¬x = 0<GOAL>IsSolvable (Polynomial.map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : α → β<VAR>s t : Set α<VAR>inst✝ : BooleanAlgebra α<VAR>S : Set α<GOAL>compl '' (compl '' S) = S
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>hfi : Integrable f volume<GOAL>HasSum (fun n => ∫ (x : ℝ) in 0 ..1, f (x + ↑n)) (∫ (x : ℝ), f x)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : Independent p<GOAL>Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0<GOAL>Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0<GOAL>LinearMap.ker ((lsum ℕ) fun i => (p i).subtype) = ⊥
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0<GOAL>∀ (m : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) m = 0 → m = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0<VAR>m : Π₀ (i : ι), ↥(p i)<VAR>hm : ((lsum ℕ) fun i => (p i).subtype) m = 0<VAR>i : ι<GOAL>m i = 0 i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0<VAR>m : Π₀ (i : ι), ↥(p i)<VAR>hm : ((lsum ℕ) fun i => (p i).subtype) m = 0<VAR>i : ι<GOAL>-m i = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → Submodule R N<VAR>h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0<VAR>m : Π₀ (i : ι), ↥(p i)<VAR>hm : ((lsum ℕ) fun i => (p i).subtype) m = 0<VAR>i : ι<GOAL>((lsum ℕ) fun i => (p i).subtype) (erase i m) = ↑(-m i)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.266427, u_1} C<VAR>inst✝⁵ : Category.{?u.266431, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝² : HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>inst✝¹ : H.Additive<VAR>inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>(H.map ((↑(fst φ)).v n m ⋯) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯ + H.map ((snd φ).v n n ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫ ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯ ≫ H.map ((inl φ).v m n ⋯) + (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫ H.map ((inr φ).f n)) = 𝟙 (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).X n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.266427, u_1} C<VAR>inst✝⁵ : Category.{?u.266431, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝² : HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>inst✝¹ : H.Additive<VAR>inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>H.map ((↑(fst φ)).v n m ⋯ ≫ (inl φ).v m n ⋯ + (snd φ).v n n ⋯ ≫ (inr φ).f n) = 𝟙 (H.obj ((mappingCone φ).X n))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.266427, u_1} C<VAR>inst✝⁵ : Category.{?u.266431, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝² : HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>inst✝¹ : H.Additive<VAR>inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>H.map ((↑(fst φ)).v n m ⋯ ≫ (inl φ).v m n ⋯ + (snd φ).v n n ⋯ ≫ (inr φ).f n) = H.map (𝟙 ((mappingCone φ).X n))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.266427, u_1} C<VAR>inst✝⁵ : Category.{?u.266431, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝² : HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>inst✝¹ : H.Additive<VAR>inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>(↑(fst φ)).v n m ⋯ ≫ (inl φ).v m n ⋯ + (snd φ).v n n ⋯ ≫ (inr φ).f n = 𝟙 ((mappingCone φ).X n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.266427, u_1} C<VAR>inst✝⁵ : Category.{?u.266431, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝² : HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>inst✝¹ : H.Additive<VAR>inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯ ≫ H.map ((inl φ).v m n ⋯) + (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫ H.map ((inr φ).f n)) ≫ (H.map ((↑(fst φ)).v n m ⋯) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯ + H.map ((snd φ).v n n ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) = 𝟙 ((mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{?u.266427, u_1} C<VAR>inst✝⁵ : Category.{?u.266431, u_2} D<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝² : HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>inst✝¹ : H.Additive<VAR>inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯ ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯ + (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫ H.map 0 ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯ + ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯ ≫ H.map 0 ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n + (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) = 𝟙 ((mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<GOAL>Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>this : Monotone fun n => ∫⁻ (x : α), f n x ∂μ<GOAL>Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))