ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>a b : α<VAR>ha : Nonempty (β a)<VAR>he : IsEmpty (β b)<VAR>hf : Finite (WType β)<VAR>hba : b ≠ a<GOAL>False
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>a b : α<VAR>ha : Nonempty (β a)<VAR>he : IsEmpty (β b)<VAR>hf : Finite (WType β)<VAR>hba : b ≠ a<GOAL>Function.Injective fun n => let_fun this := Nat.recOn n (mk b he.elim') fun x ih => mk a fun x => ih; this
<VAR>G : Type u_1<VAR>M : Type u<VAR>one₁ : M<VAR>mul₁ : M → M → M<VAR>one_mul₁ : ∀ (a : M), 1 * a = a<VAR>mul_one₁ : ∀ (a : M), a * 1 = a<VAR>one₂ : M<VAR>one_mul₂ : ∀ (a : M), 1 * a = a<VAR>mul_one₂ : ∀ (a : M), a * 1 = a<GOAL>one₁ = one₂
<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>map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i k₀ : ι<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>hk₀' : ∀ (l : ι), ¬c.Rel l k₀<VAR>h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<GOAL>(nullHomotopicMap fun i j => dite (c.Rel j i) (h i j) fun x => 0).f k₀ = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n : ℕ<VAR>hpos : 0 < n<GOAL>Irreducible (cyclotomic n ℚ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n : ℕ<VAR>hpos : 0 < n<GOAL>Irreducible (map (Int.castRingHom ℚ) (cyclotomic n ℤ))
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝ : Semiring T<VAR>s : A → A → Prop<GOAL>↑(mkAlgHom S s) = mkRingHom s
<VAR>R : Type uR<VAR>inst✝⁴ : Semiring R<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>r : R → R → Prop<VAR>inst✝ : Semiring T<VAR>s : A → A → Prop<GOAL>↑{ toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } = { toFun := fun x => { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α →ₛ E<VAR>hfi : Integrable (↑f) μ<GOAL>∫ (x : α), ↑f x ∂μ = ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α →ₛ E<VAR>hfi : Integrable (↑f) μ<GOAL>setToSimpleFunc (weightedSMul μ) f = integral μ f
<VAR>α✝ : Type u_1<VAR>G✝ : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : Inv G✝<VAR>inst✝⁴ : MeasurableSpace G✝<VAR>inst✝³ : MeasurableInv G✝<VAR>m : MeasurableSpace α<VAR>f✝ : α → G✝<VAR>μ : Measure α<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : MeasurableInv G<VAR>f : α → G<VAR>h : Measurable fun x => (f x)⁻¹<GOAL>Measurable f
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>1 - ↑p ^ (-s) ≠ 0
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>H : 1 = ↑p ^ (-s)<GOAL>False
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>H : 1 = ↑p ^ (-s)<VAR>this : ‖↑↑⟨p, hp⟩ ^ (-s)‖ ≤ 1 / 2<GOAL>False
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>H : 1 = ↑p ^ (-s)<VAR>this : ‖↑p ^ (-s)‖ ≤ 1 / 2<GOAL>False
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>H : 1 = ↑p ^ (-s)<VAR>this : 1 ≤ 1 / 2<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<GOAL>∫ (x : E), w D x ∂μ = 1
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<GOAL>((∫ (x : E), u x ∂μ) * |D| ^ finrank ℝ E)⁻¹ • ∫ (a : E), u (D⁻¹ • a) ∂μ = 1
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>Dpos : 0 < D<GOAL>(D ^ finrank ℝ E * ∫ (x : E), u x ∂μ)⁻¹ • D ^ finrank ℝ E • ∫ (x : E), u x ∂μ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X✝ Y✝ : Type ?u.20146<VAR>f : X✝ ⟶ Y✝<VAR>a✝ : ((typeToPartialFun ⋙ partialFunToPointed).obj X✝).X<VAR>a : typeToPartialFun.obj X✝<GOAL>((typeToPartialFun ⋙ partialFunToPointed).map f ≫ ((fun X => { hom := { toFun := id, map_point := ⋯ }, inv := { toFun := id, map_point := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }) Y✝).hom).toFun (some a) = (((fun X => { hom := { toFun := id, map_point := ⋯ }, inv := { toFun := id, map_point := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }) X✝).hom ≫ typeToPointed.map f).toFun (some a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X✝ Y✝ : Type ?u.20146<VAR>f : X✝ ⟶ Y✝<VAR>a✝ : ((typeToPartialFun ⋙ partialFunToPointed).obj X✝).X<VAR>a : typeToPartialFun.obj X✝<GOAL>((typeToPartialFun ⋙ partialFunToPointed).map f ≫ ((fun X => { hom := { toFun := id, map_point := ⋯ }, inv := { toFun := id, map_point := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }) Y✝).hom).toFun (some a) = (Part.some (f a)).toOption
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>inst✝ : NoZeroDivisors R<VAR>hp : ¬p = 0<VAR>hq : ¬q = 0<GOAL>(p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>inst✝ : NoZeroDivisors R<VAR>hp : ¬p = 0<VAR>hq : ¬q = 0<GOAL>p.leadingCoeff * q.leadingCoeff ≠ 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>K : ℕ → Set X<VAR>hc : ∀ (n : ℕ), IsCompact (K n)<VAR>huniv : ⋃ n, K n = s<GOAL>IsLindelof (⋃ n, K n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>K : ℕ → Set X<VAR>hc : ∀ (n : ℕ), IsCompact (K n)<VAR>huniv : ⋃ n, K n = s<VAR>hl : ∀ (n : ℕ), IsLindelof (K n)<GOAL>IsLindelof (⋃ n, K n)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>S : Set X<GOAL>DiscreteTopology ↑S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ a * b⁻¹ ∈ ker f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>a b : G<GOAL>f a = f b ↔ f (a * b⁻¹) = 1
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ i i' : ι<VAR>b : β i<VAR>h : i ≠ i'<GOAL>(single i b) i' = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a ≤ b<VAR>hfab : f a ≤ f b<VAR>hf_c : ContinuousOn f (Icc a b)<VAR>hf_i : InjOn f (Icc a b)<VAR>this : CompleteLinearOrder ↑(Icc a b) := Icc.completeLinearOrder hab<VAR>g : ↑(Icc a b) → δ := (Icc a b).restrict f<VAR>hgab : g ⊥ ≤ g ⊤<GOAL>StrictMono g
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPushout f.op g.op<GOAL>(PushoutCocone.unop (colimit.cocone (span f.op g.op))).π.app WalkingCospan.right = (pushout.inr f.op g.op).unop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ≃ β<VAR>B : Set β<GOAL>(M.mapEquiv f).Base B ↔ M.Base (⇑f.symm '' B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α ≃ β<VAR>B : Set β<GOAL>(∃ B₀, M.Base B₀ ∧ B = ⇑f '' B₀) ↔ M.Base (⇑f.symm '' B)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : PresheafedSpace CommRingCat<VAR>Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝.toPresheafedSpace<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : AlgebraicGeometry.IsOpenImmersion f<GOAL>toScheme Y f.val = X
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : PresheafedSpace CommRingCat<VAR>Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝.toPresheafedSpace<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : AlgebraicGeometry.IsOpenImmersion f<GOAL>(toScheme Y f.val).toLocallyRingedSpace = X.toLocallyRingedSpace
<VAR>α✝ : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Monoid α✝<VAR>inst✝⁶ : DistribMulAction α✝ M<VAR>inst✝⁵ : SMulCommClass α✝ R M<VAR>α : Type u_4<VAR>inst✝⁴ : Semiring α<VAR>inst✝³ : Module α R<VAR>inst✝² : Module α M<VAR>inst✝¹ : SMulCommClass α R M<VAR>inst✝ : IsScalarTower α R M<VAR>a : α<VAR>S : Submodule R M<VAR>x : M<VAR>hx : x ∈ ↑S<GOAL>(DistribMulAction.toLinearMap R M a) x ∈ S
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>τ (f ^ (n + 1)) = ↑(n + 1) * τ f
<VAR>R L K : Type u<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsAlgClosed K<VAR>ι : Type u<VAR>v : ι → K<VAR>hv✝ hv : IsTranscendenceBasis R v<GOAL>max #↥(Algebra.adjoin R (Set.range v)) ℵ₀ = max #(MvPolynomial ι R) ℵ₀
<VAR>R L K : Type u<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsAlgClosed K<VAR>ι : Type u<VAR>v : ι → K<VAR>hv✝ hv : IsTranscendenceBasis R v<GOAL>max (max (max #R #ι) ℵ₀) ℵ₀ = max (max #R #ι) ℵ₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s : Set α<VAR>hxy : x ≠ y<GOAL>{x, y}.infsep ≤ (edist x y ⊓ edist y x).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s : Set α<VAR>hxy : x ≠ y<GOAL>(edist x y ⊓ edist y x).toReal ≤ (edist x y ⊓ edist y x).toReal
<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>U U' : Y.Opens<VAR>V V' : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>i : op V ⟶ op V'<GOAL>f.appLE U V e ≫ X.presheaf.map i = f.appLE U V' ⋯
<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>U U' : Y.Opens<VAR>V V' : X.Opens<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>i : op V ⟶ op V'<GOAL>f.app U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = f.appLE U V' ⋯
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arctan (dist p₃ p₂ / dist p₁ p₂))
<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>s : ↥S<VAR>p : LocalizedModule S M<VAR>m : M<VAR>t : ↥S<GOAL>((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) ((divBy s) (mk m t)) = mk m t
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>Ideal.span (Set.range fun x => C r * X () - 1) = (Generators.localizationAway r).ker
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>Ideal.span {C r * X () - 1} = (Generators.localizationAway r).ker
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>i j k : n<VAR>M : Matrix n n α<VAR>hM : Commute (stdBasisMatrix i j 1) M<VAR>hkj : k ≠ j<GOAL>M j k = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>i j k : n<VAR>M : Matrix n n α<VAR>hM : Commute (stdBasisMatrix i j 1) M<VAR>hkj : k ≠ j<VAR>this : (stdBasisMatrix i j 1 * M) i k = (M * stdBasisMatrix i j 1) i k<GOAL>M j k = 0
<VAR>α : Type u_1<VAR>I B✝ X E : Set α<VAR>Base : Set α → Prop<VAR>base_exchange : ExchangeProperty Base<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<VAR>B : Set α<VAR>h : Base B ∧ B.Finite<GOAL>∃ B, Base B
<VAR>α : Type u_1<VAR>I B✝ X E : Set α<VAR>Base : Set α → Prop<VAR>base_exchange : ExchangeProperty Base<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<VAR>B : Set α<VAR>hB : Base B<VAR>hfin : B.Finite<GOAL>∀ X ⊆ E, ExistsMaximalSubsetProperty (fun x => ∃ B, Base B ∧ x ⊆ B) X
<VAR>α : Type u_1<VAR>I B✝ X✝ E : Set α<VAR>Base : Set α → Prop<VAR>base_exchange : ExchangeProperty Base<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<VAR>B : Set α<VAR>hB : Base B<VAR>hfin : B.Finite<VAR>X : Set α<VAR>x✝¹ : X ⊆ E<VAR>Y : Set α<VAR>x✝ : ∃ B, Base B ∧ Y ⊆ B<VAR>B' : Set α<VAR>hB' : Base B'<VAR>hYB' : Y ⊆ B'<GOAL>Y.encard ≤ ↑B.ncard
<VAR>α : Type u_1<VAR>I B✝ X✝ E : Set α<VAR>Base : Set α → Prop<VAR>base_exchange : ExchangeProperty Base<VAR>subset_ground : ∀ (B : Set α), Base B → B ⊆ E<VAR>B : Set α<VAR>hB : Base B<VAR>hfin : B.Finite<VAR>X : Set α<VAR>x✝¹ : X ⊆ E<VAR>Y : Set α<VAR>x✝ : ∃ B, Base B ∧ Y ⊆ B<VAR>B' : Set α<VAR>hB' : Base B'<VAR>hYB' : Y ⊆ B'<GOAL>Y.encard ≤ B'.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>g : β → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : β), g c ∂κ.fst a = ∫⁻ (bc : β × γ), g bc.1 ∂κ a
<VAR>α : Type u_1<VAR>inst✝ : SemilatticeSup α<VAR>f : ℕ → α<VAR>p : α → Prop<VAR>hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b<VAR>n : ℕ<GOAL>p ((partialSups f) (n + 1)) ↔ ∀ k ≤ n + 1, p (f k)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<GOAL>Continuous f ↔ ∀ (i : ι), Continuous fun a => f a i
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>n : ℕ<VAR>x : ℤ_[p]<VAR>a b : ℤ<VAR>ha : x - ↑a ∈ Ideal.span {↑p ^ n}<VAR>hb : x - ↑b ∈ Ideal.span {↑p ^ n}<GOAL>↑a = ↑b
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>n : ℕ<VAR>x : ℤ_[p]<VAR>a b : ℤ<VAR>ha : ↑p ^ n ∣ x - ↑a<VAR>hb : ↑p ^ n ∣ x - ↑b<GOAL>↑a = ↑b
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>n : ℕ<VAR>x : ℤ_[p]<VAR>a b : ℤ<VAR>ha : ↑p ^ n ∣ x - ↑a<VAR>hb : ↑p ^ n ∣ x - ↑b<GOAL>↑p ^ n ∣ a - b
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>n : ℕ<VAR>x : ℤ_[p]<VAR>a b : ℤ<VAR>ha : ↑p ^ n ∣ ↑a - x<VAR>hb : ↑p ^ n ∣ x - ↑b<GOAL>↑p ^ n ∣ a - b
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>n : ℕ<VAR>x : ℤ_[p]<VAR>a b : ℤ<VAR>ha : ↑p ^ n ∣ ↑a - x<VAR>hb : ↑p ^ n ∣ x - ↑b<VAR>this : ↑p ^ n ∣ ↑a - x + (x - ↑b)<GOAL>↑p ^ n ∣ a - b
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h : separableClosure F E = ⊥<VAR>x : E<VAR>hs : IsSeparable F x<GOAL>x ∈ (algebraMap F E).range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : Finite a b<GOAL>∃ c, b = a ^ (multiplicity a b).get hfin * c ∧ ¬a ∣ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : Finite a b<VAR>c : α<VAR>hc : b = a ^ (multiplicity a b).get hfin * c<GOAL>∃ c, b = a ^ (multiplicity a b).get hfin * c ∧ ¬a ∣ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : Finite a b<VAR>c : α<VAR>hc : b = a ^ (multiplicity a b).get hfin * c<VAR>k : α<VAR>hk : c = a * k<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : Finite a b<VAR>c k : α<VAR>hc : b = a ^ ((multiplicity a b).get hfin + 1) * k<VAR>hk : c = a * k<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : Finite a b<VAR>c k : α<VAR>hc : b = a ^ ((multiplicity a b).get hfin + 1) * k<VAR>hk : c = a * k<VAR>h₁ : a ^ ((multiplicity a b).get hfin + 1) ∣ b<GOAL>False
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)₀<GOAL>φ.realContinuousMapZeroOfNNReal ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f) = φ f
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)₀<GOAL>φ ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal - φ (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = φ f
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)₀<GOAL>φ ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = φ f
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)₀<GOAL>φ (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ }.comp f).toNNReal = φ 0
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>f : C(X, ℝ≥0)₀<GOAL>φ f - φ 0 = φ f
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<GOAL>x ∈ J
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<GOAL>Submodule.colon J (span {x}) = ⊤
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<GOAL>¬∃ M, M.IsMaximal ∧ Submodule.colon J (span {x}) ≤ M
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>le : Submodule.colon J (span {x}) ≤ P<GOAL>False
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) I ≤ map (algebraMap R (Localization.AtPrime P)) J<VAR>x : R<VAR>hx : x ∈ I<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>le : Submodule.colon J (span {x}) ≤ P<VAR>a : R<VAR>ha : a ∈ J<VAR>s : R<VAR>hs : s ∈ P.primeCompl<VAR>eq : (algebraMap R (Localization.AtPrime P)) x * (algebraMap R (Localization.AtPrime P)) ↑(⟨a, ha⟩, ⟨s, hs⟩).2 = (algebraMap R (Localization.AtPrime P)) ↑(⟨a, ha⟩, ⟨s, hs⟩).1<GOAL>False