ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>μ' : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hμ : μ ≪ μ'<VAR>f : ↥(simpleFunc E 1 μ)<VAR>f' : ↥(simpleFunc E 1 μ')<VAR>h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'<GOAL>↑(toSimpleFunc f) =ᶠ[ae μ] ↑(toSimpleFunc f')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>μ' : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hμ : μ ≪ μ'<VAR>f : ↥(simpleFunc E 1 μ)<VAR>f' : ↥(simpleFunc E 1 μ')<VAR>h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'<GOAL>↑↑↑f =ᶠ[ae μ] ↑(toSimpleFunc f')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>μ' : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hμ : μ ≪ μ'<VAR>f : ↥(simpleFunc E 1 μ)<VAR>f' : ↥(simpleFunc E 1 μ')<VAR>h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'<GOAL>↑↑↑f' =ᶠ[ae μ] ↑(toSimpleFunc f')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>μ' : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hμ : μ ≪ μ'<VAR>f : ↥(simpleFunc E 1 μ)<VAR>f' : ↥(simpleFunc E 1 μ')<VAR>h : ↑↑↑f =ᶠ[ae μ] ↑↑↑f'<VAR>goal' : ↑↑↑f' =ᶠ[ae μ'] ↑(toSimpleFunc f')<GOAL>↑↑↑f' =ᶠ[ae μ] ↑(toSimpleFunc f')
<VAR>ι✝ : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>ι : Type u_2<VAR>δ : ℝ<VAR>f : ι → Set α<VAR>I : Set ι<GOAL>thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, thickening δ (f i)
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁵ : Field F✝<VAR>inst✝⁴ : Field E✝<VAR>inst✝³ : Algebra F✝ E✝<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>m n : ℕ<VAR>hneq : m ≠ n<VAR>heq : F⟮α ^ m⟯ = F⟮α ^ n⟯<VAR>hmn : m < n<VAR>hm : ¬m = 0<GOAL>IsAlgebraic F α
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁵ : Field F✝<VAR>inst✝⁴ : Field E✝<VAR>inst✝³ : Algebra F✝ E✝<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>m n : ℕ<VAR>hneq : m ≠ n<VAR>heq : F⟮α ^ m⟯ = F⟮α ^ n⟯<VAR>hmn : m < n<VAR>hm : ¬m = 0<VAR>r s : F[X]<VAR>h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s<GOAL>IsAlgebraic F α
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁵ : Field F✝<VAR>inst✝⁴ : Field E✝<VAR>inst✝³ : Algebra F✝ E✝<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>m n : ℕ<VAR>hneq : m ≠ n<VAR>heq : F⟮α ^ m⟯ = F⟮α ^ n⟯<VAR>hmn : m < n<VAR>hm : ¬m = 0<VAR>r s : F[X]<VAR>h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s<VAR>hzero : ¬(aeval (α ^ n)) s = 0<GOAL>IsAlgebraic F α
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁵ : Field F✝<VAR>inst✝⁴ : Field E✝<VAR>inst✝³ : Algebra F✝ E✝<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>m n : ℕ<VAR>hneq : m ≠ n<VAR>heq : F⟮α ^ m⟯ = F⟮α ^ n⟯<VAR>hmn : m < n<VAR>r s : F[X]<VAR>h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s<VAR>hzero : ¬(aeval (α ^ n)) s = 0<VAR>hm : 0 < m<GOAL>IsAlgebraic F α
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁵ : Field F✝<VAR>inst✝⁴ : Field E✝<VAR>inst✝³ : Algebra F✝ E✝<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>m n : ℕ<VAR>hneq : m ≠ n<VAR>heq : F⟮α ^ m⟯ = F⟮α ^ n⟯<VAR>hmn : m < n<VAR>r s : F[X]<VAR>h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0<VAR>hzero : ¬(aeval (α ^ n)) s = 0<VAR>hm : 0 < m<GOAL>IsAlgebraic F α
<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁵ : Field F✝<VAR>inst✝⁴ : Field E✝<VAR>inst✝³ : Algebra F✝ E✝<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝² : Field F<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>m n : ℕ<VAR>hneq : m ≠ n<VAR>heq : F⟮α ^ m⟯ = F⟮α ^ n⟯<VAR>hmn : m < n<VAR>r s : F[X]<VAR>h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0<VAR>hm : 0 < m<VAR>hzero : s ≠ 0<GOAL>IsAlgebraic F α
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>n : ℕ∞<VAR>h : ContDiffAt ℂ n e ↑z<GOAL>ContDiffAt ℝ n (fun x => (e ↑x).re) z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>n : ℕ∞<VAR>h : ContDiffAt ℂ n e ↑z<VAR>A : ContDiffAt ℝ n ofReal' z<GOAL>ContDiffAt ℝ n (fun x => (e ↑x).re) z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>n : ℕ∞<VAR>h : ContDiffAt ℂ n e ↑z<VAR>A : ContDiffAt ℝ n ofReal' z<VAR>B : ContDiffAt ℝ n e ↑z<GOAL>ContDiffAt ℝ n (fun x => (e ↑x).re) z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>n : ℕ∞<VAR>h : ContDiffAt ℂ n e ↑z<VAR>A : ContDiffAt ℝ n ofReal' z<VAR>B : ContDiffAt ℝ n e ↑z<VAR>C : ContDiffAt ℝ n re (e ↑z)<GOAL>ContDiffAt ℝ n (fun x => (e ↑x).re) z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasDerivAt e e' ↑z<GOAL>HasDerivAt (fun x => (e ↑x).re) e'.re z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasDerivAt e e' ↑z<VAR>A : HasFDerivAt ofReal' ofRealCLM z<GOAL>HasDerivAt (fun x => (e ↑x).re) e'.re z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasDerivAt e e' ↑z<VAR>A : HasFDerivAt ofReal' ofRealCLM z<VAR>B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)<GOAL>HasDerivAt (fun x => (e ↑x).re) e'.re z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasDerivAt e e' ↑z<VAR>A : HasFDerivAt ofReal' ofRealCLM z<VAR>B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)<VAR>C : HasFDerivAt re reCLM (e (ofRealCLM z))<GOAL>HasDerivAt (fun x => (e ↑x).re) e'.re z
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasDerivAt e e' ↑z<VAR>A : HasFDerivAt ofReal' ofRealCLM z<VAR>B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)<VAR>C : HasFDerivAt re reCLM (e (ofRealCLM z))<GOAL>e'.re = (reCLM.comp ((ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')).comp ofRealCLM)) 1
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>h : HasDerivAt e e' ↑z<VAR>A : HasFDerivAt ofReal' ofRealCLM z<VAR>B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM z)<VAR>C : HasFDerivAt re reCLM (e (ofRealCLM z))<GOAL>e'.re = reCLM ((ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (ofRealCLM 1))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup L<VAR>inst✝⁹ : Module R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype ι'<VAR>inst✝⁴ : Fintype ιM<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq ι'<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>b✝ b : Basis ι R L<VAR>b' : Basis ι' R L<VAR>k : ℕ<GOAL>(φ.polyCharpoly b).coeff k = 0 ↔ (φ.polyCharpoly b').coeff k = 0
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a⁻¹ * a ≤ b * a ↔ 1 ≤ b * a
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁵ : PseudoEMetricSpace X<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G X<VAR>inst✝² : IsometricSMul G X<VAR>inst✝¹ : PseudoEMetricSpace G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => x * a) ⁻¹' ball b r = ball (b / a) r
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁵ : PseudoEMetricSpace X<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G X<VAR>inst✝² : IsometricSMul G X<VAR>inst✝¹ : PseudoEMetricSpace G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>g : G<VAR>f : (Fin n → G) →₀ k<VAR>r : k<GOAL>(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] f) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>g : G<VAR>f : (Fin n → G) →₀ k<VAR>r : k<GOAL>(diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] 0) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>g : G<VAR>f : (Fin n → G) →₀ k<VAR>r : k<GOAL>∀ (a : Fin n → G) (b : k) (f : (Fin n → G) →₀ k), a ∉ f.support → b ≠ 0 → (diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] f) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) f → (diagonalSucc k G n).inv.hom (single g r ⊗ₜ[k] (single a b + f)) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun f => single (g • partialProd f) r) (single a b + f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>↑(⨅ i, f i) = ⋂ i, ↑(f i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsPiSystem (C i)<VAR>s₁ : (i : ι) → Set (α i)<VAR>hs₁ : s₁ ∈ univ.pi C<VAR>s₂ : (i : ι) → Set (α i)<VAR>hs₂ : s₂ ∈ univ.pi C<VAR>hst : (univ.pi s₁ ∩ univ.pi s₂).Nonempty<GOAL>univ.pi s₁ ∩ univ.pi s₂ ∈ univ.pi '' univ.pi C
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsPiSystem (C i)<VAR>s₁ : (i : ι) → Set (α i)<VAR>hs₁ : s₁ ∈ univ.pi C<VAR>s₂ : (i : ι) → Set (α i)<VAR>hs₂ : s₂ ∈ univ.pi C<VAR>hst : (univ.pi fun i => s₁ i ∩ s₂ i).Nonempty<GOAL>(univ.pi fun i => s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsPiSystem (C i)<VAR>s₁ : (i : ι) → Set (α i)<VAR>hs₁ : s₁ ∈ univ.pi C<VAR>s₂ : (i : ι) → Set (α i)<VAR>hs₂ : s₂ ∈ univ.pi C<VAR>hst : ∀ (i : ι), (s₁ i ∩ s₂ i).Nonempty<GOAL>(univ.pi fun i => s₁ i ∩ s₂ i) ∈ univ.pi '' univ.pi C
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedSemiring α<VAR>l : Filter β<VAR>f : β → α<VAR>n : ℕ<VAR>h : Tendsto (fun x => x ^ n) atTop atTop<VAR>hn : n = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν✝ ν : Measure α<VAR>inst✝ : SigmaFinite ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<GOAL>ν.withDensity f = 0 + ν.withDensity f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>B A₁ : C<VAR>f : A₁ ⟶ B<VAR>inst✝ : Mono f<GOAL>ofMkLEMk f f ⋯ = 𝟙 A₁
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>B A₁ : C<VAR>f : A₁ ⟶ B<VAR>inst✝ : Mono f<GOAL>ofMkLEMk f f ⋯ ≫ f = 𝟙 A₁ ≫ f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<GOAL>p.primPart = p
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>hp : p.Monic<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>∃ r', r = (algebraMap A K) r' ∧ r' ∣ p.coeff 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>hp : p.Monic<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>inv : A<VAR>h_inv : 1 = ↑(den A r) * inv<GOAL>∃ r', r = (algebraMap A K) r' ∧ r' ∣ p.coeff 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>hp : p.Monic<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>inv : A<VAR>h_inv : 1 = ↑(den A r) * inv<GOAL>num A r * inv ∣ p.coeff 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>hp : p.Monic<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>inv : A<VAR>h_inv : 1 = ↑(den A r) * inv<GOAL>r = (algebraMap A K) (num A r * inv)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{v}<GOAL>lift.{u, v} (succ a) = succ (lift.{u, v} a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{v}<GOAL>lift.{u, v} a + 1 = succ (lift.{u, v} a)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I : FractionalIdeal R₁⁰ K<VAR>x✝ : ∃ J, I * J = 1<VAR>J : FractionalIdeal R₁⁰ K<VAR>hJ : I * J = 1<GOAL>I * (1 / I) = 1
<VAR>z : ℂ<GOAL>z⁻¹.im = -z.im / normSq z
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>l : Filter α<GOAL>Tendsto (fun x => ‖f x‖) l atTop ↔ Tendsto f l (cobounded E)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>f : α → E<VAR>l : Filter α<GOAL>Tendsto (fun x => ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a ∣ ↑u * b ↔ a ∣ b
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>↑(im z) = I * ((starRingEnd K) z - z) / 2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g✝ : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h : ∀ (x : X), ∃ g, ContinuousAt g (f x) ∧ g (f x) = x ∧ Function.RightInverse g f<VAR>x : X<VAR>g : Y → X<VAR>hgc : ContinuousAt g (f x)<VAR>hgx : g (f x) = x<VAR>hgf : Function.RightInverse g f<GOAL>𝓝 (f x) = map f (map g (𝓝 (f x)))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>mx : M<VAR>sx : ↥S<VAR>my : M<VAR>sy : ↥S<VAR>mz : M<VAR>sz : ↥S<GOAL>mk mx sx + mk my sy + mk mz sz = mk mx sx + (mk my sy + mk mz sz)
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>mx : M<VAR>sx : ↥S<VAR>my : M<VAR>sy : ↥S<VAR>mz : M<VAR>sz : ↥S<GOAL>mk (sz • sy • mx + sz • sx • my + (sx * sy) • mz) (sx * sy * sz) = mk ((sy * sz) • mx + (sx • sz • my + sx • sy • mz)) (sx * (sy * sz))
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>mx : M<VAR>sx : ↥S<VAR>my : M<VAR>sy : ↥S<VAR>mz : M<VAR>sz : ↥S<GOAL>1 • (sx * (sy * sz)) • (sz • sy • mx + sz • sx • my + (sx * sy) • mz) = 1 • (sx * sy * sz) • ((sy * sz) • mx + (sx • sz • my + sx • sy • mz))
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>mx : M<VAR>sx : ↥S<VAR>my : M<VAR>sy : ↥S<VAR>mz : M<VAR>sz : ↥S<GOAL>(sx * (sy * sz)) • (sz • sy • mx + sz • sx • my + (sx * sy) • mz) = (sx * sy * sz) • ((sy * sz) • mx + (sx • sz • my + sx • sy • mz))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>g : X ⟶ Y<VAR>inst✝ : IsIso g<VAR>f : Y ⟶ X<VAR>h : f ≫ g = 𝟙 Y<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>g : X ⟶ Y<VAR>inst✝ : IsIso g<VAR>f : Y ⟶ X<VAR>h : f ≫ g = 𝟙 Y<GOAL>IsIso (inv g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice α<VAR>S : Set ↥L<GOAL>↑(sInf S) = ⨅ N ∈ S, ↑N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r r' : α → α → Prop<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : PartialOrder γ<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>f : β → β<VAR>hf : StrictMono f<GOAL>∀ (n : β), n ≤ f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r r' : α → α → Prop<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : PartialOrder γ<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>f : β → β<VAR>hf : StrictMono f<VAR>h₁ : ∃ n, f n < n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r r' : α → α → Prop<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : PartialOrder γ<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>f : β → β<VAR>hf : StrictMono f<VAR>h₁ : ∃ n, f n < n<VAR>h₂ : h.min (fun x => Preorder.toLT.1 (f x) x) h₁ ∈ fun x => Preorder.toLT.1 (f x) x<GOAL>False
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>h : 1 - y ≠ 0<GOAL>x ^ (1 - y) = x / x ^ y
<VAR>θ : ↑I<GOAL>1 * (1 + ↑θ) ≤ 2 * ↑1
<VAR>θ : ↑I<GOAL>↑θ + 1 ≤ 1 + 1
<VAR>θ : ↑I<GOAL>↑θ ≤ 1
<VAR>α : Type u_1<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : InvolutiveStar α<GOAL>a⋆ ∈ s⋆ ↔ a ∈ s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrder R<VAR>a b c : R<VAR>ha : a ≠ c<VAR>hb : b ≠ c<GOAL>min a b ≠ c
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrder R<VAR>a b c : R<VAR>ha : a ≠ c<VAR>hb : b ≠ c<GOAL>(if a ≤ b then a else b) ≠ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → α → Prop<VAR>a b c d x y : α<GOAL>ReflGen (TransGen r) x y ↔ ReflTransGen r x y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(freeOn E).Basis' I X ↔ I = X ∩ E
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m✝ n : ℕ∞<VAR>p✝ : E → FormalMultilinearSeries 𝕜 E F<VAR>g : F →L[𝕜] G<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFTaylorSeriesUpToOn (↑m) f p u<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (⇑g ∘ f) p u
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>M : Matrix V V α<VAR>v w : V<GOAL>(adjMatrix α G * M) v w = ∑ u ∈ G.neighborFinset v, M u w
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>t : ℝ<VAR>ht : t ∈ Icc v.tMin v.tMax<GOAL>↑(v.proj t) = t
<VAR>α : Type u_1<VAR>f g h : Perm α<GOAL>f.Disjoint g → g.Disjoint f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>x : α<VAR>s t : Set α<VAR>hs : s ∈ 𝓝[t] x<VAR>t' : Set α<GOAL>s \ t' ∈ 𝓝[t \ t'] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>x : α<VAR>s t : Set α<VAR>hs : s ∈ 𝓝[t] x<VAR>t' : Set α<GOAL>s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : NonUnitalNonAssocSemiring A<VAR>inst✝ : DistribMulAction R A<VAR>r : R<VAR>a : A<GOAL>r • a + 0 • 0 + 0 * a = r • a
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<VAR>x✝ : a₂ ≡ b₂ [PMOD p]<VAR>m : ℤ<VAR>hm : b₂ - a₂ = m • p<GOAL>(∃ b, b₁ - b₂ - (a₁ - a₂) = (Equiv.subRight m).symm.symm b • p) ↔ a₁ ≡ b₁ [PMOD p]
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L<VAR>a a' : ℤ<VAR>h : n + a = a'<GOAL>(homologyFunctor C (up ℤ) 0).shiftMap ((quotient C (up ℤ)).map f ≫ ((quotient C (up ℤ)).commShiftIso n).hom.app L) a a' h = (homologyFunctorFactors C (up ℤ) a).hom.app K ≫ (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap f a a' h ≫ (homologyFunctorFactors C (up ℤ) a').inv.app L
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<GOAL>f.mk' x 1 = f.toMap x
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x : M<GOAL>f.toMap x * ↑1⁻¹ = f.toMap x
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s₁ s₂ s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>h₁ : IndepSets s₁ s' κ μ<VAR>h₂ : IndepSets s₂ s' κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ s₁ ∪ s₂<VAR>ht2 : t2 ∈ s'<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s₁ s₂ s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>h₁ : IndepSets s₁ s' κ μ<VAR>h₂ : IndepSets s₂ s' κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ s₁ ∪ s₂<VAR>ht2 : t2 ∈ s'<VAR>ht1₁ : t1 ∈ s₁<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s₁ s₂ s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>h₁ : IndepSets s₁ s' κ μ<VAR>h₂ : IndepSets s₂ s' κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ s₁ ∪ s₂<VAR>ht2 : t2 ∈ s'<VAR>ht1₂ : t1 ∈ s₂<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2