ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>hr : ↑r < p.radius<VAR>k : ℕ<VAR>r' : ℝ≥0<VAR>h0 : 0 < r'<VAR>hr' : ↑r + ↑r' < p.radius<GOAL>Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<VAR>hI : Nat.Prime (absNorm I)<GOAL>span {↑(absNorm I)} = comap (algebraMap ℤ S) I
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<VAR>hI : Nat.Prime (absNorm I)<VAR>this : (span {↑(absNorm I)}).IsPrime<GOAL>span {↑(absNorm I)} = comap (algebraMap ℤ S) I
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<VAR>hI : Nat.Prime (absNorm I)<VAR>this : (span {↑(absNorm I)}).IsPrime<GOAL>comap (algebraMap ℤ S) I ≠ ⊤
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<VAR>hI : Nat.Prime (absNorm I)<VAR>this : (span {↑(absNorm I)}).IsPrime<GOAL>span {↑(absNorm I)} ≤ comap (algebraMap ℤ S) I
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<VAR>hI : Nat.Prime (absNorm I)<VAR>this : (span {↑(absNorm I)}).IsPrime<GOAL>span {↑(absNorm I)} ≠ ⊥
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>a₂ : 𝕎 k<GOAL>solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>a₂ : 𝕎 k<VAR>this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0<GOAL>solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>a₂ : 𝕎 k<VAR>this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0<VAR>q : ℕ<VAR>hq : p = q.succ<GOAL>solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>a₂ : 𝕎 k<VAR>this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0<VAR>q : ℕ<VAR>hq : p = q.succ<VAR>hq' : q = p - 1<GOAL>solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>a₂ : 𝕎 k<VAR>this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0<VAR>q : ℕ<VAR>hq : p = q.succ<VAR>hq' : q = p - 1<GOAL>solution p a₁ a₂ ^ q.succ * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : IsAlgClosed k<VAR>a₁ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>a₂ : 𝕎 k<VAR>this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0<VAR>q : ℕ<VAR>hq : p = q.succ<VAR>hq' : q = p - 1<GOAL>solution p a₁ a₂ * (a₂.coeff 0 / a₁.coeff 0) * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>T : s.Terminates<VAR>a : α<VAR>h : a ∈ s<GOAL>s.Results a s.length
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>T : s.Terminates<VAR>a : α<VAR>h : a ∈ s<GOAL>s.Results s.get s.length
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>hf : LipschitzWith K f<VAR>s : Set α<GOAL>diam (f '' s) ≤ ↑K * diam s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>hf : LipschitzWith K f<VAR>s : Set α<GOAL>∀ x ∈ f '' s, ∀ y ∈ f '' s, edist x y ≤ ↑K * diam s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x✝ y✝ : α<VAR>r : ℝ≥0∞<VAR>hf : LipschitzWith K f<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<GOAL>edist (f x) (f y) ≤ ↑K * diam s
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>c' : ℤ := ↑g 1 0<VAR>c : ℝ := ↑c'<GOAL>|↑g 1 0| ≤ 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>c' : ℤ := ↑g 1 0<VAR>c : ℝ := ↑c'<GOAL>3 * c ^ 2 < 4
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>c' : ℤ := ↑g 1 0<VAR>c : ℝ := ↑c'<VAR>hc : c ≠ 0<GOAL>9 * c ^ 4 < 16
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>c' : ℤ := ↑g 1 0<VAR>c : ℝ := ↑c'<VAR>hc : 0 < c ^ 4<GOAL>9 * c ^ 4 < 16
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>c' : ℤ := ↑g 1 0<VAR>c : ℝ := ↑c'<VAR>hc : 0 < c ^ 4<VAR>h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4<GOAL>9 * c ^ 4 < 16
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>c' : ℤ := ↑g 1 0<VAR>c : ℝ := ↑c'<VAR>hc : 0 < c ^ 4<VAR>h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4<VAR>h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1<GOAL>9 * c ^ 4 < 16
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : g • z ∈ 𝒟ᵒ<VAR>c' : ℤ := ↑g 1 0<VAR>c : ℝ := ↑c'<VAR>hc : 0 < c ^ 4<VAR>h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4<VAR>h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1<VAR>nsq : ℝ := normSq (denom (↑g) z)<GOAL>9 * c ^ 4 < 16
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>x y : E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<GOAL>y ∈ openSegment 𝕜 x y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (s i)<VAR>hd : Directed (fun x x_1 => x ⊇ x_1) s<VAR>k : ι<VAR>hk : μ (s k) ≠ ⊤<GOAL>μ (⋂ i, s i) = ⨅ i, μ (s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (s i)<VAR>hd : Directed (fun x x_1 => x ⊇ x_1) s<VAR>k : ι<VAR>hk : μ (s k) ≠ ⊤<VAR>this : ∀ t ⊆ s k, μ t ≠ ⊤<GOAL>μ (⋂ i, s i) = ⨅ i, μ (s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (s i)<VAR>hd : Directed (fun x x_1 => x ⊇ x_1) s<VAR>k : ι<VAR>hk : μ (s k) ≠ ⊤<VAR>this : ∀ t ⊆ s k, μ t ≠ ⊤<GOAL>μ (s k) - ⨆ i, μ (s k \ s i) = μ (s k) - ⨆ i, μ (s k) - μ (s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), MeasurableSet (s i)<VAR>hd : Directed (fun x x_1 => x ⊇ x_1) s<VAR>k : ι<VAR>hk : μ (s k) ≠ ⊤<VAR>this : ∀ t ⊆ s k, μ t ≠ ⊤<GOAL>Directed (fun x x_1 => x ⊆ x_1) fun i => s k \ s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p q : α → Prop<VAR>inst✝² : Fintype { x // p x }<VAR>inst✝¹ : Fintype { x // q x }<VAR>inst✝ : Fintype { x // p x ∨ q x }<GOAL>card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }
<VAR>α : Type u_1<VAR>k n m : ℕ<VAR>H : Raised n m<GOAL>Raised (n + k) (m + k)
<VAR>α : Type u_1<VAR>k n m : ℕ<VAR>H : Raised n m<GOAL>Raised (k + n) (k + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a b : α<VAR>s✝ s : Finset β<VAR>f : β → α<GOAL>HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a b : α<VAR>s✝ s : Finset β<VAR>f : β → α<GOAL>HasProd (f ∘ Subtype.val) (∏ x ∈ s.attach, f ↑x)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>g : G<VAR>P : Sylow p G<GOAL>g • P = P ↔ g ∈ (↑P).normalizer
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>g : G<VAR>P : Sylow p G<GOAL>(∀ (x : G), x ∈ P ↔ x ∈ g • P) ↔ ∀ (h : G), h ∈ ↑P ↔ g⁻¹ * h * g ∈ ↑P
<VAR>this : Irrational √↑5<GOAL>Irrational ψ
<VAR>this✝ : Irrational √↑5<VAR>this : Irrational (↑1 - √↑5)<GOAL>Irrational ψ
<VAR>this✝¹ : Irrational √↑5<VAR>this✝ : Irrational (↑1 - √↑5)<VAR>this : Irrational (↑0.5 * (↑1 - √↑5))<GOAL>Irrational ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : A ⊗[R] L<GOAL>⁅x, x⁆ = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : A ⊗[R] L<GOAL>((LieAlgebra.ExtendScalars.bracket' R A L L) x) x = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : A ⊗[R] L<GOAL>((LieAlgebra.ExtendScalars.bracket' R A L L) 0) 0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : A ⊗[R] L<GOAL>∀ (x : A) (y : L), ((LieAlgebra.ExtendScalars.bracket' R A L L) (x ⊗ₜ[R] y)) (x ⊗ₜ[R] y) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x : A ⊗[R] L<GOAL>∀ (x y : A ⊗[R] L), ((LieAlgebra.ExtendScalars.bracket' R A L L) x) x = 0 → ((LieAlgebra.ExtendScalars.bracket' R A L L) y) y = 0 → ((LieAlgebra.ExtendScalars.bracket' R A L L) (x + y)) (x + y) = 0
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<GOAL>↑(ℜ a) + I • ↑(ℑ a) = a
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x : RatFunc K<GOAL>(-x).num * x.denom = -x.num * (-x).denom
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<GOAL>weightSpace M (-α + ⇑(chainBot α β)) = ⊥
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r ε : ℝ<VAR>L : E →L[𝕜] F<VAR>x y z : E<VAR>hy : y ∈ closedBall x (r / 2)<VAR>hz : z ∈ closedBall x (r / 2)<VAR>r' : ℝ<VAR>r'mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<GOAL>‖f z - f y - L (z - y)‖ ≤ ε * r
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>r ε : ℝ<VAR>L : E →L[𝕜] F<VAR>x y z : E<VAR>hy : y ∈ closedBall x (r / 2)<VAR>hz : z ∈ closedBall x (r / 2)<VAR>r' : ℝ<VAR>r'mem : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r<GOAL>‖f z - f y - L (z - y)‖ < ε * r
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.28046, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X : Dial C<GOAL>(tensorUnit.tensorObj X).rel = (Subobject.pullback (prod.map (prod.leftUnitor X.src).hom (prod.leftUnitor X.tgt).hom)).obj X.rel
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<GOAL>∀ (x : 𝕎 R), select P x + select (fun i => ¬P i) x = x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x : 𝕎 R<GOAL>∀ (n : ℕ), (ghostComponent n) (select P x + select (fun i => ¬P i) x) = (ghostComponent n) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(ghostComponent n) (select P x + select (fun i => ¬P i) x) = (ghostComponent n) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(ghostComponent n) (select P x) + (ghostComponent n) (select (fun i => ¬P i) x) = (ghostComponent n) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>∑ x ∈ Finset.range (n + 1), C ↑p ^ x * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x)) = ∑ x ∈ Finset.range (n + 1), C ↑p ^ x * X x ^ p ^ (n - x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>∀ x ∈ Finset.range (n + 1), C ↑p ^ x * ((if P x then X x else 0) ^ p ^ (n - x) + (if ¬P x then X x else 0) ^ p ^ (n - x)) = C ↑p ^ x * X x ^ p ^ (n - x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x : 𝕎 R<VAR>n m : ℕ<VAR>x✝ : m ∈ Finset.range (n + 1)<GOAL>(if P m then X m else 0) ^ p ^ (n - m) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>this : IsPoly p fun {R} [CommRing R] x => select P x + select (fun i => ¬P i) x<VAR>R : Type u_1<VAR>R._inst : CommRing R<VAR>x : 𝕎 R<VAR>n m : ℕ<VAR>x✝ : m ∈ Finset.range (n + 1)<GOAL>(if P m then X m ^ p ^ (n - m) else 0) + (if ¬P m then X m else 0) ^ p ^ (n - m) = X m ^ p ^ (n - m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>(∃ t ∈ g, ∀ᶠ (y : α) in f, ∀ x ∈ t, (x, y) ∈ (fun p => (p.2, p.1)) ⁻¹' s) ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
<VAR>a b c d m✝ n✝ : ℤ<VAR>m n : ℕ<VAR>h : n.succ ≤ m<GOAL>ofNat m + -[n+1] = ofNat (m - n.succ)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>coeff✝¹ coeff✝ : ℕ → R<VAR>h : ∀ (n : ℕ), coeff✝¹ n = coeff✝ n<GOAL>{ coeff := coeff✝¹ } = { coeff := coeff✝ }
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<GOAL>WithBot.map (⇑ofDual) s.max = (image (⇑ofDual) s).min
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset αᵒᵈ<GOAL>WithBot.map (⇑ofDual) s.max = s.inf (WithTop.some ∘ ⇑ofDual)
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>s * closedBall 1 δ = cthickening δ s
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x✝ y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<VAR>x : E<GOAL>x ∈ s * closedBall 1 δ ↔ x ∈ ⋃ x ∈ s, closedBall x δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>hN' : N ≤ 4096<GOAL>↑N * rexp (-4 * √(log ↑N)) ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>hN' : N ≤ 4096<GOAL>↑N ≤ rexp (4 ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>hN' : N ≤ 4096<GOAL>↑N ≤ rexp 16
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>hN' : N ≤ 4096<GOAL>↑N ≤ 4096
<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>X Y Z : C<VAR>f : J → C<VAR>g h : X ⟶ Y ⊗ Z ⊗ ⨁ f<VAR>w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j<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>X Y Z : C<VAR>f : J → C<VAR>g h : X ⟶ Y ⊗ Z ⊗ ⨁ f<VAR>w : ∀ (j : J), g ≫ Y ◁ Z ◁ biproduct.π f j = h ≫ Y ◁ Z ◁ biproduct.π f j<GOAL>g ≫ (α_ Y Z (⨁ f)).inv = h ≫ (α_ Y Z (⨁ f)).inv
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>h : OpenEmbedding ⇑f<GOAL>⋯.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>h : OpenEmbedding ⇑f<GOAL>CompatiblePreserving (Opens.grothendieckTopology ↑Y) ⋯.functor
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C Y<VAR>h : OpenEmbedding ⇑f<GOAL>CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) ⋯.functor
<GOAL>Tendsto sin (𝓝[<] (π / 2)) (𝓝 1)
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<GOAL>basisDivisor x x = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>u : F → E<VAR>f : Filter F<VAR>y₀ : E<GOAL>Tendsto u f (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>u : F → E<VAR>f : Filter F<VAR>y₀ : E<GOAL>(∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>P : MvPolynomial σ R → Prop<VAR>p : MvPolynomial σ R<VAR>h1 : ∀ (u : σ →₀ ℕ) (a : R), P ((monomial u) a)<VAR>h2 : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)<VAR>this : P ((monomial 0) 0)<GOAL>P 0
<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>p : ℕ<GOAL>p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
<VAR>b p : ℕ<VAR>hab : Coprime 0 b<GOAL>p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList
<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>p : ℕ<VAR>ha : a > 0<GOAL>p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
<VAR>a p : ℕ<VAR>ha : a > 0<VAR>hab : a.Coprime 0<GOAL>p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0
<VAR>a b : ℕ<VAR>hab : a.Coprime b<VAR>p : ℕ<VAR>ha : a > 0<VAR>hb : b > 0<GOAL>p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>x₀ : X<VAR>h₁ : Tendsto F l (𝓝 f)<VAR>h₂ : EquicontinuousAt F x₀<GOAL>ContinuousAt f x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>x₀ : X<VAR>h₁ : ∀ (x : X), Tendsto (fun i => F i x) l (𝓝 (f x))<VAR>h₂ : EquicontinuousWithinAt F univ x₀<GOAL>ContinuousWithinAt f univ x₀
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>{ x // x ∈ hs.toFinset } = ↑s
<VAR>R : Type u<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>x y : R<GOAL>star (star x * y) = star y * x
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>S : Submonoid M<VAR>x y : M<VAR>z : ↥S<VAR>h₁ : y * ↑z = 1<VAR>h₂ : x * y = 1<GOAL>x ∈ S