ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<VAR>a : S<VAR>b : R<VAR>hb : b ≠ 0<VAR>dim_pos : 0 < Fintype.card ι<VAR>ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))<VAR>hε : 0 < ε<VAR>ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)<VAR>μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm<VAR>hμ : μ = distinctElems bS adm<VAR>s : ι →₀ R := bS.repr a<VAR>s_eq : ∀ (i : ι), s i = (bS.repr a) i<VAR>qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b<VAR>rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b<VAR>r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b<VAR>μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i<VAR>μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i : ι, qs j i • bS i + ∑ i : ι, rs j i • bS i<VAR>j k : Fin (adm.card ε ^ Fintype.card ι).succ<VAR>j_ne_k : j ≠ k<VAR>hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε<VAR>hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε<VAR>q : S := ∑ i : ι, (qs k i - qs j i) • bS i<VAR>r : R := μ k - μ j<VAR>r_eq : r = μ k - μ j<VAR>this : r • a - b • q = ∑ x : ι, (rs k x • bS x - rs j x • bS x)<GOAL>↑(normBound abv bS) * (abv b • ε) ^ Fintype.card ι ≤ ↑(abv b ^ Fintype.card ι)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsCompact s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty<GOAL>(s ∩ ⋂ i, t i).Nonempty
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsCompact s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<GOAL>∃ u, s ∩ ⋂ i ∈ u, t i = ∅
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x : S<VAR>f : R →+* Polynomial S<VAR>g : σ → Polynomial S<VAR>p : MvPolynomial σ R<GOAL>Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x : S<VAR>f : R →+* Polynomial S<VAR>g : σ → Polynomial S<VAR>p : MvPolynomial σ R<GOAL>∀ (a : R), Polynomial.eval x (eval₂ f g (C a)) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) (C a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x : S<VAR>f : R →+* Polynomial S<VAR>g : σ → Polynomial S<VAR>p : MvPolynomial σ R<GOAL>∀ (p q : MvPolynomial σ R), Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) p → Polynomial.eval x (eval₂ f g q) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) q → Polynomial.eval x (eval₂ f g (p + q)) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) (p + q)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x : S<VAR>f : R →+* Polynomial S<VAR>g : σ → Polynomial S<VAR>p : MvPolynomial σ R<GOAL>∀ (p : MvPolynomial σ R) (n : σ), Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) p → Polynomial.eval x (eval₂ f g (p * X n)) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s => Polynomial.eval x (g s)) (p * X n)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) = pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.fst (𝒰.map i ≫ f) g
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>S : Subalgebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F E<GOAL>⊥ = ⊤ ↔ Module.rank F E = 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : StrongRankCondition F<VAR>inst✝³ : Ring E<VAR>inst✝² : Algebra F E<VAR>S : Subalgebra F E<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : Module.Free F E<VAR>this : Module.Free F ↥⊤<GOAL>⊥ = ⊤ ↔ Module.rank F E = 1
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>HasDerivAt (fun y => (fourier (-n)) ↑y) (-2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x) x
<VAR>ι : Type u<VAR>γ✝ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → AddZeroClass (β i)<VAR>γ : Type w<VAR>inst✝ : AddZeroClass γ<VAR>f g : (Π₀ (i : ι), β i) →+ γ<VAR>H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)<GOAL>f = g
<VAR>ι : Type u<VAR>γ✝ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → AddZeroClass (β i)<VAR>γ : Type w<VAR>inst✝ : AddZeroClass γ<VAR>f✝ g : (Π₀ (i : ι), β i) →+ γ<VAR>H : ∀ (i : ι) (y : β i), f✝ (single i y) = g (single i y)<VAR>f : Π₀ (i : ι), β i<VAR>hf : f ∈ ⋃ i, Set.range (single i)<GOAL>f✝ f = g f
<VAR>ι : Type u<VAR>γ✝ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → AddZeroClass (β i)<VAR>γ : Type w<VAR>inst✝ : AddZeroClass γ<VAR>f✝ g : (Π₀ (i : ι), β i) →+ γ<VAR>H : ∀ (i : ι) (y : β i), f✝ (single i y) = g (single i y)<VAR>f : Π₀ (i : ι), β i<VAR>hf : ∃ i y, single i y = f<GOAL>f✝ f = g f
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : X ⟶ (⨁ f) ⊗ Y<VAR>w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y<GOAL>g = h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : X ⟶ (⨁ f) ⊗ Y<VAR>w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y<GOAL>g ≫ (rightDistributor f Y).hom = h ≫ (rightDistributor f Y).hom
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : X ⟶ (⨁ f) ⊗ Y<VAR>w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y<VAR>j✝ : J<GOAL>(g ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝ = (h ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : X ⟶ (⨁ f) ⊗ Y<VAR>w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y<VAR>j✝ : J<GOAL>g ≫ biproduct.π f j✝ ▷ Y = h ≫ biproduct.π f j✝ ▷ Y
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q n a : ℕ<VAR>ha : n = a + q<GOAL>hσ' q n (n + 1) ⋯ = (-1) ^ a • X.σ ⟨a, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝¹ : Fintype α<VAR>a : α<VAR>inst✝ : Fintype ↑{x | x ≠ a}<VAR>this : DecidableEq α<GOAL>Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Module A M<VAR>x y : PrimeSpectrum R<VAR>e : x ⤳ y<VAR>H : x ∈ support R M<GOAL>y ∈ support R M
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Module A M<VAR>x y : PrimeSpectrum R<VAR>e : x ⤳ y<VAR>H : ∃ m, (Submodule.span R {m}).annihilator ≤ x.asIdeal<GOAL>∃ m, (Submodule.span R {m}).annihilator ≤ y.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Module A M<VAR>x y : PrimeSpectrum R<VAR>e : x ⤳ y<VAR>m : M<VAR>hm : (Submodule.span R {m}).annihilator ≤ x.asIdeal<GOAL>∃ m, (Submodule.span R {m}).annihilator ≤ y.asIdeal
<VAR>α : Type u_1<VAR>m n : Nat<VAR>x : α<VAR>xs : List α<VAR>hl : (x :: xs).Nodup<VAR>h : m ≤ n<GOAL>(take m (x :: xs)).Disjoint (drop n (x :: xs))
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>hl : (x :: xs).Nodup<VAR>n✝ : Nat<VAR>h : n✝ + 1 ≤ 0<GOAL>¬x ∈ x :: xs ∧ (take n✝ xs).Disjoint (x :: xs)
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>hl : (x :: xs).Nodup<VAR>n✝¹ n✝ : Nat<VAR>h : n✝¹ + 1 ≤ n✝ + 1<GOAL>¬x ∈ drop n✝ xs ∧ (take n✝¹ xs).Disjoint (drop n✝ xs)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C₁<VAR>inst✝⁶ : Category.{u_8, u_2} C₂<VAR>inst✝⁵ : Category.{u_5, u_3} D₁<VAR>inst✝⁴ : Category.{u_7, u_4} D₂<VAR>G : C₁ ⥤ C₂<VAR>F : C₂ ⥤ C₁<VAR>adj : G ⊣ F<VAR>L₁ : C₁ ⥤ D₁<VAR>W₁ : MorphismProperty C₁<VAR>inst✝³ : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>W₂ : MorphismProperty C₂<VAR>inst✝² : L₂.IsLocalization W₂<VAR>G' : D₁ ⥤ D₂<VAR>F' : D₂ ⥤ D₁<VAR>inst✝¹ : CatCommSq G L₁ L₂ G'<VAR>inst✝ : CatCommSq F L₂ L₁ F'<VAR>X₁ : C₁<VAR>this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso' := CatCommSq.iso'.symm }<GOAL>(ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) = L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z1 z2 : ℚ_[p]<VAR>h : ‖z1 + z2‖ < ‖z2‖<VAR>hne : ¬‖z1‖ = ‖z2‖<GOAL>‖z1 + z2‖ ≥ ‖z2‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z1 z2 : ℚ_[p]<VAR>h : ‖z1 + z2‖ < ‖z2‖<VAR>hne : ¬‖z1‖ = ‖z2‖<GOAL>max ‖z1‖ ‖z2‖ ≥ ‖z2‖
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<VAR>hcont : ContinuousOn f (Ici a)<GOAL>∫ (x : ℝ) in Ioi a, f' x = m - f a
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<VAR>hcont : ContinuousOn f (Ici a)<GOAL>Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<VAR>hcont : ContinuousOn f (Ici a)<GOAL>(fun x => f x - f a) =ᶠ[atTop] fun i => ∫ (x : ℝ) in a..id i, f' x
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<VAR>hcont : ContinuousOn f (Ici a)<VAR>x : ℝ<VAR>hx : x ∈ Ioi a<GOAL>f x - f a = ∫ (x : ℝ) in a..id x, f' x
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<VAR>hcont : ContinuousOn f (Ici a)<VAR>x : ℝ<VAR>hx : x ∈ Ioi a<VAR>h'x : a ≤ id x<GOAL>f x - f a = ∫ (x : ℝ) in a..id x, f' x
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<VAR>hcont : ContinuousOn f (Ici a)<VAR>x : ℝ<VAR>hx : x ∈ Ioi a<VAR>h'x : a ≤ id x<GOAL>∫ (x : ℝ) in a..id x, f' x = f x - f a
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<VAR>hcont : ContinuousOn f (Ici a)<VAR>x : ℝ<VAR>hx : x ∈ Ioi a<VAR>h'x : a ≤ id x<GOAL>IntervalIntegrable f' volume a (id x)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt f (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Ioi a) volume<VAR>hf : Tendsto f atTop (𝓝 m)<VAR>hcont : ContinuousOn f (Ici a)<VAR>x : ℝ<VAR>hx : x ∈ Ioi a<VAR>h'x : a ≤ id x<GOAL>IntegrableOn f' (Ioc a (id x)) volume
<VAR>n : ℕ<GOAL>map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal
<VAR>n : ℕ<GOAL>Prod.swap ⁻¹' ↑n.divisorsAntidiagonal = ↑n.divisorsAntidiagonal
<VAR>n : ℕ<VAR>x✝ : ℕ × ℕ<GOAL>x✝ ∈ Prod.swap ⁻¹' ↑n.divisorsAntidiagonal ↔ x✝ ∈ ↑n.divisorsAntidiagonal
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>H : Embedding ⇑f<VAR>g : Y ⟶ S<GOAL>Embedding ⇑(pullback.snd f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>H : Embedding ⇑f<VAR>g : Y ⟶ S<GOAL>⇑(pullback.snd f g) = ⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) ∘ ⇑(pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>H : Embedding ⇑f<VAR>g : Y ⟶ S<GOAL>⇑(pullback.snd f g) = ⇑(pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯ ≫ (asIso (pullback.snd (𝟙 S) g)).hom)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : CommSemiring K<VAR>i : R →+* K<VAR>a✝ b : R<VAR>bi : K<VAR>N : ℕ<VAR>a : R<VAR>bu : bi * i b = 1<GOAL>i 0 = i b ^ N * eval (i a * bi) (Polynomial.map i 0)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : Semifield R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<GOAL>quasispectrum R a = spectrum R a ∪ {0}
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁷ : CommSemiring R✝<VAR>inst✝⁶ : NonUnitalRing A✝<VAR>inst✝⁵ : Module R✝ A✝<VAR>inst✝⁴ : IsScalarTower R✝ A✝ A✝<VAR>inst✝³ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝² : Semifield R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<GOAL>{0} = {r | ¬IsUnit r}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n : ℕ<GOAL>Even a ↔ ∃ b, a = 2 * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>o : Option α<GOAL>(∀ (x : α), some x ≠ o) ↔ o = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>o : Option α<GOAL>(¬∀ (x : α), some x ≠ o) ↔ ¬o = none
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<GOAL>((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card) ^ 2 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>key : 16 ^ P.parts.card = ↑((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts).card<GOAL>((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card) ^ 2 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>key : 16 ^ P.parts.card = ↑((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts).card<GOAL>((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / ↑((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts).card) ^ 2 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / ↑((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts).card
<VAR>l m r ml mm mr : List Char<VAR>b e : Pos<GOAL>∃ l' r', ValidFor l' mm r' ({ str := { data := l ++ (ml ++ mm ++ mr) ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len (ml ++ mm ++ mr) } }.extract { byteIdx := utf8Len ml } { byteIdx := utf8Len ml + utf8Len mm })
<VAR>l m r ml mm mr : List Char<VAR>b e : Pos<GOAL>∃ l' r', ValidFor l' mm r' (if utf8Len ml + utf8Len mm ≤ utf8Len ml then { str := "", startPos := 0, stopPos := 0 } else { str := { data := l ++ (ml ++ (mm ++ (mr ++ r))) }, startPos := { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml }), stopPos := { byteIdx := utf8Len l + (utf8Len ml + (utf8Len mm + utf8Len mr)) }.min ({ byteIdx := utf8Len l } + { byteIdx := utf8Len ml + utf8Len mm }) })
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>h : LocallyBoundedVariationOn f univ<GOAL>∀ᵐ (x : ℝ), DifferentiableAt ℝ f x
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>h : LocallyBoundedVariationOn f univ<VAR>x : ℝ<VAR>hx : x ∈ univ → DifferentiableWithinAt ℝ f univ x<GOAL>DifferentiableAt ℝ f x
<VAR>α : Type u_1<VAR>inst✝⁴ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝³ : PseudoEMetricSpace E<VAR>V : Type u_3<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>f : ℝ → V<VAR>h : LocallyBoundedVariationOn f univ<VAR>x : ℝ<VAR>hx : x ∈ univ → DifferentiableAt ℝ f x<GOAL>DifferentiableAt ℝ f x
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>f.graph.topologicalClosure = f.closure.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>f.graph.topologicalClosure = (Exists.choose hf).graph
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : yn a1 m ∣ yn a1 n<VAR>hp : n % m > 0<GOAL>False
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : yn a1 m ∣ yn a1 n<VAR>hp : n % m > 0<VAR>co : (yn a1 m).Coprime (xn a1 (m * (n / m)))<GOAL>False
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : yn a1 m ∣ yn a1 n<VAR>hp : n % m > 0<VAR>co : (yn a1 m).Coprime (xn a1 (m * (n / m)))<VAR>m0 : 0 < m<GOAL>False
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))<VAR>hp : n % m > 0<VAR>co : (yn a1 m).Coprime (xn a1 (m * (n / m)))<VAR>m0 : 0 < m<GOAL>False
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>x✝ : m ∣ n<VAR>k : ℕ<VAR>e : n = m * k<GOAL>yn a1 m ∣ yn a1 (m * k)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ g✝ : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>u : Ultrafilter α<VAR>f g : Filter α<GOAL>¬↑u ≤ f ⊔ g ↔ ¬(↑u ≤ f ∨ ↑u ≤ g)
<VAR>K : Type u_1<VAR>inst✝ : LinearOrderedField K<VAR>a b c : K<VAR>ha : a ≠ 0<VAR>h : ∀ (x : K), a * x * x + b * x + c < 0<GOAL>∀ (x : K), 0 < -a * x * x + -b * x + -c
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>m : Nat<GOAL>(modifyNth f n l).get? m = (fun a => if n = m then f a else a) <$> l.get? m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>f : α →₀ M<VAR>h : a' ≠ a<GOAL>(erase a f) a' = f a'