mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
⊢ Ideal.map e.toRingEquiv.symm P.ker =
    (Algebra.Generators.ofSurjective (fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) ⋯).ker

Tactic:
Ideal.map_symm

Goal state after:
n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
⊢ Ideal.comap e.toRingEquiv P.ker =
    (Algebra.Generators.ofSurjective (fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) ⋯).ker
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ Submodule.restrictScalars P.Ring (Submodule.span S (Set.range fun x ↦ Extension.Cotangent.mk (v x))) = ⊤

Tactic:
rw [Submodule.restrictScalars_eq_top_iff]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ Submodule.span S (Set.range fun x ↦ Extension.Cotangent.mk (v x)) = ⊤
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.negAddY P Q / W.addZ P Q =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
negAddY_eq hP hQ hPz hQz,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ((P y * Q z - Q y * P z) *
            ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                      W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                    W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
                  P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
                Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
          P y * Q z * (P x * Q z - Q x * P z) ^ 3) /
        (P z * Q z) ^ 2 /
      W.addZ P Q =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : FaithfulSMul R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsIntegrallyClosed R
⊢ Algebra.HasGoingDown R S

Tactic:
have := (FaithfulSMul.algebraMap_injective R S).isDomain

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : FaithfulSMul R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsIntegrallyClosed R
this : IsDomain R
⊢ Algebra.HasGoingDown R S
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
⊢ x ∈ p

Tactic:
obtain ⟨f, hfm, hfa, hf⟩ := exists_monic_aeval_eq_zero_forall_mem_of_mem_map ha

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx : x ∈ Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p)
a : S
ha : x • a ∈ Ideal.map (algebraMap R S) p
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
⊢ x ∈ p
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : K[X]
⊢ (Polynomial.aeval X) p = (algebraMap K[X] K⟮X⟯) p

Tactic:
induction p using Polynomial.induction_on'

Goal state after:
case add
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p✝ q✝ : K[X]
a✝¹ : (Polynomial.aeval X) p✝ = (algebraMap K[X] K⟮X⟯) p✝
a✝ : (Polynomial.aeval X) q✝ = (algebraMap K[X] K⟮X⟯) q✝
⊢ (Polynomial.aeval X) (p✝ + q✝) = (algebraMap K[X] K⟮X⟯) (p✝ + q✝)

case monomial
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
n✝ : ℕ
a✝ : K
⊢ (Polynomial.aeval X) ((Polynomial.monomial n✝) a✝) = (algebraMap K[X] K⟮X⟯) ((Polynomial.monomial n✝) a✝)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
⊢ IsAlmostIntegral R (p.coeff i)

Tactic:
by_cases hp' : p.natDegree = 0

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : p.natDegree = 0
⊢ IsAlmostIntegral R (p.coeff i)

case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsDomain R
inst✝ : FaithfulSMul R S
i : ℕ
H : ∀ {q : S[X]}, IsAlmostIntegral R[X] q → IsAlmostIntegral R q.leadingCoeff
n : ℕ
IH : ∀ m < n, ∀ {p : S[X]}, IsAlmostIntegral R[X] p → p.natDegree = m → IsAlmostIntegral R (p.coeff i)
p : S[X]
hp : IsAlmostIntegral R[X] p
hn : p.natDegree = n
hp' : ¬p.natDegree = 0
⊢ IsAlmostIntegral R (p.coeff i)
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_3
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
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField) X)) ⋯).comp { toRingHom := f, commutes' := ⋯ } =
    AlgHom.id I.ResidueField J.ResidueField

Tactic:
apply AlgHom.coe_ringHom_injective
    ext
    · simp [f, RatFunc.liftAlgHom, ← IsScalarTower.algebraMap_apply]; rfl
    · simp [f, RatFunc.liftAlgHom]

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
P : Ideal ↑R
hP : P.IsPrime
this : LocallyQuasiFinite (Spec.map (CommRingCat.ofHom (algebraMap P.ResidueField (P.Fiber ↑S))))
⊢ Module.Finite P.ResidueField (P.Fiber ↑S)

Tactic:
simp only [HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), CommRingCat.hom_ofHom,
      RingHom.quasiFinite_algebraMap] at this

Goal state after:
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
P : Ideal ↑R
hP : P.IsPrime
this : Algebra.QuasiFinite P.ResidueField (P.Fiber ↑S)
⊢ Module.Finite P.ResidueField (P.Fiber ↑S)
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]⁰
⊢ (if h : φ ↑(q * q') ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ (p * p')) ⟨φ ↑(q * q'), h⟩ } else 0) =
    (if h : φ ↑q ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ p) ⟨φ ↑q, h⟩ } else 0) *
      if h : φ ↑q' ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ p') ⟨φ ↑q', h⟩ } else 0

Tactic:
dif_pos hq,

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]⁰
⊢ (if h : φ ↑(q * q') ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ (p * p')) ⟨φ ↑(q * q'), h⟩ } else 0) =
    { toFractionRing := Localization.mk (φ p) ⟨φ ↑q, hq⟩ } *
      if h : φ ↑q' ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ p') ⟨φ ↑q', h⟩ } else 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f],
    (∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
x✝ : ↥(pullback f (Y.affineCover.f i))
⊢ x✝ ∈ ⇑(pullback.snd f (Y.affineCover.f i)) ⁻¹' {x} ↔
    x✝ ∈ ⇑(pullback.fst f (Y.affineCover.f i)) ⁻¹' ⇑f ⁻¹' {(Y.affineCover.f i) x}

Tactic:
simp [← (Y.affineCover.f i).isOpenEmbedding.injective.eq_iff, ← Scheme.Hom.comp_apply,
      -Hom.comp_base, pullback.condition]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f],
    (∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
x✝ : ↥(pullback f (Y.affineCover.f i))
⊢ x✝ ∈ ⇑(pullback.snd f (Y.affineCover.f i)) ⁻¹' {x} ↔
    x✝ ∈ ⇑(pullback.fst f (Y.affineCover.f i)) ⁻¹' ⇑f ⁻¹' {(Y.affineCover.f i) x}

Tactic:
simp [← (Y.affineCover.f i).isOpenEmbedding.injective.eq_iff, ← Scheme.Hom.comp_apply,
      -Hom.comp_base, pullback.condition]

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]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
⊢ RatFunc.liftOn 1 (fun p q ↦ φ p / φ q) ⋯ = 1

Tactic:
simp_rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk,
      OneMemClass.coe_one, map_one, div_one]

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]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * (C a.leadingCoeff⁻¹⁻¹ * (p / gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q) ∧
    C (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * (C a.leadingCoeff⁻¹⁻¹ * (q / gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)

Tactic:
← mul_assoc,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ C (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * C a.leadingCoeff⁻¹⁻¹ * (p / gcd p q) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (p / gcd p q) ∧
    C (q.leadingCoeff / (a.leadingCoeff⁻¹ * (gcd p q).leadingCoeff))⁻¹ * (C a.leadingCoeff⁻¹⁻¹ * (q / gcd p q)) =
      C (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹ * (q / gcd p q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff⁻¹⁻¹ * (a.leadingCoeff⁻¹ * ((gcd p q).leadingCoeff / q.leadingCoeff)) =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

Tactic:
← mul_assoc,

Goal state after:
case left.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff⁻¹⁻¹ * a.leadingCoeff⁻¹ * ((gcd p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case right.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff⁻¹⁻¹ * (a.leadingCoeff⁻¹ * ((gcd p q).leadingCoeff / q.leadingCoeff)) =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹

Tactic:
← mul_assoc,

Goal state after:
case right.e_a.e_6
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q a : K[X]
hq : q ≠ 0
ha : a ≠ 0
ha' : a.leadingCoeff ≠ 0
hainv : a.leadingCoeff⁻¹ ≠ 0
hdeg : (gcd p q).degree ≤ q.degree
hdeg' : (C a.leadingCoeff⁻¹ * gcd p q).degree ≤ q.degree
hdivp : C a.leadingCoeff⁻¹ * gcd p q ∣ p
hdivq : C a.leadingCoeff⁻¹ * gcd p q ∣ q
⊢ a.leadingCoeff⁻¹⁻¹ * a.leadingCoeff⁻¹ * ((gcd p q).leadingCoeff / q.leadingCoeff) =
    (q.leadingCoeff / (gcd p q).leadingCoeff)⁻¹
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (if 0 = 0 then (0, 1)
    else
      have r := gcd p 0;
      (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) =
    if 1 = 0 then (0, 1)
    else
      have r := gcd 0 1;
      (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Tactic:
if_pos rfl,

Goal state after:
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (0, 1) =
    if 1 = 0 then (0, 1)
    else
      have r := gcd 0 1;
      (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom = x

Tactic:
induction x using RatFunc.induction_on with | _ p q hq

Goal state after:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num /
      (algebraMap K[X] K⟮X⟯) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
rw [num_div p q, denom_div p hq, map_mul, map_mul, mul_div_mul_left,
    div_eq_div_iff, ← map_mul, ← map_mul, mul_comm _ q, ←
    EuclideanDomain.mul_div_assoc, ← EuclideanDomain.mul_div_assoc, mul_comm]

Goal state after:
case f.h
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ gcd p q ∣ q

case f.h
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ gcd p q ∣ p

case f.hb
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (q / gcd p q) ≠ 0

case f.hd
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0

case f.hc
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ IsCoprime x.num x.denom

Tactic:
induction x using RatFunc.induction_on with | _ p q hq

Goal state after:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ IsCoprime ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).num
    ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).denom
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom +
        (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom) =
    (algebraMap K[X] K⟮X⟯) (x.num * y.denom + x.denom * y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)

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

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

Tactic:
map_add,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom +
        (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom) =
    ((algebraMap K[X] K⟮X⟯) (x.num * y.denom) + (algebraMap K[X] K⟮X⟯) (x.denom * y.num)) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)

case hb
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.denom ≠ 0

case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_2
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
⊢ IsUnit ((aeval ((Ideal.Quotient.mk I) (x + (aeval x) P.f * -b))) P.g)

Tactic:
map_add,

Goal state after:
case refine_2
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
⊢ IsUnit ((aeval ((Ideal.Quotient.mk I) x + (Ideal.Quotient.mk I) ((aeval x) P.f * -b))) P.g)