mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
x : K
⊢ ¬g = 0 → eval x g = 0 → eval x f = eval x (f %ₘ g)

Tactic:
hx

Goal state after:
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
x : K
hx : ¬g = 0
⊢ eval x g = 0 → eval x f = eval x (f %ₘ g)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
a✝ : Nontrivial R
⊢ (freeMonic R n).Monic

Tactic:
simp [Polynomial.Monic, ← Polynomial.coeff_natDegree, natDegree_freeMonic, coeff_freeMonic]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
x : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
⊢ x ∈ RingHom.ker f →
    x ∈
      Ideal.span
        (Set.range fun i ↦
          C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
hx

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
x : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
hx : x ∈ RingHom.ker f
⊢ x ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
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 : n = m + k
this : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
⊢ Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i)))) =
    { val := Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x,
        σ' := fun f ↦ (map C) ((tensorEquivSum R (Fin m) (Fin k) R) f), aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }.ker

Tactic:
by
      exact (ker_eval₂Hom_universalFactorizationMap R n m k hn).symm

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = 0 ^ q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
⊢ φ 0 ^ f'.natDegree = 0 ^ f'.natDegree

Tactic:
map_zero

Goal state after:
case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH : ∀ (q : R[X]), q.resultant q = 0 ^ q.natDegree
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
⊢ 0 ^ f'.natDegree = 0 ^ f'.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') =
    φ r ^ (f'.natDegree * g'.natDegree) * (map φ f').resultant (map φ g') f'.natDegree g'.natDegree

Tactic:
resultant_map_map

Goal state after:
case inr.inr.surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g : R[X]) (r : R),
    q ≠ 0 →
      g ≠ 0 →
        (q.scaleRoots r).resultant (g.scaleRoots r) q.natDegree g.natDegree =
          r ^ (q.natDegree * g.natDegree) * q.resultant g
g : S[X]
hf : f ≠ 0
hg : g ≠ 0
f' : R[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : R[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
r : R
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ (r ^ (f'.natDegree * g'.natDegree) * f'.resultant g') = φ r ^ (f'.natDegree * g'.natDegree) * φ (f'.resultant g')
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 : n = m + k
p : MonicDegreeEq R n
⊢ Algebra.Etale R 𝓡'

Tactic:
let Δ : 𝓡 := (presentation m k hn p).jacobian

Goal state after:
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 : n = m + k
p : MonicDegreeEq R n
Δ : 𝓡 := (presentation m k hn p).jacobian
⊢ Algebra.Etale R 𝓡'
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 : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit
    ((map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant
      (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p)))

Tactic:
Polynomial.isUnit_resultant_iff_isCoprime
        ((UniversalFactorizationRing.factor₁ m k hn p).monic.map _)

Goal state after:
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 : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsCoprime (map ↑f ↑(UniversalFactorizationRing.factor₁ m k hn p))
    (map ↑f ↑(UniversalFactorizationRing.factor₂ m k hn p))
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
T : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra.FiniteType R T
inst✝¹ : Algebra.IsIntegral R S
f : S →ₐ[R] T
g : S
hg : Function.Surjective ⇑(awayMapₐ f g)
p : Ideal R
inst✝ : p.IsPrime
hgp : IsUnit (1 ⊗ₜ[R] g)
this✝¹ : IsClosed (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})
r : R
hpr : { asIdeal := p, isPrime := inst✝ } ∈ ↑(PrimeSpectrum.basicOpen r)
hrg : ↑(PrimeSpectrum.basicOpen r) ⊆ (PrimeSpectrum.comap (algebraMap R S) '' PrimeSpectrum.zeroLocus {g})ᶜ
this✝ : IsLocalization.Away (f.toRingHom ((algebraMap R S) r)) (Away ((algebraMap R T) r))
h₁ : (awayMap (algebraMap R S) r).IsIntegral
x : T
n : ℕ
this : ∃ a k l, (algebraMap R T) r ^ (l + n) * f a = (algebraMap R T) r ^ (l + k) * x
⊢ ∃ a,
    (IsLocalization.Away.map (Away ((algebraMap R S) r)) (Away ((algebraMap R T) r)) f.toRingHom ((algebraMap R S) r))
        a =
      IsLocalization.mk' (Away ((algebraMap R T) r)) x ⟨(fun x ↦ (algebraMap R T) r ^ x) n, ⋯⟩

Tactic:
by
        simpa [(IsLocalization.mk'_surjective (.powers (algebraMap R S r))).exists,
          IsLocalization.Away.map, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq,
          ← map_pow, Submonoid.mem_powers_iff, IsLocalization.Away.map, IsLocalization.map_mk',
          IsLocalization.mk'_eq_iff_eq, ← map_mul, ← mul_assoc, ← pow_add,
          IsLocalization.eq_iff_exists (.powers (algebraMap R T r))]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
F : Cᵒᵖ ⥤ GrpCat
α : (F ⋙ forget GrpCat).RepresentableBy X
⊢ lift (𝟙 X) (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) ≫ μ = toUnit X ≫ η

Tactic:
change lift (𝟙 X) (α.homEquiv'.symm (α.homEquiv' (𝟙 X))⁻¹) ≫
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
        toUnit X ≫ α.homEquiv'.symm 1

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
F : Cᵒᵖ ⥤ GrpCat
α : (F ⋙ forget GrpCat).RepresentableBy X
⊢ lift (𝟙 X) (α.homEquiv'.symm (α.homEquiv' (𝟙 X))⁻¹) ≫
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
    toUnit X ≫ α.homEquiv'.symm 1
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
⊢ TensorProduct.includeRight 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
⊢ 0 = 0
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : (aeval s') f = 0
⊢ TensorProduct.includeRight 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : (aeval s') f = 0
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
x : 𝒰.toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (Cover.pullbackHom 𝒰 (toNormalization f ∣_ ⨆ x, V x) x)

Tactic:
refine (MorphismProperty.arrow_mk_iso_iff (.isomorphisms _)
      ((morphismRestrictRestrict ..).symm ≪≫ morphismRestrictOpensRange ..)).mp ?_

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
x : 𝒰.toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (toNormalization f ∣_ (⨆ x, V x).ι ''ᵁ opensRange (𝒰.f x))
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
⊢ W ≤ f ⁻¹ᵁ U

Tactic:
unfold W

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
⊢ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r ≤ f ⁻¹ᵁ U
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝¹ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
this✝ : IsIso (app (toNormalization f) ((normalization f).basicOpen r))
this : (CommRingCat.Hom.hom (appLE f U W H)).QuasiFinite
hxU : f x ∈ U
⊢ ((CommRingCat.Hom.hom (X.presheaf.germ W x hxV)).comp (CommRingCat.Hom.hom (appLE f U W ⋯))).QuasiFinite

Tactic:
refine .comp ?_ this

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝¹ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
this✝ : IsIso (app (toNormalization f) ((normalization f).basicOpen r))
this : (CommRingCat.Hom.hom (appLE f U W H)).QuasiFinite
hxU : f x ∈ U
⊢ (CommRingCat.Hom.hom (X.presheaf.germ W x hxV)).QuasiFinite
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
⊢ x ∈ {x | QuasiFiniteAt f x} → ∃ t ⊆ {x | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t

Tactic:
hx

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
x : ↥X
hx : x ∈ {x | QuasiFiniteAt f x}
⊢ ∃ t ⊆ {x | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
Module: Mathlib.RingTheory.Finiteness.Descent

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
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
x : R
⊢ x ∈ I → x ∈ comap (algebraMap R S) f.range

Tactic:
hx

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
f : S ⊗[R] ↥I →ₗ[S] S := ↑(AlgebraTensorModule.rid R S S) ∘ₗ (AlgebraTensorModule.lTensor S S) (Submodule.subtype I)
hf : Function.Injective ⇑f
x : R
hx : x ∈ I
⊢ x ∈ comap (algebraMap R S) f.range