mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case inr.refine_2
P P' : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
h : P' f
hf : P (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    P' f → P (pullback.fst f g) → (∃ R, Z = Spec R) → P g
hZ : ¬∃ R, Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (pullback.snd f ι) (pullback.snd g ι) ≅ pullback (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫
      (pullbackAssoc f g g ι).symm ≪≫ pullback.congrHom ⋯ ⋯ ≪≫ (pullbackRightPullbackFstIso f ι (pullback.fst f g)).symm
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P (pullback.fst (pullback.snd f ι) (pullback.snd g ι))

Tactic:
rw [← heq, P.cancel_left_of_respectsIso]

Goal state after:
case inr.refine_2
P P' : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
inst✝¹ : P'.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec R) (g : Y ⟶ Spec R), P' f → P (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
h : P' f
hf : P (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    P' f → P (pullback.fst f g) → (∃ R, Z = Spec R) → P g
hZ : ¬∃ R, Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (pullback.snd f ι) (pullback.snd g ι) ≅ pullback (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫
      (pullbackAssoc f g g ι).symm ≪≫ pullback.congrHom ⋯ ⋯ ≪≫ (pullbackRightPullbackFstIso f ι (pullback.fst f g)).symm
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P (pullback.snd (pullback.fst f g) (pullback.fst f ι))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: ⊢ ∀ {X Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (pullback.fst f g) → IsOpenImmersion g

Tactic:
intro X

Goal state after:
X : Scheme
⊢ ∀ {Y Z : Scheme} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
    (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (pullback.fst f g) → IsOpenImmersion g
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
⊢ f ((aeval x) p) * f u = 0

Tactic:
← map_mul,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
x : S
f : S →ₐ[R] T
hf : Function.Injective ⇑f
h : IsStronglyTranscendental R (f x)
u : S
p : R[X]
hp : (aeval x) p * u = 0
⊢ f ((aeval x) p * u) = 0
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 : (Ideal.Quotient.mk q) ((aeval x) p) * (Ideal.Quotient.mk q) u = 0
⊢ map (algebraMap R (S ⧸ q)) p * C ((Ideal.Quotient.mk q) u) = 0

Tactic:
← map_mul,

Goal state after:
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 : (Ideal.Quotient.mk q) ((aeval x) p * u) = 0
⊢ map (algebraMap R (S ⧸ q)) p * C ((Ideal.Quotient.mk q) u) = 0
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: case inl
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
g : R[X] := minpoly R a
H : ∀ (i : ℕ), i ≠ g.natDegree → g.coeff i ∈ p
i : ℕ
hi : i < g.natDegree
⊢ (map (Ideal.Quotient.mk p) g).coeff i = (X ^ g.natDegree).coeff i

Tactic:
simpa [hi.ne, Ideal.Quotient.eq_zero_iff_mem] using H _ hi.ne

Goal state after:
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
f : R[X]
hfm : f.Monic
hfa : (aeval (x • a)) f = 0
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
g : R[X] := minpoly R a
H : ∀ (i : ℕ), i ≠ g.natDegree → g.coeff i ∈ p
this : map (Ideal.Quotient.mk p) g = X ^ g.natDegree
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (a ^ (minpoly R a).natDegree) = 0

Tactic:
simpa [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, g] using
        congr(aeval (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p) a) $this).symm

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

Goal state before:
pp: case neg
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
i : ℕ
hi : i ≠ (minpoly R a).natDegree
hip : (minpoly R a).coeff i ∉ p
hx0 : ¬x = 0
⊢ x ∈ p

Tactic:
have := Polynomial.coeff_mem_radical_span_coeff_of_dvd _ _ hfm
    (minpoly.monic (Algebra.IsIntegral.isIntegral _))
    (minpoly.isIntegrallyClosed_dvd (Algebra.IsIntegral.isIntegral _) hfa)

Goal state after:
case neg
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
i : ℕ
hi : i ≠ (minpoly R a).natDegree
hip : (minpoly R a).coeff i ∉ p
hx0 : ¬x = 0
this :
  ∀ (i : ℕ),
    i ≠ (minpoly R (x • a)).natDegree →
      (minpoly R (x • a)).coeff i ∈ (Ideal.span {x | ∃ i < f.natDegree, f.coeff i = x}).radical
⊢ x ∈ p
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 : Ideal S
inst✝⁴ : p.IsPrime
inst✝³ : QuasiFiniteAt R (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p)
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
φ : A ⊗[R] S →ₐ[A] (A ⧸ Ideal.under A q) ⊗[R] (S ⧸ Ideal.map (algebraMap R S) (Ideal.under R p)) :=
  TensorProduct.map (Ideal.Quotient.mkₐ A (Ideal.under A q))
    (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))
hφ₁ : Function.Surjective ⇑φ
hφ₂ : RingHom.ker φ.toRingHom = Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
hφ₃ :
  φ.comp TensorProduct.includeRight.toRingHom =
    TensorProduct.includeRight.comp (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p)))
this : (Ideal.map φ.toRingHom q).IsPrime
⊢ Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (Ideal.under R p))) p =
    Ideal.comap TensorProduct.includeRight.toRingHom (Ideal.map φ.toRingHom q)

Tactic:
apply Ideal.comap_injective_of_surjective _ Ideal.Quotient.mk_surjective
    rwa [Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective, Ideal.comap_comap,
      ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, sup_eq_left.mpr Ideal.map_comap_le,
      ← hφ₃, ← Ideal.comap_comap, Ideal.comap_map_of_surjective _ (by exact hφ₁),
      ← RingHom.ker_eq_comap_bot, hφ₂, sup_eq_left.mpr Ideal.map_comap_le]

Goal state after:
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 : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ p ≤
    Ideal.comap (algebraMap R (Localization.AtPrime p))
      (Ideal.comap (↑(IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq)) (Ideal.map (algebraMap R Sq) p))

Tactic:
Ideal.comap_comap

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : p.IsPrime
inst✝² : q.LiesOver p
Q : Ideal (p.Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt p.ResidueField Q
Sq : Type u_2 := Localization.AtPrime q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ p ≤
    Ideal.comap ((↑(IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq)).comp (algebraMap R (Localization.AtPrime p)))
      (Ideal.map (algebraMap R Sq) p)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
⊢ id (IsLocallyArtinian X)

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y],
    (∃ R, Y = Spec R) → (∃ S, X = Spec S) → id (IsLocallyArtinian X)
hX : ¬∃ S, X = Spec S
⊢ id (IsLocallyArtinian X)

X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyQuasiFinite f
inst✝ : IsLocallyArtinian Y
hY : ∃ R, Y = Spec R
hX : ∃ S, X = Spec S
⊢ id (IsLocallyArtinian X)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian (Spec R)
⊢ id (IsFinite f)

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian (Spec R)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyQuasiFinite f] [QuasiCompact f]
    [IsLocallyArtinian (Spec R)], (∃ S, X = Spec S) → id (IsFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (IsFinite f)

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : LocallyQuasiFinite f
inst✝¹ : QuasiCompact f
inst✝ : IsLocallyArtinian (Spec R)
hX : ∃ S, X = Spec S
⊢ id (IsFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R),
    (∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) →
      (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
hX : ∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥(Spec R)), IsDiscrete (⇑f ⁻¹' {x})
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥(Spec R)), IsDiscrete (⇑f ⁻¹' {x})
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∀ (x : ↥(Spec R)), IsDiscrete (⇑f ⁻¹' {x})) → (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
H : ∀ (x : ↥(Spec R)), IsDiscrete (⇑f ⁻¹' {x})
hX : ∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), (⇑f ⁻¹' {x}).Finite
⊢ id (LocallyQuasiFinite f)

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), (⇑f ⁻¹' {x}).Finite
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFiniteType f],
    (∀ (x : ↥(Spec R)), (⇑f ⁻¹' {x}).Finite) → (∃ S, X = Spec S) → id (LocallyQuasiFinite f)
hX : ¬∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
hf : ∀ (x : ↥(Spec R)), (⇑f ⁻¹' {x}).Finite
hX : ∃ S, X = Spec S
⊢ id (LocallyQuasiFinite f)
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:
← map_mul,

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
⊢ φ (p * q') = φ 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 H.H.refine_3
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]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : φ y✝.1 * φ ↑a'.2 = φ a'.1 * φ ↑y✝.2
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1

Tactic:
← map_mul,

Goal state after:
case H.H.refine_3
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]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : φ (y✝.1 * ↑a'.2) = φ a'.1 * φ ↑y✝.2
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H.refine_3
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]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : φ (y✝.1 * ↑a'.2) = φ a'.1 * φ ↑y✝.2
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1

Tactic:
← map_mul,

Goal state after:
case H.H.refine_3
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]⁰
h : φ y✝.1 / φ ↑y✝.2 = φ a'.1 / φ ↑a'.2
this : φ (y✝.1 * ↑a'.2) = φ (a'.1 * ↑y✝.2)
⊢ ↑(a'.1, a'.2).2 * (y✝.1, y✝.2).1 = ↑(y✝.1, y✝.2).2 * (a'.1, a'.2).1
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inl
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 0) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ 0)

pp: case inr
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ q)

Tactic:
· have : (0 : K⟮X⟯) = algebraMap K[X] _ 0 / algebraMap K[X] _ 1 := by simp
    rw [map_zero, map_zero, map_zero, div_zero, div_zero, this, map_apply_div_ne_zero, map_one,
      map_one, div_one, map_zero, map_zero]
    exact one_ne_zero

Goal state after:
case inr
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p q : K[X]
hq : q ≠ 0
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ q)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
x : ↥X
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
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩}

X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
hX : ∃ S, X = Spec S
⊢ QuasiFiniteAt f x ↔ IsOpen {⟨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
x : S
h : P.HasMap x
p₁ p₂ : R[X]
n : ℕ
e : derivative P.f * p₁ + P.f * p₂ = P.g ^ n
⊢ (aeval x) P.g ^ n = (aeval x) (derivative P.f) * ?m.78

Tactic:
simpa [h.1] using congr(aeval x $e.symm)

Goal state after:
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
⊢ (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) (CAlgHom P.g) *
      (Ideal.Quotient.mk (Ideal.span {C P.f, Y * C P.g - 1})) Y =
    1

Tactic:
← map_mul,

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 (Ideal.span {C P.f, Y * C P.g - 1})) (CAlgHom P.g * 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 : (Ideal.Quotient.mkₐ R I) ((aeval x) P.g) * (Ideal.Quotient.mkₐ R I) a = 1
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)

Tactic:
← map_mul,

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 : (Ideal.Quotient.mkₐ R I) ((aeval x) P.g * a) = 1
⊢ ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)
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⟯) (p / gcd p q) * (algebraMap K[X] K⟮X⟯) q =
    (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) (q / gcd p q)

pp: 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

pp: 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

pp: 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

Tactic:
← map_mul,

Goal state after:
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⟯) (p / gcd p q * q) = (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) (q / gcd p q)

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