mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
⊢ D.P.coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
rw [Subalgebra.setRange_algebraMap]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
⊢ D.P.coeffs ⊆ ↑(subalgebra R D)
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
i : D.vars
this : ↑(D.h i).coeffs ⊆ ⋃ i, ↑(D.h i).coeffs
⊢ ↑(D.h i).coeffs ⊆ Set.range ⇑(algebraMap (↥(subalgebra R D)) A)

Tactic:
rw [Subalgebra.setRange_algebraMap]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
i : D.vars
this : ↑(D.h i).coeffs ⊆ ⋃ i, ↑(D.h i).coeffs
⊢ ↑(D.h i).coeffs ⊆ ↑(subalgebra R D)
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_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ S ⊗[D.T] D.presLeft.toExtension.Cotangent ≃ₗ[S] P.toExtension.Cotangent

Tactic:
refine LinearEquiv.ofLinearMap D.tensorCotangentHom D.tensorCotangentInv ?_ ?_
  · refine b.ext fun i ↦ ?_
    simpa only [LinearMap.coe_comp, Function.comp_apply, tensorCotangentInv_apply,
      tensorCotangentHom_tmul] using! D.hf (b i)
  · ext : 2
    refine LinearMap.ext_on_range D.span_range_mk_kerGen fun i ↦ ?_
    simp [-toExtension_commRing, -toExtension_Ring, -toExtension_algebra₂, tensorCotangentHom_tmul,
      kerGen, D.hf]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6
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
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ ((localizationAway S D.gbar).ofComp
          (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
              ⋯).toGenerators).toAlgHom
      ((rename Sum.inr)
            ((Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ
              D.gbar) *
          X (Sum.inl ()) -
        1) =
    C D.gbar * X () - 1

Tactic:
exact Generators.toAlgHom_ofComp_localizationAway _ _

Goal state after:
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
inst✝ : Nontrivial S
i : σ
⊢ D.basis (Sum.inr i) = D.cotangentEquivProd.symm (0, D.basisLeft i)

Tactic:
by
  simp [basis]

Goal state after:
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 : σ
⊢ (LinearMap.liftBaseChange S
        (Extension.Cotangent.map ((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom))
      ((b.map D.tensorCotangentEquiv.symm) r) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
Module.Basis.map_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 : σ
⊢ (LinearMap.liftBaseChange S
        (Extension.Cotangent.map ((localizationAway S D.gbar).toComp D.presLeft.toGenerators).toExtensionHom))
      (D.tensorCotangentEquiv.symm (b r)) =
    Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ f = g

Tactic:
suffices IsIso (equalizer.ι f g) from Limits.eq_of_epi_equalizer

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝³ : (isomorphisms C).DescendsAlong P
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
hv : P v
H : pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯ = pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ IsIso (equalizer.ι f g)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K

Tactic:
have : ExpChar k p := .prime hp.out

Goal state after:
case inr
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : PerfectField k
inst✝ : Algebra.EssFiniteType k K
p : ℕ
hp : Fact (Nat.Prime p)
hpk : CharP k p
this : ExpChar k p
⊢ ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(adjoin k ↑s)) K
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
⊢ IsOpenImmersion g

Tactic:
let f' := pullback.snd f U.ι

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ ↑U := pullback.snd f U.ι
⊢ IsOpenImmersion g
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this✝ : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
this : v y ^ p.natDegree = 0
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ v ((aeval y) p) = 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ p ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: 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✝)

Tactic:
simp_all

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

Goal state before:
pp: 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✝)

Tactic:
simp_all

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

Goal state before:
pp: K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
⊢ eval f a (x + y) = eval f a x + eval f a y

Tactic:
by
  unfold eval
  by_cases hxy : Polynomial.eval₂ f a (denom (x + y)) = 0
  · have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_add_dvd x y) hxy
    rw [Polynomial.eval₂_mul] at this
    cases mul_eq_zero.mp this <;> contradiction
  rw [div_add_div _ _ hx hy, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ←
    div_eq_mul_inv, div_eq_iff hxy]
  simp only [← Polynomial.eval₂_mul, ← Polynomial.eval₂_add]
  congr 1
  apply num_denom_add

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
i : ℕ
h0 : p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) → v ((algebraMap K[X] K⟮X⟯) ((monomial i) (p.coeff i))) ≤ 1

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ IsIntegral R (p.coeff i)

Tactic:
rw [hm, Multiset.prod_eq_prod_coe, coeff_C_mul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ IsIntegral R (p.leadingCoeff * (∏ x, x.fst).coeff i)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R[X]
q : S[X]
hp : p.Monic
hq : q.Monic
H : q ∣ map (algebraMap R S) p
i : ℕ
a✝ : Nontrivial S
T : Type u_2
w✝⁴ : CommRing T
w✝³ : Algebra S T
w✝² : Module.Finite S T
w✝¹ : Module.Free S T
w✝ : Nontrivial T
hqT : (map (algebraMap S T) q).Splits
algInst✝ : Algebra R T := ((algebraMap S T).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
x : T
hx : (map (algebraMap S T) q).IsRoot x
⊢ (aeval x) q = 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i✝ : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
i : ℕ
hi : i ∈ q.support
⊢ (q.coeff i).natDegree < m

pp: case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i✝ : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
i : ℕ
hi : i ∉ q.support
⊢ (q.coeff i).natDegree < m

Tactic:
· exact (Finset.le_sup (f := fun i ↦ (q.coeff i).natDegree) hi).trans_lt (by lia)

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i✝ : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
i : ℕ
hi : i ∉ q.support
⊢ (q.coeff i).natDegree < m
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : (algebraMap (MvPolynomial β R) (MvPolynomial β S)).IsIntegralElem f
n : β →₀ ℕ
this : IsIntegral R (coeff (Finsupp.embDomain e.symm.toEmbedding n) ((rename ⇑e.symm) f))
⊢ IsIntegral R (coeff n f)

Tactic:
simpa [Finsupp.embDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective] using! this

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
⊢ id (LocallyQuasiFinite f)

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
hf : ∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    (∀ (x : ↥Y), LocallyQuasiFinite (Hom.fiberToSpecResidueField f x)) → (∃ R, Y = Spec R) → id (LocallyQuasiFinite f)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
x : ↥(Y.affineCover.X i)
⊢ LocallyQuasiFinite (Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) x)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p } ≠ 0
hp : p = 0
⊢ { toFractionRing := 0 } = 0

Tactic:
ofFractionRing_zero

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p } ≠ 0
hp : p = 0
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

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

Tactic:
change id _ -- avoid typeclass synthesis from getting stuck on the wlog hypothesis.
  wlog hY : ∃ R, Y = Spec R
  · refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩
    have (x : Y) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
    refine (MorphismProperty.cancel_right_of_respectsIso @LocallyQuasiFinite _
      (Spec.map ((Y.affineCover.f i).residueFieldMap _))).mp ?_
    let g : (pullback.snd f (Y.affineCover.f i)).fiber x ⟶ f.fiber (Y.affineCover.f i x) :=
      pullback.map _ _ _ _ (pullback.fst _ _) (Spec.map ((Y.affineCover.f i).residueFieldMap _))
        (Y.affineCover.f i) (by simp [pullback.condition]) (by simp)
    have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)
    convert! (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _) using 1
    simp [g, Hom.fiberToSpecResidueField]
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦
      this _ _ (fun x ↦ ?_) ⟨_, rfl⟩
    have (x : _) : IsLocallyArtinian (f.fiber x) :=
      .of_locallyQuasiFinite (f.fiberToSpecResidueField x)
    let g : (X.affineCover.f i ≫ f).fiber x ⟶ f.fiber x :=
      pullback.map _ _ _ _ (X.affineCover.f i) (𝟙 _) (𝟙 _) (by simp) (by simp)
    have : IsClosedImmersion g := .of_isPreimmersion _ (isClosed_discrete _)
    convert (inferInstance : LocallyQuasiFinite <| g ≫ f.fiberToSpecResidueField _)
    simp [g, Hom.fiberToSpecResidueField]
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  algebraize [φ.hom]
  simp only [HasRingHomProperty.Spec_iff, id_eq]
  refine ⟨fun P hP ↦ ?_⟩
  suffices LocallyQuasiFinite (Spec.map <|
      CommRingCat.ofHom <| algebraMap P.ResidueField (P.Fiber S)) by
    simp only [HasRingHomProperty.Spec_iff (P := @LocallyQuasiFinite), CommRingCat.hom_ofHom,
      RingHom.quasiFinite_algebraMap] at this
    exact .of_quasiFinite
  obtain ⟨x, rfl⟩ : ∃ x : Spec R, P = x.asIdeal := ⟨⟨P, hP⟩, rfl⟩
  refine (MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk ?_ ?_ ?_)).mp (hf x)
  · refine asIso (pullback.map _ _ _ _ (𝟙 _) (Spec.map (Spec.residueFieldIso _ x).inv) (𝟙 _)
      ?_ ?_) ≪≫ pullbackSymmetry _ _ ≪≫ pullbackSpecIso ..
    · simp; rfl
    · simp [← Spec.map_comp, fromSpecResidueField, Spec.fromSpecStalk_eq]
  · exact asIso (Spec.map (Spec.residueFieldIso _ x).inv)
  · simp [Hom.fiberToSpecResidueField]

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

Goal state before:
pp: case inr
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
⊢ id (LocallyQuasiFinite f)

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩

Goal state after:
case inr
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)
⊢ IsDiscrete (⇑(pullback.snd f (Y.affineCover.f i)) ⁻¹' {x})
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: case inr
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
⊢ id (LocallyQuasiFinite f)

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover Y.affineCover).mpr fun i ↦
      this (f := pullback.snd _ _) (fun x ↦ ?_) ⟨_, rfl⟩

Goal state after:
case inr
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)
⊢ (⇑(pullback.snd f (Y.affineCover.f i)) ⁻¹' {x}).Finite
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
⊢ { I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
X : Scheme
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.f i)) ∧
    ∀ (i : { I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.I₀),
      IsOpenImmersion ({ I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.f i)
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H✝ : f P.X = g P.X
H :
  (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))).comp CAlgHom
H' : aeval P.X = (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1})).comp CAlgHom
⊢ (f.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))) Y =
    (g.comp (Ideal.Quotient.mkₐ R (Ideal.span {C P.f, Y * C P.g - 1}))) Y

Tactic:
change f.toMonoidHom (Ideal.Quotient.mk _ .X) = g.toMonoidHom (Ideal.Quotient.mk _ .X)

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

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this✝ : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
this :
  (↑e₀).comp (Algebra.TensorProduct.map (AlgHom.id R (MvPolynomial σ R)) (integralClosure R B).val) =
    (MvPolynomial.mapAlgHom (integralClosure R B).val).comp ↑e₁
⊢ e₀ ((Algebra.TensorProduct.map (AlgHom.id (MvPolynomial σ R) (MvPolynomial σ R)) (integralClosure R B).val) y) =
    (MvPolynomial.map ↑(integralClosure R B).val) (e₁ y)

Tactic:
exact congr($this y)

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
⊢ IsIntegral R t

Tactic:
let t' : St := IsLocalization.Away.invSelf t

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
⊢ IsIntegral R t
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr.h.zero.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
IH :
  ∀ m < 0,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = 0
hi' : i ≤ p.natDegree
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
· simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp

Goal state after: