ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig α N τ<VAR>i : Fin N.succ<VAR>h : 1 ≤ τ<VAR>H : last N ≤ i<GOAL>a.r (last N) ≤ τ * a.r i
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>n : ℕ<GOAL>f^[n.succ] = f ∘ f^[n]
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<VAR>x✝ : b = a<VAR>e : b = a := x✝<GOAL>indexOf b (b :: l) = 0
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>g : GenContFract K := of v<GOAL>(of v).dens n ≤ (of v).dens (n + 1)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>g : GenContFract K := of v<VAR>terminated : g.partDens.TerminatedAt n<GOAL>(of v).dens n ≤ (of v).dens (n + 1)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>g : GenContFract K := of v<VAR>not_terminated : ¬g.partDens.TerminatedAt n<GOAL>(of v).dens n ≤ (of v).dens (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<GOAL>(fun x => !x) ∘ isNone = isSome
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>x : Option α<GOAL>((fun x => !x) ∘ isNone) x = x.isSome
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x✝ : α<VAR>δ : ℝ<VAR>hδ : δ ≤ 0<VAR>E : Set α<VAR>x : α<GOAL>x ∈ cthickening δ E ↔ x ∈ closure E
<VAR>p k n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
<VAR>p k n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : k ≤ n + k<GOAL>(p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
<VAR>p k n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : k ≤ n + k<GOAL>(p - 1) * padicValNat p ((n + k)! / (k ! * (n + k - k)!)) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
<VAR>p k n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : k ≤ n + k<GOAL>(p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
<VAR>p k n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : k ≤ n + k<GOAL>n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.92724, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>i j k : ℤ<VAR>hij : i + 1 = j<VAR>hjk : j + 1 = k<GOAL>(mappingCone φ).d i j ≫ (↑(fst φ)).v j k hjk = -(↑(fst φ)).v i j hij ≫ F.d j k
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>F' : D ⥤ C<VAR>A B : C<VAR>adj : F ⊣ F'<VAR>f : A ⟶ B<VAR>h₁ : F'.PreservesMonomorphisms<VAR>h₂ : F.PreservesEpimorphisms<VAR>inst✝¹ : StrongEpi f<VAR>X Y : D<VAR>Z : X ⟶ Y<VAR>inst✝ : Mono Z<GOAL>HasLiftingProperty (F.map f) Z
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>F' : D ⥤ C<VAR>A B : C<VAR>adj : F ⊣ F'<VAR>f : A ⟶ B<VAR>h₁ : F'.PreservesMonomorphisms<VAR>h₂ : F.PreservesEpimorphisms<VAR>inst✝¹ : StrongEpi f<VAR>X Y : D<VAR>Z : X ⟶ Y<VAR>inst✝ : Mono Z<GOAL>HasLiftingProperty f (F'.map Z)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>p q : ℕ<VAR>inst✝ : CharP K p<VAR>h : p ∣ q<GOAL>(X ^ q - X).Separable
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>p q : ℕ<VAR>inst✝ : CharP K p<VAR>h : p ∣ q<GOAL>1 * (X ^ q - X) + (X ^ q - X - 1) * derivative (X ^ q - X) = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>p q : ℕ<VAR>inst✝ : CharP K p<VAR>h : ↑q = 0<GOAL>1 * (X ^ q - X) + (X ^ q - X - 1) * derivative (X ^ q - X) = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>p q : ℕ<VAR>inst✝ : CharP K p<VAR>h : ↑q = 0<GOAL>1 * (X ^ q - X) + (X ^ q - X - 1) * (0 * X ^ (q - 1) - 1) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>i : ℕ<VAR>a : A<VAR>ha : a ∈ asIdeal f_deg hm q<VAR>j : ℕ<VAR>h : i = j<GOAL>HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) ↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>i : ℕ<VAR>a : A<VAR>ha : a ∈ asIdeal f_deg hm q<VAR>j : ℕ<VAR>h : ¬i = j<GOAL>HomogeneousLocalization.mk { deg := m * j, num := ⟨(proj 𝒜 j) ↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ j, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ : Measure β<VAR>s : Set α<GOAL>(Measure.comap f μ).restrict s = Measure.comap f (μ.restrict (f '' s))
<VAR>a : Ordinal.{u_1}<VAR>a0 : a ≠ 0<GOAL>0 ^ a = 0
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a b✝ b c : α<VAR>l₁ l₂ : List α<GOAL>Chain' R (l₁ ++ b :: c :: l₂) ↔ Chain' R (l₁ ++ [b]) ∧ R b c ∧ Chain' R (c :: l₂)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<GOAL>padicValRat p q ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<GOAL>padicValRat p q ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<VAR>hqd : ↑q.den ≠ 0<GOAL>padicValRat p q ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<VAR>hqd : ↑q.den ≠ 0<VAR>hrn : r.num ≠ 0<GOAL>padicValRat p q ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<VAR>hqd : ↑q.den ≠ 0<VAR>hrn : r.num ≠ 0<VAR>hrd : ↑r.den ≠ 0<GOAL>padicValRat p q ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<VAR>hqd : ↑q.den ≠ 0<VAR>hrn : r.num ≠ 0<VAR>hrd : ↑r.den ≠ 0<VAR>hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)<GOAL>padicValRat p q ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<VAR>hqd : ↑q.den ≠ 0<VAR>hrn : r.num ≠ 0<VAR>hrd : ↑r.den ≠ 0<VAR>hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)<VAR>hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0<GOAL>padicValRat p q ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<VAR>hqd : ↑q.den ≠ 0<VAR>hrn : r.num ≠ 0<VAR>hrd : ↑r.den ≠ 0<VAR>hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)<VAR>hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0<GOAL>padicValRat p (q.num /. ↑q.den) ≤ padicValRat p (q + r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : padicValRat p q ≤ padicValRat p r<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<VAR>hqd : ↑q.den ≠ 0<VAR>hrn : r.num ≠ 0<VAR>hrd : ↑r.den ≠ 0<VAR>hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)<VAR>hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0<GOAL>multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)<VAR>hq : ¬q = 0<VAR>hr : ¬r = 0<VAR>hqn : q.num ≠ 0<VAR>hqd : ↑q.den ≠ 0<VAR>hrn : r.num ≠ 0<VAR>hrd : ↑r.den ≠ 0<VAR>hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)<VAR>hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0<GOAL>multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>IsUnramified k w ↔ w.mult ≤ (w.comap (algebraMap k K)).mult
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>(w.comap (algebraMap k K)).mult ≤ w.mult
<VAR>x : ℂ<GOAL>cos (x - ↑π / 2) = sin x
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommRing P<VAR>A : Type u_4<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>K : Type u_5<VAR>r : A<VAR>s : ↥(nonZeroDivisors A)<GOAL>Localization.mk r s = (algebraMap A (FractionRing A)) r / (algebraMap A (FractionRing A)) ↑s
<VAR>f : C(↑I, ℝ)<GOAL>Tendsto (fun n => bernsteinApproximation n f) atTop (𝓝 f)
<VAR>f : C(↑I, ℝ)<GOAL>∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < i
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>δ : ℝ := bernsteinApproximation.δ f ε h<GOAL>∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>δ : ℝ := bernsteinApproximation.δ f ε h<VAR>nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)<GOAL>∀ᶠ (x : ℕ) in atTop, ‖bernsteinApproximation x f - f‖ < ε
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>δ : ℝ := bernsteinApproximation.δ f ε h<VAR>nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)<VAR>n : ℕ<VAR>nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2<VAR>npos' : 0 < n<GOAL>‖bernsteinApproximation n f - f‖ < ε
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>δ : ℝ := bernsteinApproximation.δ f ε h<VAR>nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)<VAR>n : ℕ<VAR>nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2<VAR>npos' : 0 < n<VAR>npos : 0 < ↑n<GOAL>‖bernsteinApproximation n f - f‖ < ε
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>δ : ℝ := bernsteinApproximation.δ f ε h<VAR>nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)<VAR>n : ℕ<VAR>nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2<VAR>npos' : 0 < n<VAR>npos : 0 < ↑n<GOAL>∀ (x : ↑I), ‖(bernsteinApproximation n f - f) x‖ < ε
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>δ : ℝ := bernsteinApproximation.δ f ε h<VAR>nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)<VAR>n : ℕ<VAR>nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2<VAR>npos' : 0 < n<VAR>npos : 0 < ↑n<VAR>x : ↑I<VAR>S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x<GOAL>‖(bernsteinApproximation n f - f) x‖ < ε
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>δ : ℝ := bernsteinApproximation.δ f ε h<VAR>nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)<VAR>n : ℕ<VAR>nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2<VAR>npos' : 0 < n<VAR>npos : 0 < ↑n<VAR>x : ↑I<VAR>S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x<GOAL>∑ k ∈ S, |f k/ₙ - f x| * (bernstein n ↑k) x ≤ ε / 2
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>δ : ℝ := bernsteinApproximation.δ f ε h<VAR>nhds_zero : Tendsto (fun n => 2 * ‖f‖ * δ ^ (-2) / ↑n) atTop (𝓝 0)<VAR>n : ℕ<VAR>nh : 2 * ‖f‖ * δ ^ (-2) / ↑n < ε / 2<VAR>npos' : 0 < n<VAR>npos : 0 < ↑n<VAR>x : ↑I<VAR>S : Finset (Fin (n + 1)) := bernsteinApproximation.S f ε h n x<GOAL>∑ k ∈ Sᶜ, |f k/ₙ - f x| * (bernstein n ↑k) x < ε / 2
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝³ : Zero β<VAR>inst✝² : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>inst✝¹ : T1Space β<VAR>b : β<VAR>inst✝ : NeZero b<VAR>x : α<GOAL>Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝³ : Zero β<VAR>inst✝² : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>inst✝¹ : T1Space β<VAR>b : β<VAR>inst✝ : NeZero b<VAR>x : α<GOAL>{0}ᶜ ∈ 𝓝 b
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝³ : Zero β<VAR>inst✝² : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>inst✝¹ : T1Space β<VAR>b : β<VAR>inst✝ : NeZero b<VAR>x : α<GOAL>{b}ᶜ ∈ 𝓝 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<GOAL>TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<GOAL>(∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<GOAL>(connectedComponent x).Subsingleton ↔ connectedComponent x = {x}
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<GOAL>x ∈ connectedComponent x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : Arrow C<VAR>X : Augmented C<VAR>G : F.augmentedCechConerve ⟶ X<GOAL>G.left ≫ X.hom.app (SimplexCategory.mk 0) = (WidePushout.head fun x => F.hom) ≫ G.right.app (SimplexCategory.mk 0)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : TruncatedWittVector p n R<VAR>i : Fin n<GOAL>(if h : ↑i < n then coeff ⟨↑i, h⟩ x else 0) = coeff i x
<VAR>F : Type u_1<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>inst✝ : CompleteSpace F<GOAL>StronglyMeasurable fun x => derivWithin f (Ioi x) x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>r : β → β → Prop<VAR>m : Multiset α<VAR>h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)<VAR>b₁ : β<VAR>h₁ : b₁ ∈ {b | b ∈ map f m}<VAR>b₂ : β<VAR>h₂ : b₂ ∈ {b | b ∈ map f m}<VAR>hn : b₁ ≠ b₂<GOAL>r b₁ b₂
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>r : β → β → Prop<VAR>m : Multiset α<VAR>h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)<VAR>a₁ : α<VAR>H₁ : a₁ ∈ m<VAR>h₁ : f a₁ ∈ {b | b ∈ map f m}<VAR>a₂ : α<VAR>H₂ : a₂ ∈ m<VAR>h₂ : f a₂ ∈ {b | b ∈ map f m}<VAR>hn : f a₁ ≠ f a₂<GOAL>r (f a₁) (f a₂)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>0 < finrank R M ↔ Nontrivial M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : NoZeroSMulDivisors R M<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : NoZeroSMulDivisors R M<GOAL>0 < finrank R M ↔ 0 < ↑(finrank R M)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : NullMeasurableSet t μ<VAR>hfs : IntegrableOn f s μ<GOAL>∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : NullMeasurableSet t μ<VAR>hfs : IntegrableOn f s μ<GOAL>Integrable f (μ.restrict (s ∩ t))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht : NullMeasurableSet t μ<VAR>hfs : IntegrableOn f s μ<GOAL>Integrable f (μ.restrict (s \ t))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] E<VAR>hA : IsSelfAdjoint A<VAR>x y : E<GOAL>⟪↑A x, y⟫_𝕜 = ⟪x, ↑A y⟫_𝕜
<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>a : R<VAR>b : ↥M<VAR>c : R<VAR>d : ↥M<GOAL>mk a b + mk c d = mk (↑b * c + ↑d * a) (b * d)
<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>a : R<VAR>b : ↥M<VAR>c : R<VAR>d : ↥M<GOAL>mk a b + mk c d = mk (↑d * a + ↑b * c) (d * b)
<VAR>x : ℝ≥0∞<VAR>h : 0 < x.toReal<GOAL>x.log = ↑(Real.log x.toReal)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>s : Set A<VAR>x : ProjectiveSpectrum 𝒜<GOAL>x ∈ zeroLocus 𝒜 ↑(Ideal.span s) ↔ x ∈ zeroLocus 𝒜 s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Mul A<VAR>inst✝ : SMulWithZero R A<VAR>a₁ a₂ : A<GOAL>a₁ * a₂ = 0 • a₂ + 0 • a₁ + a₁ * a₂
<VAR>R✝ : Type u_1<VAR>inst✝¹⁶ : CommRing R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝¹⁵ : CommRing S✝<VAR>inst✝¹⁴ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝¹³ : CommRing P<VAR>A : Type u_4<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝¹⁰ : CommRing B<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : Field K<VAR>L : Type u_7<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Algebra A K<VAR>inst✝⁵ : IsFractionRing A K<VAR>g : A →+* L<VAR>R : Type u_8<VAR>S : Type u_9<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsFractionRing R S<GOAL>Nontrivial S
<VAR>R✝ : Type u_1<VAR>inst✝¹⁶ : CommRing R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝¹⁵ : CommRing S✝<VAR>inst✝¹⁴ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝¹³ : CommRing P<VAR>A : Type u_4<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝¹⁰ : CommRing B<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : Field K<VAR>L : Type u_7<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Algebra A K<VAR>inst✝⁵ : IsFractionRing A K<VAR>g : A →+* L<VAR>R : Type u_8<VAR>S : Type u_9<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsFractionRing R S<GOAL>?x ≠ ?y
<VAR>R✝ : Type u_1<VAR>inst✝¹⁶ : CommRing R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝¹⁵ : CommRing S✝<VAR>inst✝¹⁴ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝¹³ : CommRing P<VAR>A : Type u_4<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝¹⁰ : CommRing B<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : Field K<VAR>L : Type u_7<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Algebra A K<VAR>inst✝⁵ : IsFractionRing A K<VAR>g : A →+* L<VAR>R : Type u_8<VAR>S : Type u_9<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : IsFractionRing R S<GOAL>S
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>(∀ (m : ℕ), ↑m ≤ ⊤ → ContDiffOn 𝕜 (↑m) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<GOAL>ker f = IsSubgroup.trivial G ↔ ∀ (x : G), f x = 1 → x = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<GOAL>(∀ (x : G), x ∈ ker f ↔ x ∈ IsSubgroup.trivial G) ↔ ∀ (x : G), f x = 1 → x = 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => (s - ↑P.k) • P.Λ s) (𝓝[≠] ↑P.k) (𝓝 (P.ε • P.g₀))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => (s - ↑P.k) • P.Λ₀ s - (s - ↑P.k) • (1 / s) • P.f₀ - (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] ↑P.k) (𝓝 (0 - 0 - -P.ε • P.g₀))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => (s - ↑P.k) • P.Λ₀ s) (𝓝 ↑P.k) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => (s - ↑P.k) • (1 / s) • P.f₀) (𝓝 ↑P.k) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<GOAL>Tendsto (fun s => (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] ↑P.k) (𝓝 (-P.ε • P.g₀))