mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom

Tactic:
rw [div_add_div _ _ hx hy, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
    div_eq_mul_inv, div_eq_iff hxy]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a (x + y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    (Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.denom +
        Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.num) *
      Polynomial.eval₂ f a (x + y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case h
K : Type u_1
inst✝ : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ Valued.v 0 = n

Tactic:
simp [hn0]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (∑ v ∈ f.support, (monomial v) (coeff v f))

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (∑ v ∈ f.support, (monomial v) (coeff v f))
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ IsIntegral R (coeff (Finsupp.mapDomain Subtype.val n) f)

Tactic:
[

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ IsIntegral R (coeff (Finsupp.mapDomain Subtype.val n) f)
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
⊢ Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P) =
    Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q)

Tactic:
← Ideal.under_under (B := S),

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : WeaklyQuasiFiniteAt R Q
this : (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P).IsPrime
⊢ Ideal.under R (Ideal.under S (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) P)) =
    Ideal.under R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R Q))) Q)
Module: Mathlib.RingTheory.QuasiFinite.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
H : RingHom.ker f ≤ Ideal.map C (Ideal.under R P)
algInst✝ : Algebra R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
H' : Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f) = ⊥
g' : p.ResidueField[X] ≃ₐ[p.ResidueField] p.Fiber S :=
  ((AlgEquiv.quotientBot p.ResidueField p.ResidueField[X]).symm.trans
        (Ideal.quotientEquivAlgOfEq p.ResidueField ⋯)).trans
    (fiberEquivQuotient f hf p).symm
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S)
hQ :
  (PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := ⋯ }).symm Q =
    ⟨{ asIdeal := P, isPrime := inst✝¹ }, ⋯⟩
⊢ False

Tactic:
have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal :=
    .baseChange P Q.asIdeal congr($(hQ.symm).1.1)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : Algebra.WeaklyQuasiFiniteAt R P
H : RingHom.ker f ≤ Ideal.map C (Ideal.under R P)
algInst✝ : Algebra R[X] S := f.toAlgebra
p : Ideal R := Ideal.under R P
H' : Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker f) = ⊥
g' : p.ResidueField[X] ≃ₐ[p.ResidueField] p.Fiber S :=
  ((AlgEquiv.quotientBot p.ResidueField p.ResidueField[X]).symm.trans
        (Ideal.quotientEquivAlgOfEq p.ResidueField ⋯)).trans
    (fiberEquivQuotient f hf p).symm
Q : PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S)
hQ :
  (PrimeSpectrum.preimageEquivFiber R S { asIdeal := p, isPrime := ⋯ }).symm Q =
    ⟨{ asIdeal := P, isPrime := inst✝¹ }, ⋯⟩
inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal
⊢ False
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
I : Ideal R
inst✝⁵ : I.IsPrime
J : Ideal R[X]
inst✝⁴ : J.IsPrime
inst✝³ : J.LiesOver I
inst✝² : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra I J
f : R[X] →ₐ[R] S
hf : Function.Surjective ⇑f
p : Ideal R
inst✝ : p.IsPrime
⊢ p.Fiber S ≃ₐ[p.ResidueField] p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)

Tactic:
by
  refine .ofAlgHom (Algebra.TensorProduct.lift (Algebra.ofId _ _) (AlgHom.liftOfSurjective _ hf
    ((Ideal.Quotient.mkₐ _ _).comp (mapAlgHom (Algebra.ofId _ _))) ?_) fun _ _ ↦ .all _ _)
    (Ideal.Quotient.liftₐ _ (aeval (1 ⊗ₜ f .X)) ?_) ?_ ?_
  · simp [AlgHom.comp_toRingHom, ← RingHom.comap_ker, ← Ideal.map_le_iff_le_comap]
  · change Ideal.map _ _ ≤ RingHom.ker (aeval _).toRingHom
    rw [Ideal.map_le_iff_le_comap, RingHom.comap_ker]
    have : ((aeval (1 ⊗ₜ[R] f X : p.Fiber S)).restrictScalars R).comp
        (mapAlgHom (Algebra.ofId R p.ResidueField)) =
        Algebra.TensorProduct.includeRight.comp f := by ext; simp
    exact .trans_eq (by intro; aesop) congr(RingHom.ker $this).symm
  · apply Ideal.Quotient.algHom_ext
    ext
    simp
  · ext x
    obtain ⟨x, rfl⟩ := hf x
    simpa using aeval_algHom_apply
      ((Algebra.TensorProduct.includeRight : S →ₐ[_] p.Fiber S).comp f) X x

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : targetAffineLocally (fun X x f x_1 ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Hom.appTop f)).Finite) f
⊢ LocallyQuasiFinite f

Tactic:
HasRingHomProperty.eq_affineLocally @LocallyQuasiFinite

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : targetAffineLocally (fun X x f x_1 ↦ IsAffine X ∧ (CommRingCat.Hom.hom (Hom.appTop f)).Finite) f
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.QuasiFinite) f
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ RatFunc.liftOn 1 (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ = 1

Tactic:
[

Goal state after:
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ RatFunc.liftOn 1 (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ = 1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ ({ toFractionRing := Localization.mk p q } * { toFractionRing := Localization.mk p' q' }).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk p q }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p' q' }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯

Tactic:
[

Goal state after:
case H.H
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
hq : φ ↑q ∈ S[X]⁰
hq' : φ ↑q' ∈ S[X]⁰
hqq' : φ ↑(q * q') ∈ S[X]⁰
⊢ ({ toFractionRing := Localization.mk p q } * { toFractionRing := Localization.mk p' q' }).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk p q }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk p' q' }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (↑(map φ hφ)).toFun 0 = 0

Tactic:
[

Goal state after:
K : Type u
inst✝⁶ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁵ : CommGroupWithZero G₀
inst✝⁴ : Field L
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : RingHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
⊢ (↑(map φ hφ)).toFun 0 = 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ RatFunc.liftOn 0 (fun p q ↦ φ p / φ q) ⋯ = 0

Tactic:
[

Goal state after:
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ RatFunc.liftOn 0 (fun p q ↦ φ p / φ q) ⋯ = 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ RatFunc.liftOn 1 (fun p q ↦ φ p / φ q) ⋯ = 1

Tactic:
[

Goal state after:
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ RatFunc.liftOn 1 (fun p q ↦ φ p / φ q) ⋯ = 1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk y✝.1 y✝.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.1 a'.2 } →
    { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }

Tactic:
[

Goal state after:
case H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk y✝.1 y✝.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.1 a'.2 } →
    { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)
      { toFractionRing := Localization.mk (↑(p, q).2 * (p', q').1 + ↑(p', q').2 * (p, q).1) ((p, q).2 * (p', q').2) } =
    (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk (p, q).1 (p, q).2 } +
      (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk (p', q').1 (p', q').2 }

Tactic:
simp only [RingHom.toMonoidWithZeroHom_eq_coe,
        liftMonoidWithZeroHom_apply_ofFractionRing_mk]

Goal state after:
case inr.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ (↑q * p' + ↑q' * p) / φ ↑(q * q') = φ p / φ ↑q + φ p' / φ ↑q'
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
⊢ RatFunc.mk ((algebraMap R K[X]) 0) 1 = 0

Tactic:
by simp only [mk_one', map_zero, ofFractionRing_zero]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ✝ : K[X] →ₐ[S] L
hφ✝ : K[X]⁰ ≤ Submonoid.comap φ✝ L⁰
φ : K[X] →ₐ[S] R[X]
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
r : S
⊢ (↑↑(mapRingHom φ hφ)).toFun ((algebraMap S K⟮X⟯) r) = (algebraMap S R⟮X⟯) r

Tactic:
[

Goal state after:
K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ✝ : K[X] →ₐ[S] L
hφ✝ : K[X]⁰ ≤ Submonoid.comap φ✝ L⁰
φ : K[X] →ₐ[S] R[X]
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
r : S
⊢ (↑↑(mapRingHom φ hφ)).toFun ((algebraMap S K⟮X⟯) r) = (algebraMap S R⟮X⟯) r
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ : K[X] →ₐ[S] L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
r : S
⊢ (↑↑(liftRingHom φ.toRingHom hφ)).toFun ((algebraMap S K⟮X⟯) r) = (algebraMap S L) r

Tactic:
[

Goal state after:
K : Type u
inst✝⁸ : CommRing K
inst✝⁷ : IsDomain K
L : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Field L
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommSemiring S
inst✝² : Algebra S K[X]
inst✝¹ : Algebra S L
inst✝ : Algebra S R[X]
φ : K[X] →ₐ[S] L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
r : S
⊢ (↑↑(liftRingHom φ.toRingHom hφ)).toFun ((algebraMap S K⟮X⟯) r) = (algebraMap S L) r
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f
K✝ : Type u
inst✝¹¹ : CommRing K✝
inst✝¹⁰ : IsDomain K✝
A : Type u_1
k : Type u_2
K : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A[X] k
inst✝⁴ : Algebra A[X] K
inst✝³ : SMul k K
inst✝² : FaithfulSMul A[X] k
inst✝¹ : FaithfulSMul A[X] K
inst✝ : IsScalarTower A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
⊢ q • (((algebraMap A[X] A⟮X⟯) p / (algebraMap A[X] A⟮X⟯) q) • b) • c =
    q • ((algebraMap A[X] A⟮X⟯) p / (algebraMap A[X] A⟮X⟯) q) • b • c

Tactic:
[

Goal state after:
case f
K✝ : Type u
inst✝¹¹ : CommRing K✝
inst✝¹⁰ : IsDomain K✝
A : Type u_1
k : Type u_2
K : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A[X] k
inst✝⁴ : Algebra A[X] K
inst✝³ : SMul k K
inst✝² : FaithfulSMul A[X] k
inst✝¹ : FaithfulSMul A[X] K
inst✝ : IsScalarTower A[X] k K
b : k
c : K
p q : A[X]
hq : q ≠ 0
⊢ q • (((algebraMap A[X] A⟮X⟯) p / (algebraMap A[X] A⟮X⟯) q) • b) • c =
    q • ((algebraMap A[X] A⟮X⟯) p / (algebraMap A[X] A⟮X⟯) q) • b • c
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
this : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ (aeval P.X) P.g * (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) Y = 1

Tactic:
this

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
this : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ ((Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom) P.g *
      (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) Y =
    1
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval ((Ideal.Quotient.mk I) x)) P.g * (Ideal.Quotient.mk I) a = 1
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval ((Ideal.Quotient.mk I) x)) P.g * (Ideal.Quotient.mk I) a = 1
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0

Tactic:
· exact algebraMap_ne_zero (denom_ne_zero y)

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ ∃ p, x⁻¹ = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) x.num

Tactic:
refine ⟨x.denom, ?_⟩

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹ = (algebraMap K[X] K⟮X⟯) x.denom / (algebraMap K[X] K⟮X⟯) x.num
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hxy : x + y ≠ 0
⊢ x.num * y.denom + x.denom * y.num ≠ 0

Tactic:
intro h_zero
  have h := num_denom_add x y
  rw [h_zero, zero_mul] at h
  exact (mul_ne_zero (num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)) h

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ Ideal.span {(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)} =
    Ideal.map (↑(Bivariate.equivMvPolynomial R)) (Ideal.span {C P.f, Y * C P.g - 1})

Tactic:
by simp only [Ideal.map_span, Set.image_insert_eq, Set.image_singleton]; rfl

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr.refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝² : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝¹ : Algebra (↥R₂) St := R₂.toAlgebra
this✝ : Algebra (↥R₁) St := R₁.toAlgebra
this : IsScalarTower (↥R₁) (↥R₂) St
h✝ : Nontrivial ↥R₁
⊢ (C ⟨t', ⋯⟩ * map (algebraMap R ↥R₁) r).natDegree < (map (algebraMap R ↥R₁) p).natDegree

Tactic:
grw [natDegree_C_mul_le, natDegree_map_le, hpm.natDegree_map]; assumption

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R] Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g) := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst✝ : Algebra (AdjoinRoot 𝓟.f) S :=
  ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) (Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g)))).toAlgebra
this : IsLocalization (Submonoid.powers ((AdjoinRoot.mk 𝓟.f) 𝓟.g)) S
m : ℕ
hm : ∀ (k : ℕ), IsIntegral (AdjoinRoot 𝓟.f) ((algebraMap (AdjoinRoot 𝓟.f) S) ((AdjoinRoot.mk 𝓟.f) (𝓟.g ^ (m + k))) • a)
⊢ ∃ n, ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R] Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g) := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst✝ : Algebra (AdjoinRoot 𝓟.f) S :=
  ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) (Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g)))).toAlgebra
this : IsLocalization (Submonoid.powers ((AdjoinRoot.mk 𝓟.f) 𝓟.g)) S
m : ℕ
hm : ∀ (k : ℕ), IsIntegral (AdjoinRoot 𝓟.f) ((algebraMap (AdjoinRoot 𝓟.f) S) ((AdjoinRoot.mk 𝓟.f) (𝓟.g ^ (m + k))) • a)
⊢ ∃ n, ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)