mathlib-initiative/mathlib-tactics huggingface dataset:
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
this :
  (AlgHom.restrictScalars R (aeval (1 ⊗ₜ[R] f X))).comp (mapAlgHom (Algebra.ofId R p.ResidueField)) =
    Algebra.TensorProduct.includeRight.comp f
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker ↑f → x✝ ∈ RingHom.ker (Algebra.TensorProduct.includeRight.comp f)

Tactic:
;

Goal state after:
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
this :
  (AlgHom.restrictScalars R (aeval (1 ⊗ₜ[R] f X))).comp (mapAlgHom (Algebra.ofId R p.ResidueField)) =
    Algebra.TensorProduct.includeRight.comp f
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker ↑f → x✝ ∈ RingHom.ker (Algebra.TensorProduct.includeRight.comp f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : LocallyQuasiFinite f
⊢ LocallyQuasiFinite (X.homOfLE e ≫ f ∣_ V)

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : LocallyQuasiFinite f
⊢ LocallyQuasiFinite (X.homOfLE e ≫ f ∣_ V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case refine_1.refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ = Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))

Tactic:
;

Goal state after:
case refine_1.refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Spec.map φ = Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p : K[X]
q✝ : K⟮X⟯
q r : K[X]
x✝ : r ≠ 0
⊢ c • RatFunc.mk (p • q) r = c • p • RatFunc.mk q r

Tactic:
mk_smul

Goal state after:
K : Type u
inst✝⁴ : CommRing K
R : Type u_1
inst✝³ : IsDomain K
inst✝² : Monoid R
inst✝¹ : DistribMulAction R K[X]
inst✝ : IsScalarTower R K[X] K[X]
c : R
p : K[X]
q✝ : K⟮X⟯
q r : K[X]
x✝ : r ≠ 0
⊢ c • p • RatFunc.mk q r = c • p • RatFunc.mk q r
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]⁰
y : R⟮X⟯
x : FractionRing R[X]
⊢ ({ toFractionRing := x } * y).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := x }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      y.liftOn (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 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✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
y : R⟮X⟯
x : FractionRing R[X]
⊢ ({ toFractionRing := x } * y).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := x }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      y.liftOn (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↥X
hx : x ∈ U.toOpens
f : ↑Γ(X, U.toOpens)
hfs : f ∈ s
g : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen f ⊓ X.basicOpen g)
hxV : x ∈ toOpens ⟨X.basicOpen f ⊓ X.basicOpen g, hV⟩
⊢ ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
exact ⟨f, hfs, hxV.1⟩

Goal state after:
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]⁰
x y : R⟮X⟯
⊢ (x * y).liftOn (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    x.liftOn (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      y.liftOn (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯

Tactic:
by
    obtain ⟨x⟩ := x; obtain ⟨y⟩ := y
    cases x using Localization.induction_on with | _ pq
    cases y using Localization.induction_on with | _ p'q'
    obtain ⟨p, q⟩ := pq
    obtain ⟨p', q'⟩ := p'q'
    have hq : φ q ∈ S[X]⁰ := hφ q.prop
    have hq' : φ q' ∈ S[X]⁰ := hφ q'.prop
    have hqq' : φ ↑(q * q') ∈ S[X]⁰ := by simpa using Submonoid.mul_mem _ hq hq'
    simp_rw [← ofFractionRing_mul, Localization.mk_mul, liftOn_ofFractionRing_mk, dif_pos hq,
      dif_pos hq', dif_pos hqq', ← ofFractionRing_mul, Submonoid.coe_mul, map_mul,
      Localization.mk_mul, Submonoid.mk_mul_mk]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
haU : a ∈ ↑U
⊢ (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x ∈ ↑V

Tactic:
;

Goal state after:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
haU : a ∈ ↑U
⊢ (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x ∈ ↑V
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
haU : a ∈ ↑U
⊢ (pullback.snd ((directedCover X).f U) ((directedCover X).f V) ≫ (directedCover X).f V) x ∈ ↑V

Tactic:
;

Goal state after:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
haU : a ∈ ↑U
⊢ (pullback.snd ((directedCover X).f U) ((directedCover X).f V) ≫ (directedCover X).f V) x ∈ ↑V
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
⊢ Spec.map (X.presheaf.map ((toOpensFunctor X).map f).op) ≫ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X

Tactic:
;

Goal state after:
X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
⊢ Spec.map (X.presheaf.map ((toOpensFunctor X).map f).op) ≫ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
⊢ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X

Tactic:
;

Goal state after:
X : Scheme
U V : X.AffineZariskiSite
f : U ⟶ V
⊢ ⋯.fromSpec = ⋯.fromSpec ≫ 𝟙 X
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
D : Cover.RelativeGluingData (directedCover X) := relativeGluingData ⋯
F : (directedCover X).I₀ ⥤ Scheme := D.functor
this : (D.functor ⋙ forget).IsLocallyDirected
U : (X.openCoverOfIsOpenCover (fun i ↦ ↑i) ⋯).toPreZeroHypercover.1
⊢ Set.range ⇑(pullback.fst (colimit.desc F (cocone X)) (↑U).ι) =
    Set.range ⇑((IsAffineOpen.isoSpec ⋯).hom ≫ colimit.ι F U)

Tactic:
by
      rw [Pullback.range_fst, Opens.range_ι, ← Hom.coe_opensRange, Hom.opensRange_comp_of_isIso,
        ← Scheme.Hom.coe_preimage]
      convert! congr($(D.toBase_preimage_eq_opensRange_ι U).1)
      · delta cocone
        congr with U
        simp [D, relativeGluingData, restrictIsoSpec]
      · simp

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

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝¹ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
x✝ : R
⊢ ((Localization.localRingHom (Ideal.comap f J) J f ⋯).comp (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
      x✝ =
    (algebraMap R (Localization.AtPrime J)) x✝

Tactic:
;

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝¹ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
x✝ : R
⊢ ((Localization.localRingHom (Ideal.comap f J) J f ⋯).comp (algebraMap R (Localization.AtPrime (Ideal.comap f J))))
      x✝ =
    (algebraMap R (Localization.AtPrime J)) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝¹ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
x✝ : R
⊢ (algebraMap S (Localization.AtPrime J)) (f x✝) = (algebraMap R (Localization.AtPrime J)) x✝

Tactic:
;

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
inst✝² : LocallyQuasiFinite f✝
x : ↥X
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.QuasiFinite
J : Ideal S
x✝¹ : J.IsPrime
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.QuasiFinite R S
x✝ : R
⊢ (algebraMap S (Localization.AtPrime J)) (f x✝) = (algebraMap R (Localization.AtPrime J)) x✝
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]
r : R
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) r) }.toFractionRing =
    (algebraMap R (FractionRing K[X])) r

Tactic:
;

Goal state after:
K : Type u
inst✝³ : CommRing K
inst✝² : IsDomain K
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R K[X]
r : R
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) ((algebraMap R K[X]) r) }.toFractionRing =
    (algebraMap R (FractionRing K[X])) r
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case e'_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
H : ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι) ⁻¹' ⇑f ⁻¹' {f ((pullback.fst f ι) x)}
f' : ↑(⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x}) → ↑(⇑f ⁻¹' {f ((pullback.fst f ι) x)}) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι)) (⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x})
    (⇑f ⁻¹' {f ((pullback.fst f ι) x)}) ⋯
this : Topology.IsOpenEmbedding f'
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen {f' ⟨x, ⋯⟩}

Tactic:
;

Goal state after:
case e'_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X},
    (∃ R, Y = Spec R) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
x : ↥(pullback f (Y.affineCover.f i))
hy : (Y.affineCover.f i) ((pullback.snd f (Y.affineCover.f i)) x) = f ((pullback.fst f (Y.affineCover.f i)) x)
ι : Y.affineCover.X i ⟶ Y := Y.affineCover.f i
H : ⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x} = ⇑(pullback.fst f ι) ⁻¹' ⇑f ⁻¹' {f ((pullback.fst f ι) x)}
f' : ↑(⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x}) → ↑(⇑f ⁻¹' {f ((pullback.fst f ι) x)}) :=
  Set.MapsTo.restrict (⇑(pullback.fst f ι)) (⇑(pullback.snd f ι) ⁻¹' {(pullback.snd f ι) x})
    (⇑f ⁻¹' {f ((pullback.fst f ι) x)}) ⋯
this : Topology.IsOpenEmbedding f'
⊢ IsOpen {⟨(pullback.fst f (Y.affineCover.f i)) x, ⋯⟩} ↔ IsOpen {f' ⟨x, ⋯⟩}
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case e'_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩} ↔ IsOpen {(⇑f ⁻¹' {f (ι x)}).restrictPreimage ⇑ι ⟨x, ⋯⟩}

Tactic:
;

Goal state after:
case e'_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩} ↔ IsOpen {(⇑f ⁻¹' {f (ι x)}).restrictPreimage ⇑ι ⟨x, ⋯⟩}
Module: Mathlib.RingTheory.Etale.StandardEtale

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
⊢ (aeval P.X) X = ((Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom) X
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
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
⊢ (aeval P.X) X = ((Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom) 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
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
⊢ (aeval P.X) X = ((Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom) X
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
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
H' : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ ↑f.toRingHom ↑⋯.unit⁻¹ = ↑g.toRingHom ↑⋯.unit⁻¹

Tactic:
← Units.coe_map_inv,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
H' : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ ↑((Units.map ↑f.toRingHom) ⋯.unit)⁻¹ = ↑g.toRingHom ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_1
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 x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ (aeval x) P.f + (aeval x) (derivative P.f) * ((aeval x) P.f * -b) = 0

Tactic:
;

Goal state after:
case refine_1
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 x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
⊢ (aeval x) P.f + (aeval x) (derivative P.f) * ((aeval x) P.f * -b) = 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ Associated x⁻¹.denom x.num

Tactic:
apply Associated.symm
  convert! associated_num_inv (inv_ne_zero hx)
  rw [inv_inv]

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

Goal state before:
pp: case refine_3
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
⊢ (((P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯).comp
            (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯)).comp
        (Algebra.algHom R (AdjoinRoot P.f) (Localization (Submonoid.powers ((AdjoinRoot.mk P.f) P.g)))))
      (AdjoinRoot.root P.f) =
    ((AlgHom.id R (Localization.Away ((AdjoinRoot.mk P.f) P.g))).comp
        (Algebra.algHom R (AdjoinRoot P.f) (Localization (Submonoid.powers ((AdjoinRoot.mk P.f) P.g)))))
      (AdjoinRoot.root P.f)

Tactic:
;

Goal state after:
case refine_3
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
⊢ (((P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯).comp
            (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯)).comp
        (Algebra.algHom R (AdjoinRoot P.f) (Localization (Submonoid.powers ((AdjoinRoot.mk P.f) P.g)))))
      (AdjoinRoot.root P.f) =
    ((AlgHom.id R (Localization.Away ((AdjoinRoot.mk P.f) P.g))).comp
        (Algebra.algHom R (AdjoinRoot P.f) (Localization (Submonoid.powers ((AdjoinRoot.mk P.f) P.g)))))
      (AdjoinRoot.root P.f)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_4
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
⊢ ((IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
        (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯))
      P.X =
    (AlgHom.id R P.Ring) P.X

Tactic:
;

Goal state after:
case refine_4
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
⊢ ((IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
        (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯))
      P.X =
    (AlgHom.id R P.Ring) P.X
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_5
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.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
            (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯).comp
        (P.lift
          ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X) ⋯))
      P.X =
    (AlgHom.id R P.Ring) P.X

Tactic:
;

Goal state after:
case refine_5
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.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
            (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯).comp
        (P.lift
          ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X) ⋯))
      P.X =
    (AlgHom.id R P.Ring) P.X
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.span {↑(Bivariate.equivMvPolynomial R) (C P.f), ↑(Bivariate.equivMvPolynomial R) (Y * C P.g - 1)}

Tactic:
;

Goal state after:
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.span {↑(Bivariate.equivMvPolynomial R) (C P.f), ↑(Bivariate.equivMvPolynomial R) (Y * C P.g - 1)}
Module: Mathlib.RingTheory.Etale.StandardEtale

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : StandardEtalePair R
⊢ (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) (C X) = P.X