mathlib-initiative/mathlib-tactics huggingface dataset:
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)))
r : MvPolynomial σ R
⊢ (e₀.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B))) r =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ B)) r

Tactic:
congr 1

Goal state after:
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)))
r : MvPolynomial σ R
⊢ e₀.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)) =
    algebraMap (MvPolynomial σ R) (MvPolynomial σ B)
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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ ⇑(AlgHom.restrictScalars R (toIntegralClosure R S B)) =
    ⇑↑(AlgEquiv.restrictScalars R
          (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
            (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))

Tactic:
congr 1

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
M : Submonoid R
inst✝ : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)) :=
  (Algebra.TensorProduct.includeRight.comp (integralClosure R B).val).codRestrict
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this✝² : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B)) := φ.toAlgebra
this✝¹ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B))
this✝ : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B))) (S ⊗[R] B)
this : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M) ↥(integralClosure S (S ⊗[R] B))
⊢ AlgHom.restrictScalars R (toIntegralClosure R S B) =
    ↑(AlgEquiv.restrictScalars R
        (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
          (S ⊗[R] ↥(integralClosure R B)) ↥(integralClosure S (S ⊗[R] B))))
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]
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
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝³ : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝² : Algebra (↥R₂) St := R₂.toAlgebra
this✝¹ : Algebra (↥R₁) St := R₁.toAlgebra
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ eval₂ ((algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩)) ((algebraMap S St) t) q =
    eval₂ ((algebraMap S St).comp φ.toRingHom) ((algebraMap S St) t) q

Tactic:
congr 1

Goal state after:
case e_f
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]
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
ht't : t' * (algebraMap S St) t = 1
R₁ : Subalgebra R St := R[t']
R₂ : Subalgebra (↥R₁) St := (↥R₁)[(algebraMap S St) (φ X)]
this✝³ : Algebra ↥R₁ ↥R₂ := R₂.algebra
this✝² : Algebra (↥R₂) St := R₂.toAlgebra
this✝¹ : Algebra (↥R₁) St := R₁.toAlgebra
this✝ : IsScalarTower (↥R₁) (↥R₂) St
this : Algebra.IsIntegral ↥R₁ ↥R₂
q : R[X][X]
hq : q.Monic
hq' : eval₂ φ.toRingHom t q = 0
⊢ (algebraMap (↥R₂) St).comp ↑(aeval ⟨(algebraMap S St) (φ X), ⋯⟩) = (algebraMap S St).comp φ.toRingHom
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
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
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
⊢ φ p.eraseLead * t ∈ (conductor R (φ X)).radical

Tactic:
simp only [← self_sub_C_mul_X_pow, map_sub, ← algebraMap_eq, map_mul, AlgHom.commutes,
          map_pow, sub_mul, mul_right_comm _ _ t, ← Algebra.smul_def _ 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
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
n : ℕ
IH :
  ∀ m < n + 1,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = n + 1
hi' : i ≠ p.natDegree
⊢ φ p * t - p.leadingCoeff • t * φ X ^ p.natDegree ∈ (conductor R (φ X)).radical
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝² : j = f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) * (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + 1)

Tactic:
← Nat.cast_one (R := R),

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝² : j = f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + ↑1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree * ↑f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) * (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + 1)

Tactic:
← Nat.cast_one (R := R),

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree * ↑f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) *
      (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + ↑1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ ↑↑(∏ i,
            ∏ j > i,
              if
                  ((finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)).trans
                        (finCongr ⋯).symm)
                      i <
                    ((finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)).trans
                        (finCongr ⋯).symm)
                      j then
                1
              else -1) *
      (g.sylvester f n m).det =
    (-1) ^ (m * n) * (g.sylvester f n m).det

Tactic:
congr 1

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
⊢ ↑↑(∏ i,
          ∏ j > i,
            if
                ((finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)).trans
                      (finCongr ⋯).symm)
                    i <
                  ((finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)).trans
                      (finCongr ⋯).symm)
                    j then
              1
            else -1) =
    (-1) ^ (m * n)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) 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 = M₂.det
hi : i + 1 ≤ m
⊢ ((M (i + 1)).updateCol ⟨i, ⋯⟩ fun k_1 ↦ M (i + 1) k_1 ⟨i, ⋯⟩ + -r • M (i + 1) k_1 ⟨i + k + m, ⋯⟩).det = (M i).det

Tactic:
congr 1

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) 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 = M₂.det
hi : i + 1 ≤ m
⊢ ((M (i + 1)).updateCol ⟨i, ⋯⟩ fun k_1 ↦ M (i + 1) k_1 ⟨i, ⋯⟩ + -r • M (i + 1) k_1 ⟨i + k + m, ⋯⟩) = M i
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ ((pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι) ≫ toNormalization f =
    (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫ toNormalization f

Tactic:
congr 1

Goal state after:
case e_a
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
⊢ (pullbackRestrictIsoRestrict f ↑U).hom ≫ (f ⁻¹ᵁ ↑U).ι = (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) 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₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ (f.sylvester (g + f * (monomial k) r) m n).det = (M m).det

Tactic:
congr 1

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (g + f * (monomial k) r) 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₂
this : ∀ i ≤ m, (M i).det = M₂.det
⊢ f.sylvester (g + f * (monomial k) r) m n = M m
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
g : R[X]
H : 0 ≤ n - m + 1
⊢ f.resultant (g + 0) m n = f.resultant g m n

Tactic:
add_zero

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
g : R[X]
H : 0 ≤ n - m + 1
⊢ f.resultant g m n = f.resultant g m n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: 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₂
this : ∀ i ≤ m, (M i).det = r ^ i * M₂.det
⊢ (f.sylvester (C r * g) m n).det = (M m).det

Tactic:
congr 1

Goal state after:
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₂
this : ∀ i ≤ m, (M i).det = r ^ i * M₂.det
⊢ f.sylvester (C r * g) m n = M m
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U =
    (f ⁻¹ᵁ ↑U).ι ''ᵁ ((f ⁻¹ᵁ ↑U).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
⊢ app ((normalizationOpenCover f).f U) (fromNormalization f ⁻¹ᵁ ↑U) ≫
      ((normalizationOpenCover f).X U).presheaf.map (eqToHom ⋯) ≫
        (ΓSpecIso ((normalizationDiagram f).obj (Opposite.op ((toOpensFunctor Y).obj U)))).hom ≫
          CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val ≫ X.presheaf.map (eqToHom ⋯) =
    app ((normalizationOpenCover f).f U) (fromNormalization f ⁻¹ᵁ ↑U) ≫
      app (Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val))
          ((normalizationOpenCover f).f U ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U) ≫
        app (f ⁻¹ᵁ ↑U).toSpecΓ
            ((TopologicalSpace.Opens.map
                  (Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val)).base).obj
              ((TopologicalSpace.Opens.map ((normalizationOpenCover f).f U).base).obj (fromNormalization f ⁻¹ᵁ ↑U))) ≫
          X.presheaf.map ((opensFunctor (f ⁻¹ᵁ ↑U).ι).map (eqToHom ⋯)).op ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
congr 1

Goal state after:
case e_a
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
this : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U =
    (f ⁻¹ᵁ ↑U).ι ''ᵁ ((f ⁻¹ᵁ ↑U).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
⊢ ((normalizationOpenCover f).X U).presheaf.map (eqToHom ⋯) ≫
      (ΓSpecIso ((normalizationDiagram f).obj (Opposite.op ((toOpensFunctor Y).obj U)))).hom ≫
        CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val ≫ X.presheaf.map (eqToHom ⋯) =
    app (Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val))
        ((normalizationOpenCover f).f U ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U) ≫
      app (f ⁻¹ᵁ ↑U).toSpecΓ
          ((TopologicalSpace.Opens.map
                (Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val)).base).obj
            ((TopologicalSpace.Opens.map ((normalizationOpenCover f).f U).base).obj (fromNormalization f ⁻¹ᵁ ↑U))) ≫
        X.presheaf.map ((opensFunctor (f ⁻¹ᵁ ↑U).ι).map (eqToHom ⋯)).op ≫ X.presheaf.map (eqToHom ⋯)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (-1) ^ (m + 1 + n + m) = (-1) ^ (2 * m + (n + 1))

Tactic:
congr 1

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ m + 1 + n + m = 2 * m + (n + 1)
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
⊢ (C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)).coeff (C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)).natDegree = 1

Tactic:
natDegree_C_mul (by simpa),

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
⊢ (C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)).coeff (f %ₘ g).natDegree = 1
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] := ⋯
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := ⋯
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
⊢ (Multiset.map (fun x ↦ eval x f) g.roots).prod =
    (Multiset.map (fun x ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots).prod

Tactic:
congr 1

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
⊢ Multiset.map (fun x ↦ eval x f) g.roots = Multiset.map (fun x ↦ (f %ₘ g).leadingCoeff * eval x r) g.roots
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
hx : ¬g = 0
hxg : eval x g = 0
| eval x (f %ₘ g) + 0

Tactic:
add_zero

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
hxg : eval x g = 0
| eval x (f %ₘ g)