mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⇑φ
⊢ Ideal.map TensorProduct.includeLeft (RingHom.ker ↑(Ideal.Quotient.mkₐ A (Ideal.under A q))) ⊔
      Ideal.map TensorProduct.includeRight
        (RingHom.ker ↑(Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))) =
    Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)

Tactic:
← Ideal.map_coe,

Goal state after:
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 ⇑φ
⊢ Ideal.map (↑TensorProduct.includeLeft) (RingHom.ker ↑(Ideal.Quotient.mkₐ A (Ideal.under A q))) ⊔
      Ideal.map TensorProduct.includeRight
        (RingHom.ker ↑(Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (Ideal.under R p)))) =
    Ideal.map (algebraMap A (A ⊗[R] S)) (Ideal.under A q)
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
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal T
inst✝¹ : q.IsPrime
inst✝ : WeaklyQuasiFiniteAt R q
this : QuasiFiniteAt S (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) q)
H : Ideal.map (algebraMap R T) (Ideal.under R q) ≤ Ideal.map (algebraMap S T) (Ideal.under S q)
⊢ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q)))
      (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) q) =
    Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q)))
      (Ideal.comap (Ideal.quotientMapₐ (Ideal.map (algebraMap S T) (Ideal.under S q)) (AlgHom.id S T) H).toRingHom
        (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap S T) (Ideal.under S q))) q))

Tactic:
rw [Ideal.comap_comap, Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective]

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
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal T
inst✝¹ : q.IsPrime
inst✝ : WeaklyQuasiFiniteAt R q
this : QuasiFiniteAt S (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) q)
H : Ideal.map (algebraMap R T) (Ideal.under R q) ≤ Ideal.map (algebraMap S T) (Ideal.under S q)
⊢ q ⊔ Ideal.comap (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))) ⊥ =
    Ideal.comap
      ((Ideal.quotientMapₐ (Ideal.map (algebraMap S T) (Ideal.under S q)) (AlgHom.id S T) H).comp
        (Ideal.Quotient.mk (Ideal.map (algebraMap R T) (Ideal.under R q))))
      (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap S T) (Ideal.under S q))) q)
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
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
let φ₁ : p.ResidueField →ₐ[R] Sq ⧸ p.map (algebraMap R Sq) :=
    Ideal.quotientMapₐ _ (IsScalarTower.toAlgHom _ _ _) (by
    rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p, Ideal.map_le_iff_le_comap,
      ← Ideal.comap_coe (F := AlgHom _ _ _), Ideal.comap_comap]
    simpa [← IsScalarTower.algebraMap_eq] using Ideal.le_comap_map)

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.ResidueField →ₐ[R] Sq ⧸ Ideal.map (algebraMap R Sq) p :=
  Ideal.quotientMapₐ (Ideal.map (algebraMap R Sq) p) (IsScalarTower.toAlgHom R (Localization.AtPrime p) Sq) ⋯
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))
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
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ LocallyQuasiFinite (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))

Tactic:
refine (MorphismProperty.arrow_mk_iso_iff _ (Arrow.isoMk ?_ ?_ ?_)).mp (hf x)

Goal state after:
case refine_1
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).left ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).left

case refine_2
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).right ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).right

case refine_3
R S : CommRingCat
φ : R ⟶ S
hf : ∀ (x : ↥(Spec R)), LocallyQuasiFinite (Hom.fiberToSpecResidueField (Spec.map φ) x)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
x : ↥(Spec R)
hP : x.asIdeal.IsPrime
⊢ Iso.hom ?refine_1 ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (algebraMap x.asIdeal.ResidueField (x.asIdeal.Fiber ↑S))))).hom =
    (Arrow.mk (Hom.fiberToSpecResidueField (Spec.map φ) x)).hom ≫ Iso.hom ?refine_2
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

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

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

Tactic:
· exact (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ _
      (fun x ↦ ((hf x).preimage (X.affineCover.f _).isOpenEmbedding.injective.injOn :)) ⟨_, rfl⟩

Goal state after:
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.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.f = 0

Tactic:
rw [aeval_algebraMap_apply, AdjoinRoot.aeval_eq, AdjoinRoot.mk_self, map_zero]

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

Goal state before:
pp: case e'_3.e'_8.h₁
R : Type u_1
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Ideal R
inst✝ : P.IsPrime
x : S
hx : R[x] = ⊤
hx' : Function.Surjective ⇑(aeval x)
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
e : P.Fiber S ≃ₐ[P.ResidueField] P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I :=
  fiberEquivQuotient (aeval x) hx' P
a : R
⊢ (((e.toRingEquiv.toRingHom.comp (aeval (1 ⊗ₜ[R] x)).toRingHom).comp C).comp (algebraMap R P.ResidueField)) a =
    (((Ideal.Quotient.mk (Ideal.map (mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (aeval x).toRingHom))).comp
            C).comp
        (algebraMap R P.ResidueField))
      a

Tactic:
dsimp [-TensorProduct.algebraMap_apply]
    rw [aeval_C, AlgEquiv.commutes]
    simp [← Ideal.Quotient.mk_algebraMap, I]

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
a : S'
ham : a ∈ m
⊢ IsIntegral R (Multiset.map (eval a) (Multiset.map (fun x ↦ X - C x) m)).prod

Tactic:
Multiset.prod_eq_zero

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
a : S'
ham : a ∈ m
⊢ IsIntegral R 0

case refine_2
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
a : S'
ham : a ∈ m
⊢ 0 ∈ Multiset.map (eval a) (Multiset.map (fun x ↦ X - C x) m)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ ∀
    x ∈
      Multiset.map natDegree
        (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m),
    x ≤ f.natDegree - 1

Tactic:
simp only [Multiset.map_map, Function.comp_apply, Multiset.mem_map, forall_exists_index,
      and_imp, forall_apply_eq_imp_iff₂]

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
g : S'[X]
hg :
  Polynomial.map (algebraMap S S') (derivative f * y) -
      (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum =
    Polynomial.map (algebraMap S S') f * g
⊢ ∀ a ∈ m, ((Multiset.map (fun x ↦ X - C x) (m.erase a)).prod * C ((aeval a) y)).natDegree ≤ f.natDegree - 1
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
x : S
hQ' : (Ideal.under (↥R[x]) Q).primesOver S = {Q}
hQ'Q : Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this✝¹ : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this✝ : Module.Finite (↥S') S
this : IsUnramifiedAt (↥S') Q
hφ : Function.Bijective ⇑(Localization.localRingHom Q' Q ↑S'.val ⋯)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨r, hrQ', H⟩ := Localization.exists_awayMap_bijective_of_residueField_surjective hQ' hQ'Q.2

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
Q : Ideal S
inst✝² : Q.IsPrime
inst✝¹ : Module.Finite R S
inst✝ : IsUnramifiedAt R Q
x : S
hQ' : (Ideal.under (↥R[x]) Q).primesOver S = {Q}
hQ'Q : Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this✝¹ : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this✝ : Module.Finite (↥S') S
this : IsUnramifiedAt (↥S') Q
hφ : Function.Bijective ⇑(Localization.localRingHom Q' Q ↑S'.val ⋯)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H : ∀ (r' : ↥R[x]), r ∣ r' → Function.Bijective ⇑(Localization.awayMap (algebraMap (↥R[x]) S) r')
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
P : ↥R[X]_m
⊢ ↑((addLinearEquiv R m n).symm ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n) P)) = ↑P

Tactic:
rw [← (basis ..).sum_repr P]

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
P : ↥R[X]_m
⊢ ↑((addLinearEquiv R m n).symm ((LinearMap.inl R (↥R[X]_m) ↥R[X]_n) (∑ i, ((basis R m).repr P) i • (basis R m) i))) =
    ↑(∑ i, ((basis R m).repr P) i • (basis R m) i)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)

Tactic:
dsimp +instances [inst]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: n : ℕ
IH :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (f : MvPolynomial (Fin n) R →ₐ[R] S), f.Finite → ZariskisMainProperty R p
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin (n + 1)) R →ₐ[R] S
hf : f.Finite
f' : (MvPolynomial (Fin n) R)[X] →ₐ[R] S := f.comp ↑(MvPolynomial.finSuccEquiv R n).symm
this✝⁴ : Algebra (MvPolynomial (Fin n) R) S := (f'.comp C).toAlgebra
this✝³ : IsScalarTower R (MvPolynomial (Fin n) R) S
f'' : (MvPolynomial (Fin n) R)[X] →ₐ[MvPolynomial (Fin n) R] S := { toRingHom := f'.toRingHom, commutes' := ⋯ }
this✝² : WeaklyQuasiFiniteAt (MvPolynomial (Fin n) R) p
this✝¹ : ZariskisMainProperty (MvPolynomial (Fin n) R) p
r : S
hrp : r ∉ p
hr : IsIntegral (MvPolynomial (Fin n) R) r
m : S → ℕ
hm : ∀ (x : S), IsIntegral (MvPolynomial (Fin n) R) (r ^ m x * x)
s : Finset S
hs : adjoin R ↑s = ⊤
R' : Subalgebra R S := adjoin R ↑(Finset.image (⇑f ∘ MvPolynomial.X ∘ Fin.succ) Finset.univ ∪ r ^ s.sup m • s ∪ {r})
hrR' : r ∈ R'
this✝ : WeaklyQuasiFiniteAt R (Ideal.under (↥R') p)
φ : MvPolynomial (Fin n) R →ₐ[R] ↥R' := MvPolynomial.aeval fun i ↦ ⟨f (MvPolynomial.X i.succ), ⋯⟩
this : Algebra (MvPolynomial (Fin n) R) ↥R' := φ.toAlgebra
⊢ algebraMap (MvPolynomial (Fin n) R) S = (algebraMap (↥R') S).comp (algebraMap (MvPolynomial (Fin n) R) ↥R')

Tactic:
ext <;> simp [φ, (f'.toRingHom.comp C).algebraMap_toAlgebra, φ.algebraMap_toAlgebra, f',
            MvPolynomial.finSuccEquiv, MvPolynomial.optionEquivLeft]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn✝ hn : n = m + k
a✝¹ : Nontrivial R
a✝ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
            ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                Algebra.TensorProduct.includeRight)).coeff
        n =
      1 ∧
    ∀ i > n,
      (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
              ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
                  Algebra.TensorProduct.includeRight)).coeff
          i =
        0

Tactic:
refine (MonicDegreeEq.mk _ ?_ ?_).2

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn✝ hn : n = m + k
a✝¹ : Nontrivial R
a✝ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
      ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
          Algebra.TensorProduct.includeRight)).Monic

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn✝ hn : n = m + k
a✝¹ : Nontrivial R
a✝ : Nontrivial (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R)
⊢ (↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) m) Algebra.TensorProduct.includeLeft) *
        ↑((mapEquivMonic R (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) k)
            Algebra.TensorProduct.includeRight)).natDegree =
    n