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

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff
        ((Finsupp.mapDomain (⇑e) σ) none)) =
    coeff σ F
⊢ False

Tactic:
Finsupp.mapDomain_equiv_apply,

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff (σ (e.symm none))) =
    coeff σ F
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
algInst✝ : Algebra ↑(CommRingCat.of K) ↑Γ(X, ⊤) := (CommRingCat.Hom.hom F).toAlgebra
algebraizeInst✝ : Algebra.IsIntegral ↑(CommRingCat.of K) ↑Γ(X, ⊤)
⊢ IsField ↑Γ(X, ⊤)

Tactic:
exact isField_of_isIntegral_of_isField' (Field.toIsField K)

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

Goal state before:
pp: case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝ :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : ⟨x, hxU⟩ ∈ closure ↑(smoothLocus (U.ι ≫ f))
⊢ x ∈ closure ↑(smoothLocus f)

Tactic:
← preimage_smoothLocus_eq,

Goal state after:
case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝ :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : ⟨x, hxU⟩ ∈ closure ↑(U.ι ⁻¹ᵁ smoothLocus f)
⊢ x ∈ closure ↑(smoothLocus f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this✝¹ : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure ↑U = irreducibleComponent x
this✝ : IsIntegral ↑U
this : genericPoint ↥↑U ∈ smoothLocus (U.ι ≫ f)
⊢ U.ι (genericPoint ↥↑U) ∈ smoothLocus f

Tactic:
← preimage_smoothLocus_eq,

Goal state after:
X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this✝¹ : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure ↑U = irreducibleComponent x
this✝ : IsIntegral ↑U
this : genericPoint ↥↑U ∈ U.ι ⁻¹ᵁ smoothLocus f
⊢ U.ι (genericPoint ↥↑U) ∈ smoothLocus f
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
s t : ↥F.support
h : σ' ↑s = σ' ↑t
i : ι
⊢ ↑s i = ↑t i

Tactic:
hσ' _ s.2,

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
s t : ↥F.support
h : σ' ↑s = σ' ↑t
i : ι
⊢ (p • σ' ↑s) i = ↑t i
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion (pullback.diagonal f)], (∃ R, Y = Spec R) → FormallyUnramified f
hY : ¬∃ R, Y = Spec R
⊢ FormallyUnramified f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @FormallyUnramified) Y.affineCover]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion (pullback.diagonal f)], (∃ R, Y = Spec R) → FormallyUnramified f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), FormallyUnramified (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsReduced S
x : S
hx : IsStronglyTranscendental R x
q : Ideal S
hq : q ∈ minimalPrimes S
u : S
p : R[X]
e : (aeval x) p * u ∈ q
this✝¹ : q.IsPrime
this✝ : Ring.KrullDimLE 0 (Localization.AtPrime q)
this : Field (Localization.AtPrime q) := ⋯.toField
m : S
hmq : m ∈ q.primeCompl
hm : ↑⟨m, hmq⟩ * ((aeval x) p * u) = 0
i : ℕ
⊢ (algebraMap R S) (p.coeff i) * u * m = 0

Tactic:
simpa [← mul_assoc] using congr(($(hx (u * m) p (by linear_combination hm))).coeff i)

Goal state after:
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
⊢ ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I ≃+* S ⧸ Ideal.map (algebraMap R S) I

Tactic:
let f : R<x> ⧸ I.map (algebraMap R R<x>) →+* S ⧸ I.map (algebraMap R S) :=
    (Ideal.Quotient.lift (I.map (algebraMap R R<x>))
      ((Ideal.Quotient.mk (I.map (algebraMap R S))).comp (algebraMap R<x> S)) (fun r hr => by
      have : algebraMap R S = (algebraMap R<x> S).comp (algebraMap R R<x>) := by ext; rfl
      rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, this, ← Ideal.map_map]
      exact Ideal.mem_map_of_mem _ hr))

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
⊢ ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I ≃+* S ⧸ Ideal.map (algebraMap R S) I
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L
h : Transcendental K f
g : K[X]
⊢ (algEquivOfTranscendental f h) ((algebraMap K[X] K⟮X⟯) g) = (aeval (AdjoinSimple.gen K f)) g

Tactic:
by
  ext
  simp [algEquivOfTranscendental]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ Function.Surjective ⇑Valued.v

Tactic:
intro n
  by_cases hn0 : n = 0
  · use 0; simp [hn0]
  · use (RatFunc.X ^ (-WithZero.log n))
    simp [WithZero.exp_log hn0]

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

Goal state before:
pp: X : Scheme
W : X.Opens
hW : IsAffineOpen W
g : ↑Γ(X, toOpens ⟨W, hW⟩)
hV : IsAffineOpen (X.basicOpen g)
f : ↑Γ(X, toOpens ⟨X.basicOpen g, hV⟩)
hU : IsAffineOpen (X.basicOpen f)
⊢ ∃ f_1, X.basicOpen f_1 = toOpens ⟨X.basicOpen f, hU⟩

Tactic:
exact hW.basicOpen_basicOpen_is_basicOpen g f

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

Tactic:
obtain ⟨p', q'⟩ := p'q'

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]⁰
⊢ ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 } *
          { toFractionRing := Localization.mk (p', q').1 (p', q').2 }).liftOn
      (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ =
    { toFractionRing := Localization.mk (p, q).1 (p, q).2 }.liftOn
        (fun n d ↦ if h : φ d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ d, h⟩ } else 0) ⋯ *
      { toFractionRing := Localization.mk (p', q').1 (p', q').2 }.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: case inr
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₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ (p * q') = φ p' * φ q

pp: case inr.hb
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₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q ≠ 0

pp: case inr.hd
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₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q' ≠ 0

Tactic:
mul_comm p,

Goal state after:
case inr
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₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ (q' * p) = φ p' * φ q

case inr.hb
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₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q ≠ 0

case inr.hd
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₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q' ≠ 0
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'q' : R[X] × ↥R[X]⁰
p : R[X]
q : ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)
      ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 } + { toFractionRing := Localization.mk p'q'.1 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:
obtain ⟨p', q'⟩ := p'q'

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]⁰
⊢ (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)
      ({ toFractionRing := Localization.mk (p, q).1 (p, q).2 } +
        { toFractionRing := Localization.mk (p', q').1 (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 }
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]⁰
⊢ φ (↑q * p' + ↑q' * p) * (φ ↑q * φ ↑q') = (φ p * φ ↑q' + φ ↑q * φ p') * φ ↑(q * q')

Tactic:
rw [mul_comm _ p, mul_comm _ p', mul_comm _ (φ p'), add_comm]

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]⁰
⊢ φ (p * ↑q' + p' * ↑q) * (φ ↑q * φ ↑q') = (φ p * φ ↑q' + φ p' * φ ↑q) * φ ↑(q * q')
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
y : ↥K[X]⁰
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } = IsLocalization.mk' K⟮X⟯ x y

Tactic:
IsFractionRing.mk'_eq_div,

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
y : ↥K[X]⁰
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) x / (algebraMap K[X] (FractionRing K[X])) ↑y } =
    IsLocalization.mk' K⟮X⟯ x y
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
y : ↥K[X]⁰
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) x / (algebraMap K[X] (FractionRing K[X])) ↑y } =
    IsLocalization.mk' K⟮X⟯ x y

Tactic:
IsFractionRing.mk'_eq_div,

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
y : ↥K[X]⁰
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) x / (algebraMap K[X] (FractionRing K[X])) ↑y } =
    (algebraMap K[X] K⟮X⟯) x / (algebraMap K[X] K⟮X⟯) ↑y
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x✝ : FractionRing K[X]
x : K[X] × ↥K[X]⁰
⊢ { toFractionRing := Localization.mk x.1 x.2 } =
    (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) K⟮X⟯) (Localization.mk x.1 x.2)

Tactic:
by
      simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
        IsLocalization.map_mk', RingHom.id_apply]

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

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x✝¹ : K⟮X⟯
x✝ : FractionRing K[X]
x : K[X] × ↥K[X]⁰
⊢ { toFractionRing := Localization.mk x.1 x.2 }.toFractionRing =
    (IsLocalization.algEquiv K[X]⁰ K⟮X⟯ (FractionRing K[X])) { toFractionRing := Localization.mk x.1 x.2 }

Tactic:
by
      simp only [Localization.mk_eq_mk'_apply, ofFractionRing_mk', IsLocalization.algEquiv_apply,
        IsLocalization.map_mk', RingHom.id_apply]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ ∀ {p q a : K[X]},
    q ≠ 0 →
      a ≠ 0 →
        (if a * q = 0 then (0, 1)
          else
            let r := gcd (a * p) (a * q);
            (C (a * q / r).leadingCoeff⁻¹ * (a * p / r), C (a * q / r).leadingCoeff⁻¹ * (a * q / r))) =
          if q = 0 then (0, 1)
          else
            let r := gcd p q;
            (C (q / r).leadingCoeff⁻¹ * (p / r), C (q / r).leadingCoeff⁻¹ * (q / r))

Tactic:
intro p q a hq ha
      dsimp
      rw [if_neg hq, if_neg (mul_ne_zero ha hq)]
      have ha' : a.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.mpr ha
      have hainv : a.leadingCoeff⁻¹ ≠ 0 := inv_ne_zero ha'
      simp only [Prod.ext_iff, gcd_mul_left, normalize_apply a, Polynomial.coe_normUnit, mul_assoc,
        CommGroupWithZero.coe_normUnit _ ha']
      have hdeg : (gcd p q).degree ≤ q.degree := degree_gcd_le_right _ hq
      have hdeg' : (Polynomial.C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree := by
        rw [Polynomial.degree_mul, Polynomial.degree_C hainv, zero_add]
        exact hdeg
      have hdivp : Polynomial.C a.leadingCoeff⁻¹ * gcd p q ∣ p :=
        (C_mul_dvd hainv).mpr (gcd_dvd_left p q)
      have hdivq : Polynomial.C a.leadingCoeff⁻¹ * gcd p q ∣ q :=
        (C_mul_dvd hainv).mpr (gcd_dvd_right p q)
      rw [EuclideanDomain.mul_div_mul_cancel ha hdivp, EuclideanDomain.mul_div_mul_cancel ha hdivq,
        leadingCoeff_div hdeg, leadingCoeff_div hdeg', Polynomial.leadingCoeff_mul,
        Polynomial.leadingCoeff_C, div_C_mul, div_C_mul, ← mul_assoc, ← Polynomial.C_mul, ←
        mul_assoc, ← Polynomial.C_mul]
      constructor <;> congr <;>
        rw [inv_div, mul_comm, mul_div_assoc, ← mul_assoc, inv_inv, mul_inv_cancel₀ ha',
          one_mul, inv_div]

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

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
p q : K[X]
hq : q = 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num = C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

pp: case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num = C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)

Tactic:
· simp [hq]

Goal state after:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num = C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
p q : K[X]
hq : q = 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom ∣ q

pp: case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom ∣ q

Tactic:
· simp [hq]

Goal state after:
case neg
K : Type u
inst✝ : Field K
p q : K[X]
hq : ¬q = 0
⊢ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom ∣ q
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
P✝ : StandardEtalePresentation R S
P : StandardEtalePair R
⊢ Function.Bijective ⇑(P.lift P.X ⋯)

Tactic:
simpa [StandardEtalePair.lift_X_left] using Function.bijective_id

Goal state after:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
hp :
  Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬m ^ 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
⊢ (minpoly R x).leadingCoeff ^ (p.natDegree + 2) ≠ 0

Tactic:
simp [minpoly.monic hRx]

Goal state after: