ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<VAR>H : G.Subgraph<VAR>c : H.coe.ConnectedComponent<VAR>hw : w ∈ H.verts<VAR>hadj : H.Adj v w<VAR>w✝ : ↑H.verts<VAR>h : w✝ ∈ ↑c ∧ ↑w✝ = v<GOAL>w ∈ Subtype.val '' ↑c
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<VAR>H : G.Subgraph<VAR>c : H.coe.ConnectedComponent<VAR>hw : w ∈ H.verts<VAR>hadj : H.Adj v w<VAR>w✝ : ↑H.verts<VAR>h : w✝ ∈ ↑c ∧ ↑w✝ = v<GOAL>⟨w, hw⟩ ∈ ↑c ∧ ↑⟨w, hw⟩ = w
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<VAR>H : G.Subgraph<VAR>c : H.coe.ConnectedComponent<VAR>hw : w ∈ H.verts<VAR>hadj : H.Adj v w<VAR>w✝ : ↑H.verts<VAR>h : w✝ ∈ ↑c ∧ ↑w✝ = v<GOAL>⟨w, hw⟩ ∈ ↑(H.coe.connectedComponentMk w✝) ∧ ↑⟨w, hw⟩ = w
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<GOAL>(thickenedIndicator δ_pos E) x ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<GOAL>(ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hdiff : DifferentiableOn ℝ f (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0<GOAL>∀ x ∈ Icc a b, f x = f a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hdiff : DifferentiableOn ℝ f (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0<VAR>H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0<GOAL>∀ x ∈ Icc a b, f x = f 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>T : Type u_3<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝¹ : LocalRing S<VAR>inst✝ : IsLocalRingHom f<GOAL>f.SurjectiveOnStalks ↔ Function.Surjective ⇑f
<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>T : Type u_3<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝¹ : LocalRing S<VAR>inst✝ : IsLocalRingHom f<VAR>H : f.SurjectiveOnStalks<VAR>x : S<GOAL>∃ a, f a = 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>T : Type u_3<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝¹ : LocalRing S<VAR>inst✝ : IsLocalRingHom f<VAR>H : f.SurjectiveOnStalks<VAR>x : S<VAR>y r : R<VAR>c : S<VAR>hc : c ∉ LocalRing.maximalIdeal S<VAR>hr : f r ∉ LocalRing.maximalIdeal S<VAR>e : c * f r * x = c * f y<GOAL>∃ a, f a = 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>T : Type u_3<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝¹ : LocalRing S<VAR>inst✝ : IsLocalRingHom f<VAR>H : f.SurjectiveOnStalks<VAR>x : S<VAR>y r : R<VAR>c : S<VAR>e : c * f r * x = c * f y<VAR>hc : IsUnit c<VAR>hr : IsUnit (f r)<GOAL>∃ a, f a = 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>T : Type u_3<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝¹ : LocalRing S<VAR>inst✝ : IsLocalRingHom f<VAR>H : f.SurjectiveOnStalks<VAR>x : S<VAR>y r : R<VAR>c : S<VAR>e : c * f r * x = c * f y<VAR>hc : IsUnit c<VAR>hr : IsUnit (f r)<GOAL>f (↑⋯.unit⁻¹ * y) = 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>T : Type u_3<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝¹ : LocalRing S<VAR>inst✝ : IsLocalRingHom f<VAR>H : f.SurjectiveOnStalks<VAR>x : S<VAR>y r : R<VAR>c : S<VAR>e : c * f r * x = c * f y<VAR>hc : IsUnit c<VAR>hr : IsUnit (f r)<GOAL>(fun x => f r * x) (f (↑⋯.unit⁻¹ * y)) = (fun x => f r * x) 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>T : Type u_3<VAR>inst✝⁵ : CommRing T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>inst✝¹ : LocalRing S<VAR>inst✝ : IsLocalRingHom f<VAR>H : f.SurjectiveOnStalks<VAR>x : S<VAR>y r : R<VAR>c : S<VAR>e : c * f r * x = c * f y<VAR>hc : IsUnit c<VAR>hr : IsUnit (f r)<GOAL>(fun x => c * x) ((fun x => f r * x) (f (↑⋯.unit⁻¹ * y))) = (fun x => c * x) ((fun x => f r * x) x)
<VAR>a b : ℝ<VAR>f : C(↑(Set.Icc a b), ℝ)<GOAL>f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure
<VAR>a b : ℝ<VAR>f : C(↑(Set.Icc a b), ℝ)<GOAL>f ∈ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>f : α → PMF β<VAR>g : β → PMF γ<VAR>b : β<GOAL>b ∈ (p.bind f).support ↔ ∃ a ∈ p.support, b ∈ (f a).support
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>P : R[X]<VAR>r : R<GOAL>eval r ((expand R p) P) = eval (r ^ p) P
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>P : R[X]<VAR>r : R<VAR>f g : R[X]<VAR>hf : eval r ((expand R p) f) = eval (r ^ p) f<VAR>hg : eval r ((expand R p) g) = eval (r ^ p) g<GOAL>eval r ((expand R p) (f + g)) = eval (r ^ p) (f + g)
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝⁹ : MeasurableSpace M<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : Monoid M<VAR>inst✝⁶ : MulAction M β<VAR>inst✝⁵ : MeasurableSMul M β<VAR>inst✝⁴ : MeasurableSpace α<VAR>f : α → β<VAR>μ : Measure α<VAR>G : Type u_5<VAR>inst✝³ : Group G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : MulAction G β<VAR>inst✝ : MeasurableSMul G β<VAR>c : G<VAR>h : Measurable fun x => c • f x<GOAL>Measurable f
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>h : I ⊔ J = ⊤<GOAL>I * K ⊔ J = K ⊔ J
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>h : J ⊔ I = ⊤<GOAL>I * K ⊔ J = K ⊔ J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>x : β<VAR>f : Fin n → β<GOAL>∏ i : Fin n.succ, cons x f i = x * ∏ i : Fin n, f i
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<GOAL>(λ_ ((free R).obj X)).hom = (ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<GOAL>(TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ (λ_ ((free R).obj X)).hom = (TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<GOAL>((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ (λ_ ((free R).obj X)).hom) 1 = ((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom)) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<GOAL>∀ (a : X), ((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ (λ_ ((free R).obj X)).hom) 1 ∘ₗ Finsupp.lsingle a = ((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom)) 1 ∘ₗ Finsupp.lsingle a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x : X<GOAL>((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ (λ_ ((free R).obj X)).hom) 1 ∘ₗ Finsupp.lsingle x = ((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom)) 1 ∘ₗ Finsupp.lsingle x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x : X<GOAL>(((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ (λ_ ((free R).obj X)).hom) 1 ∘ₗ Finsupp.lsingle x) 1 = (((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom)) 1 ∘ₗ Finsupp.lsingle x) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x : X<GOAL>∀ (a : X), ((((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ (λ_ ((free R).obj X)).hom) 1 ∘ₗ Finsupp.lsingle x) 1) a = ((((TensorProduct.mk R ↑(𝟙_ (ModuleCat R)) ↑((free R).obj X)).compr₂ ((ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom)) 1 ∘ₗ Finsupp.lsingle x) 1) a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X : Type u<VAR>x x' : X<VAR>q : X →₀ R := (λ_ (of R (X →₀ R))).hom (1 ⊗ₜ[R] Finsupp.single x 1)<GOAL>q x' = (Finsupp.mapDomain (λ_ X).hom ((finsuppTensorFinsupp' R (𝟙_ (Type u)) X) (Finsupp.single PUnit.unit 1 ⊗ₜ[R] Finsupp.single x 1))) x'
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>s.points i = (affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>s.pointsWithCircumcenter (pointIndex i) = (affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>(affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i) = s.pointsWithCircumcenter (pointIndex i)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>∀ i2 ∈ univ, i2 ≠ pointIndex i → pointWeightsWithCircumcenter i i2 = 0
<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>hf : OpenEmbedding f<VAR>l : Filter Z<VAR>x : X<GOAL>Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l
<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>hf : OpenEmbedding f<VAR>l : Filter Z<VAR>x : X<GOAL>map g (𝓝 (f x)) ≤ l ↔ Tendsto g (𝓝 (f x)) l
<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✝ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<GOAL>↑(s.sup' H f) = s.sup (WithBot.some ∘ f)
<VAR>k : ℕ<VAR>a : ℝ<VAR>ha : a ≤ 1<VAR>t : ℝ<VAR>n : ℕ<VAR>this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))<GOAL>f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>α' : TypeVec.{u_2} (n + 1)<VAR>f f' : α.drop ⟹ α'.drop<VAR>g g' : α.last → α'.last<VAR>H : splitFun f g = splitFun f' g'<GOAL>f = f' ∧ g = g'
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} (n + 1)<VAR>α' : TypeVec.{u_2} (n + 1)<VAR>f f' : α.drop ⟹ α'.drop<VAR>g g' : α.last → α'.last<VAR>H : splitFun f g = splitFun f' g'<GOAL>dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'
<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>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : X → ℝ≥0<VAR>f_meas : Measurable f<VAR>g : X → E<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>(∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>a b : M<VAR>inst✝ : Unique Mˣ<VAR>x : M<VAR>x✝ : IsUnit x<VAR>u : Mˣ<VAR>hu : ↑u = x<GOAL>x = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : a ≤ b<VAR>hb : 0 ≤ b<GOAL>a * b⁻¹ ≤ 1
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁴ : CommSemiring S<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : NonUnitalSemiring A<VAR>inst✝¹¹ : Module R A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁸ : Semiring B<VAR>inst✝⁷ : Algebra S B<VAR>inst✝⁶ : Algebra S R<VAR>inst✝⁵ : DistribMulAction S A<VAR>inst✝⁴ : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝³ : Semiring C<VAR>inst✝² : Algebra R C<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F (Unitization R A) B<VAR>inst✝ : AlgHomClass F S (Unitization R A) B<VAR>φ ψ : F<VAR>h : ∀ (a : A), φ ↑a = ψ ↑a<VAR>h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)<GOAL>φ = ψ
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁴ : CommSemiring S<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : NonUnitalSemiring A<VAR>inst✝¹¹ : Module R A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁸ : Semiring B<VAR>inst✝⁷ : Algebra S B<VAR>inst✝⁶ : Algebra S R<VAR>inst✝⁵ : DistribMulAction S A<VAR>inst✝⁴ : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝³ : Semiring C<VAR>inst✝² : Algebra R C<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F (Unitization R A) B<VAR>inst✝ : AlgHomClass F S (Unitization R A) B<VAR>φ ψ : F<VAR>h : ∀ (a : A), φ ↑a = ψ ↑a<VAR>h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)<VAR>x : Unitization R A<GOAL>φ x = ψ x
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁴ : CommSemiring S<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : NonUnitalSemiring A<VAR>inst✝¹¹ : Module R A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁸ : Semiring B<VAR>inst✝⁷ : Algebra S B<VAR>inst✝⁶ : Algebra S R<VAR>inst✝⁵ : DistribMulAction S A<VAR>inst✝⁴ : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝³ : Semiring C<VAR>inst✝² : Algebra R C<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F (Unitization R A) B<VAR>inst✝ : AlgHomClass F S (Unitization R A) B<VAR>φ ψ : F<VAR>h : ∀ (a : A), φ ↑a = ψ ↑a<VAR>h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)<VAR>r✝ : R<VAR>a✝ : A<GOAL>φ (inl r✝ + ↑a✝) = ψ (inl r✝ + ↑a✝)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : AddMonoid ι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>a : ⨁ (i : ι), ↥(𝒜 i)<VAR>i : ι<GOAL>(proj 𝒜 i) ((decompose 𝒜).symm a) = (decompose 𝒜).symm ((of (fun i => ↥(𝒜 i)) i) (a i))
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>hr₀ : 0 < r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>hr₀ : 0 < r<VAR>A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>hr₀ : 0 < r<VAR>A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>hr₀ : 0 < r<VAR>A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>C : {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s \ {x}] x ⊔ 𝓝[{x}] x<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>hr₀ : 0 < r<VAR>A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>C : {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧ {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>hr₀ : 0 < r<VAR>A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>C : {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧ {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x<GOAL>∀ (a : ℝ), ‖(a - x)⁻¹ • (f a - f x)‖ ∈ Iio r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>hr₀ : 0 < r<VAR>A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r<VAR>C : {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧ {x_1 | (fun z => ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x<GOAL>∀ (a : ℝ), ‖a - x‖⁻¹ * ‖f a - f x‖ < r → ‖a - x‖⁻¹ * ‖f a - f x‖ < r
<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>inst✝ : HasPullbacks C<VAR>x : Subobject X<GOAL>(pullback (𝟙 X)).obj x = x
<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>inst✝ : HasPullbacks C<VAR>f : MonoOver X<GOAL>(pullback (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>hd : HasDerivWithinAt d d' s x<VAR>hx : d x ≠ 0<GOAL>HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>hd : HasDerivWithinAt d d' s x<VAR>hx : d x ≠ 0<GOAL>(fun y => c y / d y) = fun y => c y * ((fun y => y⁻¹) ∘ d) y
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>hd : HasDerivWithinAt d d' s x<VAR>hx : d x ≠ 0<GOAL>(c' * d x - c x * d') / d x ^ 2 = c' * ((fun y => y⁻¹) ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')
<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>s : ℕ → Set α<VAR>t : Set α<VAR>h : ∀ (n : ℕ), s n =ᶠ[ae μ] t<GOAL>limsup s atTop =ᶠ[ae μ] t
<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>s : ℕ → Set α<VAR>t : Set α<VAR>h : ∀ (n : ℕ), μ (s n \ t) = 0 ∧ μ (t \ s n) = 0<GOAL>μ (limsup s atTop \ t) = 0 ∧ μ (t \ limsup s atTop) = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n✝ n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<VAR>inst✝ : CharZero K<GOAL>cyclotomic n ℤ = minpoly ℤ μ
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n✝ n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<VAR>inst✝ : CharZero K<GOAL>(cyclotomic n ℤ).natDegree ≤ (minpoly ℤ μ).natDegree
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h : c ≤ b<GOAL>a - c ≤ b - c ↔ a ≤ b
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<GOAL>(if h : Δ = Δ then eqToHom ⋯ else if h : Isδ₀ (𝟙 Δ) then K.d Δ.len Δ.len else 0) = 𝟙 (K.X Δ.len)
<VAR>k : Type u_1<VAR>inst✝ : Field k<VAR>σ : Type u_2<VAR>I : Ideal (MvPolynomial σ k)<VAR>p : MvPolynomial σ k<VAR>hp : p ∈ I.radical<VAR>x : σ → k<VAR>hx : x ∈ zeroLocus I<GOAL>(eval x) p = 0
<VAR>k : Type u_1<VAR>inst✝ : Field k<VAR>σ : Type u_2<VAR>I : Ideal (MvPolynomial σ k)<VAR>p : MvPolynomial σ k<VAR>hp : p ∈ I.radical<VAR>x : σ → k<VAR>hx : x ∈ zeroLocus I<GOAL>p ∈ vanishingIdeal {x}
<VAR>k : Type u_1<VAR>inst✝ : Field k<VAR>σ : Type u_2<VAR>I : Ideal (MvPolynomial σ k)<VAR>p : MvPolynomial σ k<VAR>hp : p ∈ sInf {J | I ≤ J ∧ J.IsPrime}<VAR>x : σ → k<VAR>hx : x ∈ zeroLocus I<GOAL>p ∈ vanishingIdeal {x}
<VAR>x y a b c : ℝ<GOAL>c + a < c + b ↔ a < b
<VAR>x y b c : ℝ<VAR>y✝ : CauSeq ℚ abs<GOAL>c + mk y✝ < c + b ↔ mk y✝ < b
<VAR>x y c : ℝ<VAR>y✝¹ y✝ : CauSeq ℚ abs<GOAL>c + mk y✝¹ < c + mk y✝ ↔ mk y✝¹ < mk y✝
<VAR>x y : ℝ<VAR>y✝² y✝¹ y✝ : CauSeq ℚ abs<GOAL>mk y✝ + mk y✝² < mk y✝ + mk y✝¹ ↔ mk y✝² < mk y✝¹
<VAR>x y : ℝ<VAR>y✝² y✝¹ y✝ : CauSeq ℚ abs<GOAL>y✝ + y✝² < y✝ + y✝¹ ↔ y✝² < y✝¹
<VAR>x y : ℝ<VAR>y✝² y✝¹ y✝ : CauSeq ℚ abs<GOAL>(y✝ + y✝¹ - (y✝ + y✝²)).Pos ↔ (y✝¹ - y✝²).Pos
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S S' : C ⥤ D<VAR>f : CostructuredArrow S T<GOAL>(map (𝟙 T)).obj f = f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S S' : C ⥤ D<VAR>f : CostructuredArrow S T<GOAL>(map (𝟙 T)).obj (mk f.hom) = mk f.hom
<VAR>x : ℂ<GOAL>HasStrictDerivAt sin (cos x) x