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

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
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)
a b : S
⊢ a ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) →
    b ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) →
      a + b ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I)

Tactic:
rintro ⟨z, hz, rfl⟩ ⟨y, hy, rfl⟩
    rw [← map_add]
    exact ⟨z + y, Ideal.add_mem _ (SetLike.mem_coe.mp hz) hy, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral

Goal state before:
pp: case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
⊢ -∑ x ∈ Finset.range (minpoly R s).natDegree, b • (minpoly R s).coeff x • s ^ (n - (minpoly R s).natDegree + x) ∈
    (algebraMap R S).range

Tactic:
smul_comm b

Goal state after:
case h.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s : S
H : IsIntegral R s
h : ∃ t ∈ R⁰, t • s ∈ (algebraMap R S).range
b : R
hb' : b ∈ R⁰
hb : ∀ i < (minpoly R s).natDegree, b • s ^ i ∈ (algebraMap R S).range
n : ℕ
IH : ∀ m < n, b • s ^ m ∈ (algebraMap R S).range
hn : (minpoly R s).natDegree ≤ n
this : s ^ (minpoly R s).natDegree = -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • s ^ x
⊢ -∑ x ∈ Finset.range (minpoly R s).natDegree, (minpoly R s).coeff x • b • s ^ (n - (minpoly R s).natDegree + x) ∈
    (algebraMap R S).range
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
z : S
hz : z ∈ R[x]
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥R[x]) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this : z ∈ ⇑(algebraMap (↥R[x]) S) '' ↑(Ideal.map (algebraMap R ↥R[x]) I) ↔ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I
⊢ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
rw [← this, ← temp]
      obtain ⟨a, ha⟩ := (Set.mem_image _ _ _).mp (prod_mem_ideal_map_of_mem_conductor hp
          (show z ∈ I.map (algebraMap R S) by rwa [Ideal.mem_comap] at hy))
      use a + algebraMap R R<x> q * ⟨z, hz⟩
      refine ⟨Ideal.add_mem (I.map (algebraMap R R<x>)) ha.left ?_, by
          simp only [ha.right, map_add, map_mul, add_right_inj]; rfl⟩
      rw [mul_comm]
      exact Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ hq)

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 R
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : QuasiFiniteAt R q
⊢ QuasiFinite R (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) (Ideal.under R q))

Tactic:
exact .of_surjective_algHom (Ideal.Quotient.mkₐ _ _) Ideal.Quotient.mk_surjective

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).QuasiFinite
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt (hV.primeIdealOf ⟨x, hxV⟩).asIdeal

Tactic:
algebraize [(X.presheaf.germ V x hxV).hom]

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
hx : QuasiFiniteAt f x
V : X.Opens
hV : IsAffineOpen V
U : Y.Opens
hU : IsAffineOpen U
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V.carrier
algInst✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
H : (CommRingCat.Hom.hom (Y.presheaf.germ U (f x) ⋯)).QuasiFinite
algInst✝ : Algebra ↑(X.presheaf.obj (Opposite.op V)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).toAlgebra
⊢ (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk y✝.1 y✝.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.1 a'.2 } →
    { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }

Tactic:
| _ a'
   => 

Goal state after:
case H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk y✝.1 y✝.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.1 a'.2 } →
    { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
inst✝ : LocallyQuasiFinite g
⊢ QuasiFiniteAt (f ≫ g) x ↔ QuasiFiniteAt f x

Tactic:
by
  simp only [QuasiFiniteAt, stalkMap_comp]
  exact RingHom.QuasiFinite.comp_iff (g.quasiFiniteAt _)

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

Goal state before:
pp: case inr.H.H.hb
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑(q * q') ≠ 0

Tactic:
simp only [← map_mul, ← Submonoid.coe_mul]

Goal state after:
case inr.H.H.hb
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑(q * q') ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.H.H.hd
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q * φ ↑q' ≠ 0

Tactic:
simp only [← map_mul, ← Submonoid.coe_mul]

Goal state after:
case inr.H.H.hd
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑(q * q') ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.H.H.hb
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q ≠ 0

Tactic:
simp only [← map_mul, ← Submonoid.coe_mul]

Goal state after:
case inr.H.H.hb
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.H.H.hd
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q' ≠ 0

Tactic:
simp only [← map_mul, ← Submonoid.coe_mul]

Goal state after:
case inr.H.H.hd
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q' ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
hq : q ≠ 0
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) = φ p / φ q

Tactic:
simp only [← mk_eq_div, mk_eq_localization_mk _ hq,
    liftMonoidWithZeroHom_apply_ofFractionRing_mk]

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

Goal state before:
pp: case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (0, 1) =
    if 1 = 0 then (0, 1)
    else
      have r := gcd 0 1;
      (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))

Tactic:
if_neg (one_ne_zero' K[X])

Goal state after:
case f0
K : Type u
inst✝ : Field K
p✝ q : K[X]
hq : q ≠ 0
p : K[X]
⊢ (0, 1) =
    have r := gcd 0 1;
    (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x⁻¹.num ∣ x.denom

Tactic:
rw [num_dvd x.denom_ne_zero]
  refine ⟨x.num, num_ne_zero hx, ?_⟩
  nth_rw 1 [← x.num_div_denom]
  rw [inv_div]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case refine_2
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
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (ofId S T).toRingHom a = (fun x ↦ (algebraMap S T) t ^ x) n * x
⊢ ∃ m_1, IsIntegral R ((algebraMap S T) (s ^ (m + 1) * t) ^ m_1 * x)

Tactic:
obtain ⟨k, hk⟩ := Hs a

Goal state after:
case refine_2
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
p : Ideal T
inst✝ : p.IsPrime
s : S
hsp : s ∉ Ideal.under S p
hs : IsIntegral R s
Hs : ∀ (x : S), ∃ m, IsIntegral R (s ^ m * x)
t : S
htp : t ∉ Ideal.under S p
Ht : ⊥.saturation (Submonoid.powers ((algebraMap S T) t)) ⋯ = ⊤
m : ℕ
hm : IsIntegral R (s ^ m * t)
x : T
n : ℕ
a : S
ha : (ofId S T).toRingHom a = (fun x ↦ (algebraMap S T) t ^ x) n * x
k : ℕ
hk : IsIntegral R (s ^ k * a)
⊢ ∃ m_1, IsIntegral R ((algebraMap S T) (s ^ (m + 1) * t) ^ m_1 * x)
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
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁶ : IsDomain S'
this✝⁵ : IsDomain R
this✝⁴ : Algebra.IsIntegral R R'
this✝³ : FaithfulSMul R' K
this✝² : FaithfulSMul R R'
this✝¹ : FaithfulSMul R' L
this✝ : FaithfulSMul R' S'
this : IsIntegrallyClosedIn R' K
⊢ False

Tactic:
have : IsIntegrallyClosed R' := .of_isIntegrallyClosed_of_isIntegrallyClosedIn _ K

Goal state after:
R : Type u_1
S : Type u_2
inst✝²⁸ : CommRing R
inst✝²⁷ : CommRing S
inst✝²⁶ : Algebra R S
K : Type u_4
L : Type u_5
inst✝²⁵ : Field K
inst✝²⁴ : Field L
inst✝²³ : Algebra R K
inst✝²² : Algebra R L
inst✝²¹ : Algebra S L
inst✝²⁰ : Algebra K L
inst✝¹⁹ : IsScalarTower R K L
inst✝¹⁸ : IsScalarTower R S L
inst✝¹⁷ : IsFractionRing R K
inst✝¹⁶ : IsFractionRing S L
R' : Type u_6
S' : Type u_7
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' S'
inst✝¹¹ : Algebra R S'
inst✝¹⁰ : Algebra S' L
inst✝⁹ : Algebra R' L
inst✝⁸ : IsScalarTower R' S' L
inst✝⁷ : Algebra R' K
inst✝⁶ : IsScalarTower R' K L
inst✝⁵ : IsScalarTower R R' S'
inst✝⁴ : FaithfulSMul S' L
inst✝³ : IsIntegralClosure R' R K
inst✝² : IsScalarTower R R' K
f : S →ₐ[R] S'
hf₁ : Function.Surjective ⇑(TensorProduct.lift (ofId R' S') f ⋯)
hf₂ : (algebraMap S' L).comp f.toRingHom = algebraMap S L
x : S
hx' : (aeval x).Finite
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
hx : IsStronglyTranscendental R x
this✝⁷ : IsDomain S'
this✝⁶ : IsDomain R
this✝⁵ : Algebra.IsIntegral R R'
this✝⁴ : FaithfulSMul R' K
this✝³ : FaithfulSMul R R'
this✝² : FaithfulSMul R' L
this✝¹ : FaithfulSMul R' S'
this✝ : IsIntegrallyClosedIn R' K
this : IsIntegrallyClosed R'
⊢ False
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
⊢ f.resultant g m 0 = g.coeff 0 ^ m

Tactic:
by
  rw [resultant_comm]; simp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
⊢ (M (i + 1)).det = r ^ (i + 1) * M₂.det

Tactic:
suffices (M i).updateCol ⟨i, by lia⟩ (r • fun j ↦ M i j ⟨i, by lia⟩) = (M (i + 1)) by
        rw [pow_succ', mul_assoc, ← IH (by lia), ← this, Matrix.det_updateCol_smul,
          Matrix.updateCol_eq_self]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
⊢ (M i).updateCol ⟨i, ⋯⟩ (r • fun j ↦ M i j ⟨i, ⋯⟩) = M (i + 1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.e_a.left
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin m
⊢ Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (m + 1) then f.coeff (↑i - ↑j₁) else 0)
      ((Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.castAdd (n + 1) j))) =
    Fin.addCases (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + (n + 1) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑j₁ ≤ ↑i ∧ ↑i ≤ ↑j₁ + m then f.coeff (↑i - ↑j₁) else 0) (Fin.castAdd (n + 1) j)

Tactic:
have : ((Fin.last m).castAdd (n + 1)).succAbove ((j.castAdd (n + 1)).cast (by grind)) =
          j.castSucc.castAdd (n + 1) := by ext; simp [Fin.succAbove, Fin.lt_def]
        simp [this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
⊢ f₁ = f₂

Tactic:
apply f.normalizationOpenCover.hom_ext _ _ fun U ↦ ?_

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
⊢ (normalizationOpenCover f).f U ≫ f₁ = (normalizationOpenCover f).f U ≫ f₂
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ toNormalization (iU ≫ f) ≫ coprod.inl ≫ (normalizationCoprodIso f e).hom = iU ≫ toNormalization f

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ toNormalization (iV ≫ f) ≫ coprod.inr ≫ (normalizationCoprodIso f e).hom = iV ≫ toNormalization f

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inl ≫ (normalizationCoprodIso f e).hom ≫ fromNormalization f = fromNormalization (iU ≫ f)

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inr ≫ (normalizationCoprodIso f e).hom ≫ fromNormalization f = fromNormalization (iV ≫ f)

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ (normalizationCoprodIso f e).inv ≫ coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) =
    fromNormalization f

Tactic:
simp [Scheme.Hom.normalizationCoprodIso]

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

Goal state before:
pp: case inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
b : R[X]
e : 0 * f + b * g = 1
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
obtain ⟨r, hr, rfl⟩ := isUnit_iff.mp (.of_mul_eq_one_right b (by simpa using e))
    simp [hr.pow]

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

Goal state before:
pp: 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
⊢ f.coeff f.natDegree = φ (f'.coeff f'.natDegree)

Tactic:
← natDegree_eq_natDegree ef,

Goal state after:
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
⊢ f.coeff f'.natDegree = φ (f'.coeff 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
⊢ (map φ (f'.scaleRoots r)).resultant (map φ (g'.scaleRoots r)) f.natDegree g.natDegree =
    φ r ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
← natDegree_eq_natDegree ef,

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
⊢ (map φ (f'.scaleRoots r)).resultant (map φ (g'.scaleRoots r)) f'.natDegree g.natDegree =
    φ r ^ (f'.natDegree * g.natDegree) * f.resultant g f'.natDegree