ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hiw : ⟪i w, w⟫_ℝ = 1 / 2<VAR>this : (fun v => 𝐞 (-⟪v, w⟫_ℝ) • f (v + i w)) = fun v => (fun x => -(𝐞 (-⟪x, w⟫_ℝ) • f x)) (v + i w)<GOAL>∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f (v + i w) = -∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hiw : ⟪i w, w⟫_ℝ = 1 / 2<VAR>this : (fun v => 𝐞 (-⟪v, w⟫_ℝ) • f (v + i w)) = fun v => (fun x => -(𝐞 (-⟪x, w⟫_ℝ) • f x)) (v + i w)<GOAL>∫ (v : V), (fun x => -(𝐞 (-⟪x, w⟫_ℝ) • f x)) (v + i w) = -∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hiw : ⟪i w, w⟫_ℝ = 1 / 2<VAR>this✝ : (fun v => 𝐞 (-⟪v, w⟫_ℝ) • f (v + i w)) = fun v => (fun x => -(𝐞 (-⟪x, w⟫_ℝ) • f x)) (v + i w)<VAR>this : ∫ (x : V), -(𝐞 (-⟪x + i w, w⟫_ℝ) • f (x + i w)) = ∫ (x : V), -(𝐞 (-⟪x, w⟫_ℝ) • f x)<GOAL>∫ (v : V), (fun x => -(𝐞 (-⟪x, w⟫_ℝ) • f x)) (v + i w) = -∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v
<VAR>E : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>inst✝ : CompleteSpace E<VAR>w : V<VAR>hw : w ≠ 0<VAR>hiw : ⟪i w, w⟫_ℝ = 1 / 2<VAR>this✝ : (fun v => 𝐞 (-⟪v, w⟫_ℝ) • f (v + i w)) = fun v => (fun x => -(𝐞 (-⟪x, w⟫_ℝ) • f x)) (v + i w)<VAR>this : ∫ (x : V), -(𝐞 (-⟪x + i w, w⟫_ℝ) • f (x + i w)) = ∫ (x : V), -(𝐞 (-⟪x, w⟫_ℝ) • f x)<GOAL>∫ (x : V), -(𝐞 (-⟪x, w⟫_ℝ) • f x) = -∫ (v : V), 𝐞 (-⟪v, w⟫_ℝ) • f v
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : Field R<VAR>inst✝¹ : Module R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>x : F<VAR>t : R<VAR>ht : t ≠ 0<GOAL>IsOpenMap ⇑(homothety x t)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z<VAR>hc : ContinuousAt f c<GOAL>AnalyticAt ℂ f c
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z<VAR>hc : ContinuousAt f c<VAR>R : ℝ<VAR>hR0 : 0 < R<VAR>hRs : closedBall c R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}<GOAL>AnalyticAt ℂ f c
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z<VAR>hc : ContinuousAt f c<VAR>R : ℝ≥0<VAR>hR0 : 0 < ↑R<VAR>hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}<GOAL>AnalyticAt ℂ f c
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z<VAR>R : ℝ≥0<VAR>hR0 : 0 < ↑R<VAR>hRs : closedBall c ↑R ∩ {c}ᶜ ⊆ {x | (fun z => DifferentiableAt ℂ f z) x}<VAR>hc : ContinuousOn f (closedBall c ↑R)<GOAL>AnalyticAt ℂ f c
<VAR>m n : ℤ<GOAL>Odd (m + n) ↔ (Odd m ↔ Even n)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>(P y / P z ^ 3 - Q y / Q z ^ 3) / ((P x * Q z ^ 2 - Q x * P z ^ 2) / (P z ^ 2 * Q z ^ 2)) = (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>(P y * Q z ^ 3 - P z ^ 3 * Q y) * (P z ^ 2 * Q z ^ 2) * (P z * Q z * (P x * Q z ^ 2 - Q x * P z ^ 2)) = (P y * Q z ^ 3 - Q y * P z ^ 3) * (P z ^ 3 * Q z ^ 3 * (P x * Q z ^ 2 - Q x * P z ^ 2))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<GOAL>(↑‖a‖₊)⁻¹ ≤ radius fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>r : ℝ≥0<VAR>hr : ↑r < (↑‖a‖₊)⁻¹<VAR>n : ℕ<GOAL>‖ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)‖₊ * r ^ n ≤ max 1 ‖1‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>r : ℝ≥0<VAR>hr : ↑r < (↑‖a‖₊)⁻¹<VAR>n : ℕ<GOAL>‖a ^ n‖₊ * r ^ n ≤ max 1 ‖1‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>y : 𝕜<VAR>hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹<VAR>norm_lt : ‖y • a‖ < 1<GOAL>HasSum (fun n => (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) fun x => y) (Ring.inverse (1 - (0 + y) • a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>g : C(X, Z)<VAR>h : FactorsThrough ⇑g ⇑f<VAR>a✝ : X<GOAL>((hf.lift g h).comp f) a✝ = g a✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>ι : Type u_5<VAR>ιₘ : Type u_6<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : Nontrivial R<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : Algebra R A<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : Module.Finite R L<VAR>inst✝¹⁰ : Module.Free R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : LieRingModule L M<VAR>inst✝⁶ : LieModule R L M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ιₘ<VAR>inst✝ : DecidableEq ιₘ<VAR>b : Basis ι R L<VAR>bₘ : Basis ιₘ R M<VAR>x : L<GOAL>rank R L = ((↑(ad R L)).polyCharpoly b).natTrailingDegree
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : BaireSpace X<VAR>inst✝¹ : Nonempty X<VAR>inst✝ : Countable ι<VAR>f : ι → Set X<VAR>hc : ∀ (i : ι), IsClosed (f i)<VAR>hU : ⋃ i, f i = univ<GOAL>∃ i, (interior (f i)).Nonempty
<VAR>p : ℕ<VAR>hp : Prime p<GOAL>p.primeFactorsList = [p]
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : p = p - 2 + 2<GOAL>p.primeFactorsList = [p]
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : p = p - 2 + 2<GOAL>(p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : p = p - 2 + 2<GOAL>p.minFac :: (p / p.minFac).primeFactorsList = [p]
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this✝ : p = p - 2 + 2<VAR>this : p.minFac = p<GOAL>p.minFac :: (p / p.minFac).primeFactorsList = [p]
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>ClassGroup.mk (XYIdeal' h₁) * ClassGroup.mk (XYIdeal' h₂) = ClassGroup.mk (XYIdeal' ⋯)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>ClassGroup.mk (XYIdeal' h₁ * XYIdeal' h₂) = ClassGroup.mk (XYIdeal' ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f fab : α → β<VAR>fbc : β → γ<VAR>ga ga' : α → α<VAR>gb gb' : β → β<VAR>gc gc' : γ → γ<VAR>f' : β → α<VAR>h : Semiconj f ga gb<VAR>hf₁ : LeftInverse f' f<VAR>hf₂ : RightInverse f' f<VAR>x : β<GOAL>f' (gb x) = ga (f' x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>(mk W) (C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) = -(XClass W x₁ * XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>(AdjoinRoot.mk W.polynomial) (C (X - C x₁)) * (AdjoinRoot.mk W.polynomial) (C (X - C x₂)) * (AdjoinRoot.mk W.polynomial) (C (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))) = XClass W x₁ * XClass W x₂ * XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π✝ : ι → Set (Set Ω)<VAR>m : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>S : Finset ι<VAR>s : ι → Set Ω<VAR>π : ι → Set (Set Ω)<VAR>μ : Measure Ω<GOAL>iIndepSets π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>hu : ∃ u, a < u<VAR>hl : ∃ l, l < a<GOAL>𝓝 a = ⨅ l, ⨅ (_ : l < a), ⨅ u, ⨅ (_ : a < u), 𝓟 (Ioo l u)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>hu : ∃ u, a < u<VAR>hl : ∃ l, l < a<GOAL>(⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = (⨅ i, ⨅ (_ : i < a), 𝓟 (Ioi i)) ⊓ ⨅ i, ⨅ (_ : a < i), 𝓟 (Iio i)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : Aˣ<GOAL>(σ ↑a)⁻¹ = σ ↑a⁻¹
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : Aˣ<VAR>k : 𝕜<VAR>hk : k ∈ (σ ↑a)⁻¹<GOAL>k ∈ σ ↑a⁻¹
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : Aˣ<VAR>k : 𝕜<VAR>hk : k ∈ σ ↑a⁻¹<GOAL>k ∈ (σ ↑a)⁻¹
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : Semiring R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSemiring R<VAR>inst✝ : T2Space R<VAR>I : Ideal C(X, R)<GOAL>IsOpen (setOfIdeal I)
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : Semiring R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSemiring R<VAR>inst✝ : T2Space R<VAR>I : Ideal C(X, R)<GOAL>IsClosed (⋂ i ∈ I, {x | i x = 0})
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝¹ : DecidableEq β<VAR>f : α → β<VAR>s : Finset β<VAR>inst✝ : (x : β) → Decidable (x ∈ Set.range f)<VAR>hf : InjOn f (f ⁻¹' ↑s)<GOAL>↑(image f (s.preimage f hf)) = ↑(filter (fun x => x ∈ Set.range f) s)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝¹ : DecidableEq β<VAR>f : α → β<VAR>s : Finset β<VAR>inst✝ : (x : β) → Decidable (x ∈ Set.range f)<VAR>hf : InjOn f (f ⁻¹' ↑s)<GOAL>{x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<VAR>hf : X - C a ∣ f /ₘ (X - C a)<GOAL>X - C a ∣ derivative f
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>a : K<VAR>hf : X - C a ∣ f /ₘ (X - C a)<VAR>key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f<GOAL>X - C a ∣ derivative f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x y z : α<VAR>s : Set α<GOAL>EMetric.diam (range ⇑f) = ↑(ratio f) * EMetric.diam univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f : F<VAR>g : G<VAR>x y z : α<VAR>s : Set α<GOAL>EMetric.diam (⇑f '' univ) = ↑(ratio f) * EMetric.diam univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>(∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s) ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<GOAL>(iterate f a).tail.get n = (iterate f (f a)).get n
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<GOAL>(iterate f a).get (n + 1) = (iterate f (f a)).get n
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b c : X<VAR>s t : Set X<GOAL>s.ordConnectedComponent a ∈ 𝓝 a ↔ s ∈ 𝓝 a
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b c : X<VAR>s t : Set X<VAR>h : s ∈ 𝓝 a<GOAL>s.ordConnectedComponent a ∈ 𝓝 a
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b✝ c✝ : X<VAR>s t : Set X<VAR>h : s ∈ 𝓝 a<VAR>b c : X<VAR>ha : a ∈ Icc b c<VAR>ha' : Icc b c ∈ 𝓝 a<VAR>hs : Icc b c ⊆ s<GOAL>s.ordConnectedComponent a ∈ 𝓝 a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<GOAL>adjoin F S = ⊥ ↔ S ⊆ ↑⊥
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<GOAL>S ≤ ↑⊥ ↔ S ⊆ ↑⊥
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>x : α × β<GOAL>x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>φ : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ<GOAL>φ = wittStructureInt p Φ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>φ : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ<VAR>k : ℕ<GOAL>φ k = wittStructureInt p Φ k
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>φ : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ<VAR>k : ℕ<GOAL>(map (Int.castRingHom ℚ)) (φ k) = (map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>φ : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ<VAR>k : ℕ<GOAL>(map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>φ : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ<GOAL>(fun k => (map (Int.castRingHom ℚ)) (φ k)) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>φ : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ<GOAL>∀ (n : ℕ), (bind₁ fun k => (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>φ : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ<GOAL>∀ (n : ℕ), (bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<GOAL>(map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<VAR>hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1<GOAL>(map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<VAR>hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1<GOAL>↑n ≠ 0
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝³ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝² : IsDomain K<VAR>inst✝¹ : CharZero K<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<VAR>hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1<VAR>hzero : ↑n = 0<GOAL>False
<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<GOAL>Tendsto (fun i => (As i).indicator fun x => b) 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<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<GOAL>{b}ᶜ ∈ 𝓝 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m✝ n m : ℕ<GOAL>(m + 1) % 2 + m % 2 = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>pred : ι → Prop<VAR>inst✝ : DecidablePred pred<GOAL>((affineCombination k (Finset.subtype pred s) fun i => p ↑i) fun i => w ↑i) = (affineCombination k (filter pred s) p) w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x<GOAL>map (Embedding.subtype p) (Ici a) = Ici ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x<GOAL>map (Embedding.subtype p) (Finset.subtype p (Ici ↑a)) = Ici ↑a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticWithinOn 𝕜 f (s ∩ u)<VAR>x : E<VAR>m : x ∈ s<VAR>u : Set E<VAR>ou : IsOpen u<VAR>xu : x ∈ u<VAR>fu : AnalyticWithinOn 𝕜 f (s ∩ u)<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticWithinOn 𝕜 f (s ∩ u)<VAR>x : E<VAR>m : x ∈ s<VAR>u : Set E<VAR>ou : IsOpen u<VAR>xu : x ∈ u<VAR>fu : AnalyticWithinOn 𝕜 f (s ∩ u)<VAR>r : ℝ<VAR>r0 : r > 0<VAR>ru : Metric.ball x r ⊆ u<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<GOAL>∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.2 ∈ K i → closedBall p.2 p.1 ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<GOAL>∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<VAR>i : ι<VAR>hi : x ∈ K i<GOAL>∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i