ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>w : V<GOAL>𝓕 (fun v => cexp (-b * ↑‖v‖ ^ 2)) w = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑‖w‖ ^ 2 / b)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<GOAL>IsSheafFor P (Presieve.ofArrows X π) ↔ Nonempty (IsLimit (Fork.ofι (forkMap P X π) ⋯))
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<GOAL>(∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i) ↔ ∀ (y : FirstObj P X), firstMap P X π y = secondMap P X π y → ∃! x, forkMap P X π x = y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<GOAL>(∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i) ↔ ∀ (a : (j : I) → P.obj (op (X j))), firstMap P X π ((Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a) = secondMap P X π ((Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a) → ∃! x, forkMap P X π x = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<GOAL>(∀ (x : (i : I) → P.obj (op (X i))), Arrows.Compatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i) ↔ ∀ (a : (j : I) → P.obj (op (X j))), Arrows.Compatible P π a → ∃! x, forkMap P X π x = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<GOAL>∀ (a : (i : I) → P.obj (op (X i))), Arrows.Compatible P π a → ((∃! t, ∀ (i : I), P.map (π i).op t = a i) ↔ ∃! x, forkMap P X π x = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm a)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>x : (i : I) → P.obj (op (X i))<VAR>b✝ : Arrows.Compatible P π x<GOAL>(∃! t, ∀ (i : I), P.map (π i).op t = x i) ↔ ∃! x_1, forkMap P X π x_1 = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>x : (i : I) → P.obj (op (X i))<VAR>b✝ : Arrows.Compatible P π x<GOAL>∀ (a : P.obj (op B)), (∀ (i : I), P.map (π i).op a = x i) ↔ forkMap P X π a = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>x : (i : I) → P.obj (op (X i))<VAR>b✝ : Arrows.Compatible P π x<VAR>t : P.obj (op B)<GOAL>(∀ (i : I), P.map (π i).op t = x i) ↔ forkMap P X π t = (Types.productIso fun i => P.obj (op (X i))).toEquiv.symm x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type (max v u)<VAR>X✝¹ : C<VAR>R✝ : Presieve X✝¹<VAR>S✝ : Sieve X✝¹<VAR>inst✝¹ : R✝.hasPullbacks<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>R : Presieve X✝<VAR>S : Sieve X✝<VAR>B : C<VAR>I : Type<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (Presieve.ofArrows X π).hasPullbacks<VAR>x : (i : I) → P.obj (op (X i))<VAR>b✝ : Arrows.Compatible P π x<VAR>t : P.obj (op B)<GOAL>(∀ (i : I), P.map (π i).op t = x i) ↔ (Types.productIso fun i => P.obj (op (X i))).toEquiv (forkMap P X π t) = x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<GOAL>IsCompl Weight.ker (span K {coroot α})
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x1 x2 y : ℕ × K<VAR>H : R K p x1 x2<VAR>n : ℕ<VAR>x : K<GOAL>R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2) ((n + 1, (frobenius K p) x).1 + y.1, (⇑(frobenius K p))^[y.1] (n + 1, (frobenius K p) x).2 + (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x1 x2 y : ℕ × K<VAR>H : R K p x1 x2<VAR>n : ℕ<VAR>x : K<GOAL>R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2) ((n + y.1).succ, (frobenius K p) ((⇑(frobenius K p))^[y.1] x + (⇑(frobenius K p))^[n] y.2))
<VAR>θ : Angle<GOAL>θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁶ : AddCommMonoid L<VAR>inst✝⁵ : TopologicalSpace L<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : TopologicalSpace N<VAR>v : VectorMeasure α M<VAR>w✝ : VectorMeasure α N<VAR>inst✝ : ContinuousAdd M<VAR>v₁ v₂ : VectorMeasure α M<VAR>w : VectorMeasure α N<VAR>hv₁ : v₁ ≪ᵥ w<VAR>hv₂ : v₂ ≪ᵥ w<VAR>s : Set α<VAR>hs : ↑w s = 0<GOAL>↑(v₁ + v₂) s = 0
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>t.prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>(prod 0).coeff 0 = (Multiset.map (fun f => f.coeff 0) 0).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t✝ : Multiset R[X]<VAR>a : R[X]<VAR>t : Multiset R[X]<VAR>ht : t.prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) t).prod<GOAL>(a ::ₘ t).prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) (a ::ₘ t)).prod
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<VAR>k x : ℕ<VAR>kpos : 0 < k<GOAL>(f.ppow k) x = f x ^ k
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<VAR>k x : ℕ<VAR>kpos : 0 < k<GOAL>{ toFun := fun x => f x ^ k, map_zero' := ⋯ } x = f x ^ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (i : β), AEMeasurable (f i) μ<GOAL>∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (i : β), AEMeasurable (f i) μ<GOAL>∫⁻ (a : α), ⨆ s, ∑ i ∈ s, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (i : β), AEMeasurable (f i) μ<GOAL>⨆ b, ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ = ⨆ s, ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (i : β), AEMeasurable (f i) μ<GOAL>∀ (b : Finset β), AEMeasurable (fun a => ∑ i ∈ b, f i a) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (i : β), AEMeasurable (f i) μ<GOAL>Directed (fun x x_1 => x ≤ x_1) fun s a => ∑ i ∈ s, f i a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<VAR>hn : 2 < n.natAbs<VAR>h : ↑n ≠ 0<GOAL>0 < (W.preΨ n).natDegree
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<VAR>r : R<GOAL>rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>r : R<GOAL>rootMultiplicity r ((expand R (p ^ n)) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<VAR>r : R<VAR>h0 : f ≠ 0<GOAL>rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<VAR>r : R<VAR>h0 : f ≠ 0<VAR>g : R[X]<VAR>hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g<VAR>ndvd : ¬X - C (r ^ p ^ n) ∣ g<GOAL>rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<VAR>r : R<VAR>h0 : f ≠ 0<VAR>g : R[X]<VAR>hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g<VAR>ndvd : ¬((expand R (p ^ n)) g).IsRoot r<GOAL>rootMultiplicity r ((expand R (p ^ n)) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>h : c • x ∈ s<GOAL>egauge 𝕜 s x ≤ (↑‖c‖₊)⁻¹
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>h : 0 • x ∈ s<GOAL>egauge 𝕜 s x ≤ (↑‖0‖₊)⁻¹
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>h : c • x ∈ s<VAR>hc : c ≠ 0<GOAL>egauge 𝕜 s x ≤ (↑‖c‖₊)⁻¹
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ χ' : MulChar R R'<VAR>h : ∀ (a : Rˣ), χ ↑a = χ' ↑a<GOAL>χ = χ'
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝ : CommMonoidWithZero R'<VAR>χ χ' : MulChar R R'<VAR>h : ∀ (a : Rˣ), χ ↑a = χ' ↑a<GOAL>∀ (a : R), χ a = χ' a
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜<GOAL>logDeriv (fun x => x⁻¹) x = -1 / x
<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 : α → ℝ≥0∞<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>(fun x => ENNReal.ofReal (f x).toReal) =ᶠ[ae μ] f
<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 : α → ℝ≥0∞<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>∀ (a : α), f a < ⊤ → ENNReal.ofReal (f a).toReal = f 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 : α → ℝ≥0∞<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>x : α<VAR>hx : f x < ⊤<GOAL>ENNReal.ofReal (f x).toReal = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0∞<VAR>hf : ∑' (i : ℕ), f i ≠ ⊤<GOAL>Tendsto (fun i => ∑' (k : ℕ), f (k + i)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>hf : ∑' (i : ℕ), (fun i => ↑(f i)) i ≠ ⊤<GOAL>Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>hf : Summable f<GOAL>Tendsto (fun i => ∑' (k : ℕ), (fun i => ↑(f i)) (k + i)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>hf : Summable f<GOAL>Tendsto (fun i => ↑(∑' (a : ℕ), f (a + i))) atTop (𝓝 ↑0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s✝ s : Set α<GOAL>IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
<VAR>N✝ : ℕ<VAR>N : ℕ+<GOAL>Gamma ↑N ≤ Gamma ↑N
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>A B : C<VAR>h : A ⟶ ⊥.obj.left<GOAL>h ≫ ⊥.arrow = 0
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<GOAL>LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ fun (p : ↑(range C)) => ↑p
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<GOAL>LinearIndependent ℤ (Subtype.val ∘ (equiv_range C).toFun) ↔ LinearIndependent ℤ fun (p : ↑(range C)) => ↑p
<VAR>α : Type u<VAR>β : Type v<VAR>f fa g : α → α<VAR>x y : α<VAR>fb : β → β<VAR>m n k : ℕ<VAR>e : Perm α<VAR>x✝ : α<GOAL>x✝ ∈ fixedPoints id ↔ x✝ ∈ Set.univ
<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>θ : Real.Angle<GOAL>LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1
<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>θ : Real.Angle<VAR>this : Nontrivial V<GOAL>LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1
<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>θ : Real.Angle<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1
<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>θ : Real.Angle<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>LinearMap.det ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos]) = 1
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<GOAL>¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝² : PseudoEMetricSpace α✝<VAR>δ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>E : Set α<VAR>hE : IsClosed E<VAR>hδ : 0 ≤ δ<GOAL>cthickening δ E = ⋃ x ∈ E, closedBall x δ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i j : Fin (n + 1)<VAR>H : i ≤ j<GOAL>X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ i.castSucc).op = X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ j.succ).op
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s s₁ s₂ : Finset ι<VAR>t t₁ t₂ : (i : ι) → Finset (α i)<VAR>f : (i : ι) × α i → β<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : OrderBot β<GOAL>(s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : Type u_3<VAR>s s₁ s₂ : Finset ι<VAR>t t₁ t₂ : (i : ι) → Finset (α i)<VAR>f : (i : ι) × α i → β<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : OrderBot β<GOAL>(∀ (a : ι) (b : α a), a ∈ s → b ∈ t a → f ⟨a, b⟩ ≤ s.sup fun i => (t i).sup fun b => f ⟨i, b⟩) ∧ ∀ b ∈ s, ∀ b_1 ∈ t b, f ⟨b, b_1⟩ ≤ (s.sigma t).sup f
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>b ≤ 1 * a ↔ b ≤ a
<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>c c₁ c₂ p₁ p₂ : P<GOAL>perpBisector p₁ p₂ = ⊤ ↔ p₁ = p₂
<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>c c₁ c₂ p₁ p₂ : P<VAR>h : perpBisector p₁ p₂ = ⊤<GOAL>p₁ = p₂
<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>c c₁ c₂ p₁ p₂ : P<VAR>h : perpBisector p₁ p₂ = ⊤<GOAL>p₁ ∈ ⊤
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hI : autoParam (I ⊆ M.E) _auto✝<GOAL>M✶.Indep I ↔ ∃ B, M.Base B ∧ Disjoint I B
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝¹ : Category.{v₂, v₁} I<VAR>F : I ⥤ C<VAR>inst✝ : HasColimit F<VAR>i : I<GOAL>(coyonedaOpColimitIsoLimitCoyoneda F).inv ≫ coyoneda.map (colimit.ι F i).op = limit.π (F.op ⋙ coyoneda) (op i)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q✝ : R[X]<VAR>x : R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>p q : R[X]<VAR>H : q.IsRoot a<GOAL>(p * q).IsRoot a
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>hf : ∀ (x : α), f x ∈ 𝓝 x<GOAL>∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>hf : ∀ (x : α), f x ∈ 𝓝 x<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)<GOAL>∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>hf : ∀ (x : α), f x ∈ 𝓝 x<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)<GOAL>⋃ x ∈ s, interior (f x) = univ
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>f : α → Set α<VAR>hf : ∀ (x : α), f x ∈ 𝓝 x<VAR>s : Set α<VAR>hsc : s.Countable<VAR>hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)<GOAL>∀ (x : α), ∃ i, x ∈ interior (f i)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(X ^ n).roots = n • {0}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>k a : ℕ<VAR>h : a ≥ k<GOAL>a ≤ (fun a => a - k) a + k
<VAR>α : Type u_1<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : OrderBot α<VAR>inst✝¹ : Finite α<VAR>s : { s // SupIrred s }<VAR>inst✝ : Fintype ↥↑s<GOAL>supIrredLowerSet.symm s = (↑↑s).toFinset.sup id
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.227632}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : s ⊆ range f<GOAL>lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.227632}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : f '' (f ⁻¹' s) = s<GOAL>lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)
<VAR>α✝ β✝ : Type u<VAR>c : Cardinal.{?u.227632}<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>h : f '' (f ⁻¹' s) = s<GOAL>lift.{u, v} #↑(f '' (f ⁻¹' s)) ≤ lift.{v, u} #↑(f ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>g : P →ₐ[R] P'<VAR>I : Submodule R P<VAR>a : R<VAR>a_nonzero : a ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (a • b)<VAR>b : P'<VAR>hb : b ∈ Submodule.map g.toLinearMap I<GOAL>IsInteger R (a • b)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>g : P →ₐ[R] P'<VAR>I : Submodule R P<VAR>a : R<VAR>a_nonzero : a ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (a • b)<VAR>b : P'<VAR>hb : b ∈ Submodule.map g.toLinearMap I<VAR>b' : P<VAR>b'_mem : b' ∈ I<VAR>hb' : g.toLinearMap b' = b<GOAL>IsInteger R (a • b)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>g : P →ₐ[R] P'<VAR>I : Submodule R P<VAR>a : R<VAR>a_nonzero : a ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (a • b)<VAR>b : P'<VAR>hb : b ∈ Submodule.map g.toLinearMap I<VAR>b' : P<VAR>b'_mem : b' ∈ I<VAR>hb' : g b' = b<GOAL>IsInteger R (a • b)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>g : P →ₐ[R] P'<VAR>I : Submodule R P<VAR>a : R<VAR>a_nonzero : a ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (a • b)<VAR>b : P'<VAR>hb : b ∈ Submodule.map g.toLinearMap I<VAR>b' : P<VAR>b'_mem : b' ∈ I<VAR>hb' : g b' = b<VAR>x : R<VAR>hx : (algebraMap R P) x = a • b'<GOAL>IsInteger R (a • b)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>g : P →ₐ[R] P'<VAR>I : Submodule R P<VAR>a : R<VAR>a_nonzero : a ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (a • b)<VAR>b : P'<VAR>hb : b ∈ Submodule.map g.toLinearMap I<VAR>b' : P<VAR>b'_mem : b' ∈ I<VAR>hb' : g b' = b<VAR>x : R<VAR>hx : (algebraMap R P) x = a • b'<GOAL>(algebraMap R P') x = a • b