ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>CommRing K<GOAL>RatFunc.zero = { toFractionRing := 0 }
<VAR>K : Type u<VAR>CommRing K<GOAL>{ toFractionRing := 0 } = 0
<VAR>K : Type u_1<VAR>CommRing K<GOAL>∀ (x x_1 : RatFunc K), x.add x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p + q }
<VAR>K : Type u<VAR>CommRing K<VAR>p q : FractionRing K[X]<GOAL>{ toFractionRing := p + q } = { toFractionRing := p } + { toFractionRing := q }
<VAR>K : Type u_1<VAR>CommRing K<GOAL>∀ (x x_1 : RatFunc K), x.sub x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p - q }
<VAR>K : Type u<VAR>CommRing K<VAR>p q : FractionRing K[X]<GOAL>{ toFractionRing := p - q } = { toFractionRing := p } - { toFractionRing := q }
<VAR>K : Type u_1<VAR>CommRing K<GOAL>∀ (x : RatFunc K), x.neg = match x with | { toFractionRing := p } => { toFractionRing := -p }
<VAR>K : Type u<VAR>CommRing K<VAR>p : FractionRing K[X]<GOAL>{ toFractionRing := -p } = -{ toFractionRing := p }
<VAR>K : Type u_1<VAR>CommRing K<GOAL>RatFunc.one = { toFractionRing := 1 }
<VAR>K : Type u<VAR>CommRing K<GOAL>{ toFractionRing := 1 } = 1
<VAR>K : Type u_1<VAR>CommRing K<GOAL>∀ (x x_1 : RatFunc K), x.mul x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }
<VAR>K : Type u<VAR>CommRing K<VAR>p q : FractionRing K[X]<GOAL>{ toFractionRing := p * q } = { toFractionRing := p } * { toFractionRing := q }
<VAR>K : Type u_1<VAR>CommRing K<VAR>IsDomain K<GOAL>∀ (x x_1 : RatFunc K), x.div x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p q : FractionRing K[X]<GOAL>{ toFractionRing := p / q } = { toFractionRing := p } / { toFractionRing := q }
<VAR>K : Type u_1<VAR>CommRing K<VAR>IsDomain K<GOAL>∀ (x : RatFunc K), x.inv = match x with | { toFractionRing := p } => { toFractionRing := p⁻¹ }
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p : FractionRing K[X]<GOAL>{ toFractionRing := p⁻¹ } = { toFractionRing := p }⁻¹
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p : RatFunc K<GOAL>p ≠ 0 → p * p⁻¹ = 1
<VAR>K : Type u_2<VAR>CommRing K<VAR>R : Type u_3<VAR>SMul R (FractionRing K[X])<GOAL>∀ (x : R) (x_1 : RatFunc K), RatFunc.smul x x_1 = match x, x_1 with | r, { toFractionRing := p } => { toFractionRing := r • p }
<VAR>K : Type u<VAR>CommRing K<VAR>R : Type u_1<VAR>SMul R (FractionRing K[X])<VAR>c : R<VAR>p : FractionRing K[X]<GOAL>{ toFractionRing := c • p } = c • { toFractionRing := p }
<VAR>K : Type u<VAR>CommRing K<VAR>R : Type u_1<VAR>SMul R (FractionRing K[X])<VAR>c : R<VAR>p : RatFunc K<GOAL>(c • p).toFractionRing = c • p.toFractionRing
<VAR>K : Type u<VAR>CommRing K<VAR>x : RatFunc K<VAR>r : K<GOAL>r • x = Polynomial.C r • x
<VAR>K : Type u<VAR>CommRing K<VAR>R : Type u_1<VAR>IsDomain K<VAR>Monoid R<VAR>DistribMulAction R K[X]<VAR>IsScalarTower R K[X] K[X]<VAR>c : R<VAR>p q : K[X]<GOAL>RatFunc.mk (c • p) q = c • RatFunc.mk p q
<VAR>K : Type u<VAR>CommRing K<VAR>self : RatFunc K<GOAL>(RatFunc.toFractionRingRingEquiv K) self = self.toFractionRing
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R[X] S[X]<VAR>MonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰<VAR>n : R[X]<VAR>d : ↥R[X]⁰<GOAL>(RatFunc.map φ hφ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, ⋯⟩ }
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R[X] S[X]<VAR>MonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰<VAR>hf : Function.Injective ⇑φ<GOAL>Function.Injective ⇑(RatFunc.map φ hφ)
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>FunLike F R[X] S[X]<VAR>RingHomClass F R[X] S[X]<VAR>φ : F<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰<GOAL>⇑(RatFunc.mapRingHom φ hφ) = ⇑(RatFunc.map φ hφ)
<VAR>G₀ : Type u_1<VAR>R : Type u_3<VAR>CommGroupWithZero G₀<VAR>CommRing R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰<VAR>n : R[X]<VAR>d : ↥R[X]⁰<GOAL>(RatFunc.liftMonoidWithZeroHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
<VAR>G₀ : Type u_1<VAR>R : Type u_3<VAR>CommGroupWithZero G₀<VAR>CommRing R<VAR>Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰ := ⋯<GOAL>Function.Injective ⇑(RatFunc.liftMonoidWithZeroHom φ hφ')
<VAR>L : Type u_2<VAR>R : Type u_3<VAR>Field L<VAR>CommRing R<VAR>φ : R[X] →+* L<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>n : R[X]<VAR>d : ↥R[X]⁰<GOAL>(RatFunc.liftRingHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
<VAR>L : Type u_2<VAR>R : Type u_3<VAR>Field L<VAR>CommRing R<VAR>Nontrivial R<VAR>φ : R[X] →+* L<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : R[X]⁰ ≤ Submonoid.comap φ L⁰ := ⋯<GOAL>Function.Injective ⇑(RatFunc.liftRingHom φ hφ')
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>x : K[X]<GOAL>RatFunc.mk x 1 = (algebraMap K[X] (RatFunc K)) x
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>x : K[X]<GOAL>{ toFractionRing := (algebraMap K[X] (FractionRing K[X])) x } = (algebraMap K[X] (RatFunc K)) x
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>p q : K[X]<GOAL>RatFunc.mk p q = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>R : Type u_1<VAR>Monoid R<VAR>DistribMulAction R K[X]<VAR>IsScalarTower R K[X] K[X]<VAR>c : R<VAR>p q : K[X]<GOAL>(algebraMap K[X] (RatFunc K)) (c • p) / (algebraMap K[X] (RatFunc K)) q = c • ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q)
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R K[X]<VAR>x : R<GOAL>(algebraMap R (RatFunc K)) x = (algebraMap K[X] (RatFunc K)) ((algebraMap R K[X]) x) / (algebraMap K[X] (RatFunc K)) 1
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>FunLike F K[X] R[X]<VAR>MonoidHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>(RatFunc.map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>FunLike F K[X] R[X]<VAR>MonoidWithZeroHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>p q : K[X]<GOAL>(RatFunc.map φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = (algebraMap R[X] (RatFunc R)) (φ p) / (algebraMap R[X] (RatFunc R)) (φ q)
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>L : Type u_1<VAR>CommGroupWithZero L<VAR>φ : K[X] →*₀ L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<GOAL>(RatFunc.liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>L : Type u_1<VAR>CommGroupWithZero L<VAR>φ : K[X] →*₀ L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<GOAL>(RatFunc.liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p) / (RatFunc.liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>L : Type u_1<VAR>Field L<VAR>φ : K[X] →+* L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<GOAL>(RatFunc.liftRingHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>L : Type u_1<VAR>Field L<VAR>φ : K[X] →+* L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<GOAL>(RatFunc.liftRingHom φ hφ) ((algebraMap K[X] (RatFunc K)) p) / (RatFunc.liftRingHom φ hφ) ((algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<GOAL>RatFunc.ofFractionRing ∘ ⇑(algebraMap K[X] (FractionRing K[X])) = ⇑(algebraMap K[X] (RatFunc K))
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<GOAL>Function.Injective ⇑(algebraMap K[X] (RatFunc K))
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>x : K[X]<GOAL>(algebraMap K[X] (RatFunc K)) x = 0 ↔ x = 0
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>x : K[X]<VAR>hx : x ≠ 0<GOAL>(algebraMap K[X] (RatFunc K)) x ≠ 0
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommRing R<VAR>IsDomain R<VAR>CommSemiring S<VAR>Algebra S K[X]<VAR>Algebra S R[X]<VAR>φ : K[X] →ₐ[S] R[X]<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<GOAL>⇑(RatFunc.mapAlgHom φ hφ) = ⇑(RatFunc.map φ hφ)
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>L : Type u_1<VAR>S : Type u_3<VAR>Field L<VAR>CommSemiring S<VAR>Algebra S K[X]<VAR>Algebra S L<VAR>φ : K[X] →ₐ[S] L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>n : K[X]<VAR>d : ↥K[X]⁰<GOAL>(RatFunc.liftAlgHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>L : Type u_1<VAR>S : Type u_3<VAR>Field L<VAR>CommSemiring S<VAR>Algebra S K[X]<VAR>Algebra S L<VAR>φ : K[X] →ₐ[S] L<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : K[X]⁰ ≤ Submonoid.comap φ L⁰ := ⋯<GOAL>Function.Injective ⇑(RatFunc.liftAlgHom φ hφ')
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>L : Type u_1<VAR>S : Type u_3<VAR>Field L<VAR>CommSemiring S<VAR>Algebra S K[X]<VAR>Algebra S L<VAR>φ : K[X] →ₐ[S] L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<GOAL>(RatFunc.liftAlgHom φ hφ) ((algebraMap K[X] (RatFunc K)) p) / (RatFunc.liftAlgHom φ hφ) ((algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>L : Type u_1<VAR>S : Type u_3<VAR>Field L<VAR>CommSemiring S<VAR>Algebra S K[X]<VAR>Algebra S L<VAR>φ : K[X] →ₐ[S] L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<GOAL>(RatFunc.liftAlgHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>P : Sort v<VAR>p q : K[X]<VAR>f : K[X] → K[X] → P<VAR>f0 : ∀ (p : K[X]), f p 0 = f 0 1<VAR>H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'<VAR>H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q' := ⋯<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).liftOn f H = f p q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>P : Sort v<VAR>p q : K[X]<VAR>f : K[X] → K[X] → P<VAR>f0 : ∀ (p : K[X]), f p 0 = f 0 1<VAR>H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).liftOn' f H = f p q
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>P : RatFunc K → Prop<VAR>x : RatFunc K<VAR>f : ∀ (p q : K[X]), q ≠ 0 → P ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q)<GOAL>P x
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>x : K[X]<VAR>y : ↥K[X]⁰<GOAL>{ toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } = IsLocalization.mk' (RatFunc K) x y
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<VAR>f : K[X]<VAR>g : K[X]<VAR>hg : g ≠ 0<GOAL>RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<GOAL>RatFunc.ofFractionRing = ⇑(IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K))
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<GOAL>RatFunc.toFractionRing = ⇑(IsLocalization.algEquiv K[X]⁰ (RatFunc K) (FractionRing K[X]))
<VAR>K : Type u<VAR>CommRing K<VAR>IsDomain K<GOAL>(RatFunc.toFractionRingRingEquiv K).symm = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K)).toRingEquiv
<VAR>K : Type u<VAR>Field K<VAR>p : K[X]<VAR>q : K[X]<VAR>hq : q ≠ 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).numDenom = (Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))
<VAR>K : Type u<VAR>Field K<VAR>p : K[X]<VAR>q : K[X]<VAR>hq : q ≠ 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.num 0 = 0
<VAR>K : Type u<VAR>Field K<VAR>p q : K[X]<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.num 1 = 1
<VAR>K : Type u<VAR>Field K<VAR>p : K[X]<GOAL>((algebraMap K[X] (RatFunc K)) p).num = p
<VAR>K : Type u<VAR>Field K<VAR>p : K[X]<VAR>q : K[X]<VAR>hq : q ≠ 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num ∣ p
<VAR>K : Type u<VAR>Field K<VAR>p : K[X]<VAR>q : K[X]<VAR>hq : q ≠ 0<GOAL>Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p
<VAR>K : Type u<VAR>Field K<VAR>p : K[X]<VAR>q : K[X]<VAR>hq : q ≠ 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<GOAL>x.denom.Monic
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<GOAL>x.denom ≠ 0
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.denom 0 = 1
<VAR>K : Type u<VAR>Field K<GOAL>RatFunc.denom 1 = 1
<VAR>K : Type u<VAR>Field K<VAR>p : K[X]<GOAL>((algebraMap K[X] (RatFunc K)) p).denom = 1
<VAR>K : Type u<VAR>Field K<VAR>p q : K[X]<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom ∣ q
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<GOAL>(algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom = x
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<GOAL>IsCoprime x.num x.denom
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<GOAL>x.num = 0 ↔ x = 0
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<VAR>hx : x ≠ 0<GOAL>x.num ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>x.num * q = p * x.denom ↔ x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<GOAL>(x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<GOAL>(-x).num * x.denom = -x.num * (-x).denom
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<GOAL>(x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<VAR>p : K[X]<VAR>hp : p ≠ 0<GOAL>x.num ∣ p ↔ ∃ q, q ≠ 0 ∧ x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q
<VAR>K : Type u<VAR>Field K<VAR>x : RatFunc K<VAR>q : K[X]<VAR>hq : q ≠ 0<GOAL>x.denom ∣ q ↔ ∃ p, x = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<GOAL>(x * y).num ∣ x.num * y.num
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<GOAL>(x * y).denom ∣ x.denom * y.denom
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<GOAL>(x + y).denom ∣ x.denom * y.denom
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>F : Type u_2<VAR>Zero L<VAR>FunLike F K[X] L<VAR>ZeroHomClass F K[X] L<VAR>φ : F<VAR>hφ : Function.Injective ⇑φ<VAR>f : RatFunc K<GOAL>φ f.denom ≠ 0
<VAR>K : Type u<VAR>Field K<VAR>R : Type u_1<VAR>F : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>FunLike F K[X] R[X]<VAR>MonoidHomClass F K[X] R[X]<VAR>φ : F<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰<VAR>f : RatFunc K<GOAL>(RatFunc.map φ hφ) f = (algebraMap R[X] (RatFunc R)) (φ f.num) / (algebraMap R[X] (RatFunc R)) (φ f.denom)
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>CommGroupWithZero L<VAR>φ : K[X] →*₀ L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>f : RatFunc K<GOAL>(RatFunc.liftMonoidWithZeroHom φ hφ) f = φ f.num / φ f.denom
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>Field L<VAR>φ : K[X] →+* L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>f : RatFunc K<GOAL>(RatFunc.liftRingHom φ hφ) f = φ f.num / φ f.denom
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>S : Type u_2<VAR>Field L<VAR>CommSemiring S<VAR>Algebra S K[X]<VAR>Algebra S L<VAR>φ : K[X] →ₐ[S] L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>f : RatFunc K<GOAL>(RatFunc.liftAlgHom φ hφ) f = φ f.num / φ f.denom
<VAR>K : Type u<VAR>Field K<VAR>x y : RatFunc K<VAR>hxy : x + y ≠ 0<GOAL>x.num * y.denom + x.denom * y.num ≠ 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>X : C<VAR>R : CategoryTheory.Presieve X<VAR>self : R.Extensive<GOAL>∃ α, ∃ (_ : Finite α), ∃ Z π, R = CategoryTheory.Presieve.ofArrows Z π ∧ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>X : C<VAR>S : CategoryTheory.Presieve X<VAR>S.Extensive<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>CategoryTheory.Limits.PreservesFiniteProducts F<GOAL>CategoryTheory.Presieve.IsSheafFor F S
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>W : C<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.extensiveTopology C) (CategoryTheory.yoneda.obj W)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.FinitaryPreExtensive C<GOAL>CategoryTheory.Sheaf.Subcanonical (CategoryTheory.extensiveTopology C)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>CategoryTheory.FinitaryExtensive C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.extensiveTopology C) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>CategoryTheory.FinitaryExtensive C<VAR>F : CategoryTheory.Functor Cᵒᵖ D<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X A : C<VAR>f : A ⟶ X<VAR>hf : CategoryTheory.Mono f<GOAL>(CategoryTheory.MonoOver.mk' f).obj = CategoryTheory.Over.mk f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>f : CategoryTheory.MonoOver X<GOAL>((CategoryTheory.MonoOver.forget X).obj f).left = f.obj.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X A : C<VAR>f : A ⟶ X<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.MonoOver.mk' f).obj.left = A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X A : C<VAR>f : A ⟶ X<VAR>CategoryTheory.Mono f<GOAL>(CategoryTheory.MonoOver.mk' f).arrow = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>f : CategoryTheory.MonoOver X<GOAL>((CategoryTheory.MonoOver.forget X).obj f).hom = f.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>f g : CategoryTheory.MonoOver X<VAR>k : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp k.left g.arrow = f.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>f g : CategoryTheory.MonoOver X<VAR>h : f.obj.left ≅ g.obj.left<VAR>w : CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow := by aesop_cat<GOAL>(CategoryTheory.MonoOver.isoMk h w).hom = CategoryTheory.MonoOver.homMk h.hom w
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>f g : CategoryTheory.MonoOver X<VAR>h : f.obj.left ≅ g.obj.left<VAR>w : CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow := by aesop_cat<GOAL>(CategoryTheory.MonoOver.isoMk h w).inv = CategoryTheory.MonoOver.homMk h.inv ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>Y : D<VAR>F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)<VAR>h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom<GOAL>∀ {X_1 Y_1 : CategoryTheory.MonoOver Y} (k : X_1 ⟶ Y_1), (CategoryTheory.MonoOver.lift F h).map k = ((CategoryTheory.MonoOver.forget Y).comp F).map k
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>Y : D<VAR>F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)<VAR>h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom<VAR>f : CategoryTheory.MonoOver Y<GOAL>((CategoryTheory.MonoOver.lift F h).obj f).obj = F.obj ((CategoryTheory.MonoOver.forget Y).obj f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)<VAR>h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom<GOAL>(CategoryTheory.MonoOver.lift F h).comp (CategoryTheory.MonoOver.forget X) = (CategoryTheory.MonoOver.forget Y).comp F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>Y : D<VAR>F : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)<VAR>h : ∀ (f : CategoryTheory.MonoOver Y), CategoryTheory.Mono (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom<VAR>f : CategoryTheory.MonoOver Y<GOAL>((CategoryTheory.MonoOver.lift F h).obj f).arrow = (F.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>f : X ⟶ Y<VAR>g : CategoryTheory.MonoOver Y<GOAL>((CategoryTheory.MonoOver.pullback f).obj g).obj.left = CategoryTheory.Limits.pullback g.arrow f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>f : X ⟶ Y<VAR>g : CategoryTheory.MonoOver Y<GOAL>((CategoryTheory.MonoOver.pullback f).obj g).arrow = CategoryTheory.Limits.pullback.snd ((CategoryTheory.MonoOver.forget Y).obj g).hom f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>g : CategoryTheory.MonoOver X<GOAL>((CategoryTheory.MonoOver.map f).obj g).obj.left = g.obj.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>g : CategoryTheory.MonoOver X<GOAL>((CategoryTheory.MonoOver.map f).obj g).arrow = CategoryTheory.CategoryStruct.comp g.arrow f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : C<VAR>e : A ≅ B<GOAL>(CategoryTheory.MonoOver.mapIso e).unitIso = ((CategoryTheory.MonoOver.mapComp e.hom e.inv).symm ≪≫ CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.MonoOver.mapId A).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : C<VAR>e : A ≅ B<GOAL>(CategoryTheory.MonoOver.mapIso e).counitIso = (CategoryTheory.MonoOver.mapComp e.inv e.hom).symm ≪≫ CategoryTheory.eqToIso ⋯ ≪≫ CategoryTheory.MonoOver.mapId B
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : C<VAR>e : A ≅ B<GOAL>(CategoryTheory.MonoOver.mapIso e).inverse = CategoryTheory.MonoOver.map e.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : C<VAR>e : A ≅ B<GOAL>(CategoryTheory.MonoOver.mapIso e).functor = CategoryTheory.MonoOver.map e.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.MonoOver.congr X e).functor = CategoryTheory.MonoOver.lift (CategoryTheory.Over.post e.functor) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.MonoOver.congr X e).counitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.MonoOver.isoMk (e.counitIso.app Y.obj.left) ⋯) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.MonoOver.congr X e).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.MonoOver.isoMk (e.unitIso.app Y.obj.left) ⋯) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>(CategoryTheory.MonoOver.congr X e).inverse = (CategoryTheory.MonoOver.lift (CategoryTheory.Over.post e.inverse) ⋯).comp (CategoryTheory.MonoOver.mapIso (e.unitIso.symm.app X)).functor