mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker *
      Ideal.map ((localizationAway T g).toComp P).toAlgHom P.ker ≤
    RingHom.ker (compLocalizationAwayAlgHom T g P)

Tactic:
← Ideal.map_mul,

Goal state after:
case a.a
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
hsple :
  ∀ {x : ((localizationAway T g).comp P).Ring},
    x ∈ Ideal.span {(rename Sum.inr) (P.σ g) * X (Sum.inl ()) - 1} → (compLocalizationAwayAlgHom T g P) x = 0
⊢ Ideal.map ((localizationAway T g).toComp P).toAlgHom (P.ker * P.ker) ≤ RingHom.ker (compLocalizationAwayAlgHom T g P)
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
⊢ IsStandardSmooth R S ↔ Subsingleton (H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(D R S)

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, ?_⟩, fun ⟨h, ⟨_, b, hb⟩⟩ ↦ .of_basis_kaehlerDifferential b hb⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FinitePresentation R S
h : IsStandardSmooth R S
⊢ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(D R S)
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
have : eₚ = b.repr.symm := by
    ext i
    trans IsLocalizedModule.map p.primeCompl l₁ l₂ e <| l₁ <| Finsupp.single i 1
    · simp [eₚ, -IsLocalizedModule.map_apply, l₁]
    · simp [l₂, e, hb]

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
h : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this : eₚ = ↑b.repr.symm
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
⊢ Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Tactic:
refine IsLocalizedModule.injective_of_map_zero (Submonoid.powers g)
    (TensorProduct.mk S T P.toExtension.Cotangent 1) (fun x hx ↦ ?_)

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : P.toExtension.Cotangent
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) x) =
    0
⊢ ((TensorProduct.mk S T P.toExtension.Cotangent) 1) x = 0
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk ⟨(AlgHom.id R P.Ring).toRingHom ↑x, ⋯⟩ = Extension.Cotangent.mk ⟨↑x, ⋯⟩

Tactic:
AlgHom.toRingHom_eq_coe,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk ⟨↑(AlgHom.id R P.Ring) ↑x, ⋯⟩ = Extension.Cotangent.mk ⟨↑x, ⋯⟩
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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ D.cotangentEquivProd.symm (0, D.basisLeft r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
cotangentEquivProd_symm_apply,

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ (cotangentCompLocalizationAwayEquiv D.gbar D.presLeft.toGenerators ⋯).symm (D.basisLeft r, 0) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
by
  let := (f.appLE U V hVU).hom.toAlgebra
  let p := (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal
  let q := (hV.primeIdealOf ⟨x, hx⟩).asIdeal
  have : q.LiesOver p :=
    ⟨congr($(IsAffineOpen.comap_primeIdealOf_appLE U hU V hV hVU hx).1).symm⟩
  let := Localization.AtPrime.algebraOfLiesOver p q
  trans Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)
  · rw [← formallySmooth_algebraMap]
    exact RingHom.FormallySmooth.respectsIso.arrow_mk_iso_iff
      (IsAffineOpen.arrowStalkMapIso f U hU V hV hVU hx)
  · exact Algebra.FormallySmooth.iff_restrictScalars.symm

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (@LocallyOfFiniteType ⊓ @FormallyUnramified) f → diagonal (@Etale) f

Tactic:
⟨hft, hfu⟩

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hft : LocallyOfFiniteType f
hfu : FormallyUnramified f
⊢ diagonal (@Etale) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P' ((T.isoSpec.inv ≫ p) ≫ f)

Tactic:
rw [Category.assoc, P'.cancel_left_of_respectsIso]

Goal state after:
case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P' (p ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case a
P P' : MorphismProperty Scheme
inst✝³ : P'.RespectsIso
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H : ∀ {R : CommRingCat} {S X : Scheme} (f : Spec R ⟶ S) (g : X ⟶ S), P' f → P (pullback.fst f g) → P g
X Y Z T : Scheme
inst✝ : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (pullback.fst f g)
⊢ P' (p ≫ f)

Tactic:
exact P'.comp_mem _ _ hp h

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
Y : Scheme
g : Y ⟶ Spec R
hfst : IsIso (pullback.fst (Spec.map φ) g)
this : IsAffine Y
hY : ∃ T, Y = Spec T
⊢ isomorphisms Scheme g

Tactic:
obtain ⟨T, rfl⟩ := hY

Goal state after:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
g : Spec T ⟶ Spec R
hfst : IsIso (pullback.fst (Spec.map φ) g)
this : IsAffine (Spec T)
⊢ isomorphisms Scheme g
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
g : Spec T ⟶ Spec R
hfst : IsIso (pullback.fst (Spec.map φ) g)
this : IsAffine (Spec T)
⊢ isomorphisms Scheme g

Tactic:
obtain ⟨ψ, rfl⟩ := Spec.map_surjective g

Goal state after:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine (Spec T)
ψ : R ⟶ T
hfst : IsIso (pullback.fst (Spec.map φ) (Spec.map ψ))
⊢ isomorphisms Scheme (Spec.map ψ)
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Ideal

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
x : S
h✝ : Nontrivial R
p : (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x}))[X]
hp : p.Monic
q : R[X] := ∑ i ∈ Finset.range (p.natDegree + 1), C ((↑(p.coeff i)).coeff (p.natDegree - i)) * X ^ i
hq : q.natDegree = p.natDegree
e :
  ∑ b ∈ Finset.range (p.natDegree + 1),
      ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff b) * (C x * X) ^ b).coeff
        p.natDegree =
    0
i : ℕ
hi : i ≤ p.natDegree
⊢ x ^ i * (algebraMap R S) ((↑(p.coeff i)).coeff (p.natDegree - i)) =
    x ^ i * ((algebraMap (↥(Algebra.adjoin R {x | ∃ r ∈ I, C r * X = x})) S[X]) (p.coeff i)).coeff (p.natDegree - i)

Tactic:
simp [Subalgebra.algebraMap_def]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
f : K⟮X⟯
⊢ (∃ x, Polynomial.C x = f.num) ∧ f.denom.natDegree = 0 → ∃ c, f = C c

Tactic:
Polynomial.natDegree_eq_zero

Goal state after:
K : Type u
inst✝ : Field K
f : K⟮X⟯
⊢ ((∃ x, Polynomial.C x = f.num) ∧ ∃ x, Polynomial.C x = f.denom) → ∃ c, f = C c
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
f : K⟮X⟯
a : K
ha : Polynomial.C a = f.num
b : K
hb : Polynomial.C b = f.denom
⊢ f = C (a / b)

Tactic:
rw [← num_div_denom f, ← ha, ← hb, algebraMap_C, algebraMap_C, map_div₀]

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

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
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ Ideal.under R p ≤
    Ideal.comap (f.comp (algebraMap R (Localization.AtPrime p)))
      (Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
AlgHom.toRingHom_eq_coe,

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
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : QuasiFinite R (Localization.AtPrime p ⧸ Ideal.map (algebraMap R (Localization.AtPrime p)) (Ideal.under R p))
q : Ideal T
inst✝ : q.IsPrime
f : Localization.AtPrime p →ₐ[R] Localization.AtPrime q
hf : Function.Surjective ⇑f
⊢ Ideal.under R p ≤
    Ideal.comap ((↑f).comp (algebraMap R (Localization.AtPrime p)))
      (Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
Module: Mathlib.RingTheory.QuasiFinite.Weakly

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 : 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.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ q.primeCompl
⊢ 1 ⊗ₜ[R] s ∈ Q.primeCompl

Tactic:
simpa [← hQ] using hs

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.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
φ₂ : p.Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) p)) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p := IsLocalization.liftAlgHom ⋯
this : Function.Surjective ⇑φ₃
inst : QuasiFiniteAt R Q
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
obtain rfl := q.over_def p

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
q : Ideal S
inst✝⁴ : q.IsPrime
Sq : Type u_2 := Localization.AtPrime q
inst✝³ : (Ideal.under R q).IsPrime
inst✝² : q.LiesOver (Ideal.under R q)
Q : Ideal ((Ideal.under R q).Fiber S)
inst✝¹ : Q.IsPrime
hQ : Ideal.comap TensorProduct.includeRight.toRingHom Q = q
inst✝ : QuasiFiniteAt (Ideal.under R q).ResidueField Q
this✝ : Algebra (Localization.AtPrime (Ideal.under R q)) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R q) q
φ₁ : (Ideal.under R q).ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) (Ideal.under R q) :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) (Ideal.under R q))
    (IsScalarTower.toAlgHom R (Localization.AtPrime (Ideal.under R q)) Sq) ⋯
φ₂ : (Ideal.under R q).Fiber S →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) (Ideal.under R q) :=
  TensorProduct.lift φ₁ (IsScalarTower.toAlgHom R S (Sq ⧸ Ideal.map (algebraMap R Sq) (Ideal.under R q))) ⋯
φ₃ : Localization.AtPrime Q →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) (Ideal.under R q) := IsLocalization.liftAlgHom ⋯
this : Function.Surjective ⇑φ₃
inst : QuasiFiniteAt R Q
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
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]⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
⊢ (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:
simp only [Submonoid.mem_comap.mp (hφ hq), Submonoid.mem_comap.mp (hφ hq'),
        dif_pos, ofFractionRing.injEq, Localization.mk_eq_mk_iff]
      refine Localization.r_of_eq ?_
      simpa only [map_mul] using congr_arg φ h

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
haV : a ∈ ↑V
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
⊢ (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯ ≫ pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι) ⟨a, hxf⟩ =
    ↑((TopCat.Hom.hom (pullback.fst (↑U).ι (↑V).ι).base) x)

Tactic:
simp only [pullback.lift_fst_assoc, homOfLE_ι, Opens.ι_apply]

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
haV : a ∈ ↑V
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
⊢ a = ↑((TopCat.Hom.hom (pullback.fst (↑U).ι (↑V).ι).base) x)
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]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝¹ y✝ : R[X] × ↥R[X]⁰
⊢ ({ toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } * { toFractionRing := Localization.mk y✝.1 y✝.2 }).liftOn
      (fun p q ↦ φ p / φ q) ⋯ =
    { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯ *
      { toFractionRing := Localization.mk y✝.1 y✝.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯

Tactic:
rw [← ofFractionRing_mul, Localization.mk_mul]

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]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝¹ y✝ : R[X] × ↥R[X]⁰
⊢ { toFractionRing := Localization.mk (y✝¹.1 * y✝.1) (y✝¹.2 * y✝.2) }.liftOn (fun p q ↦ φ p / φ q) ⋯ =
    { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯ *
      { toFractionRing := Localization.mk y✝.1 y✝.2 }.liftOn (fun p q ↦ φ p / φ q) ⋯
Module: Mathlib.FieldTheory.RatFunc.Basic

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

Tactic:
AlgHom.toRingHom_eq_coe,

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

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

Tactic:
simp only [map_add, map_mul, map_pow] at e

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

Goal state before:
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:
· exact algebraMap_ne_zero (denom_ne_zero x)

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