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

Goal state before:
pp: case inr.left
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
i : Fin (m + n)
i✝ : Fin m
⊢ f.sylvester (g + f * (monomial k) r) m n i (Fin.castAdd n i✝) = M m i (Fin.castAdd n i✝)

pp: case inr.right
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
i : Fin (m + n)
i✝ : Fin n
⊢ f.sylvester (g + f * (monomial k) r) m n i (Fin.natAdd m i✝) = M m i (Fin.natAdd m i✝)

Tactic:
<;>

Goal state after:
case inr.left
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
i : Fin (m + n)
i✝ : Fin m
⊢ f.sylvester (g + f * (monomial k) r) m n i (Fin.castAdd n i✝) = M m i (Fin.castAdd n i✝)

case inr.right
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
i : Fin (m + n)
i✝ : Fin n
⊢ f.sylvester (g + f * (monomial k) r) m n i (Fin.natAdd m i✝) = M m i (Fin.natAdd m i✝)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.H
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ k ≤ n - m + 1

pp: case succ.hk
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ k + m ≤ n

pp: case succ.hf
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ f.natDegree ≤ m

Tactic:
<;>

Goal state after:
case succ.H
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ k ≤ n - m + 1

case succ.hk
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ k + m ≤ n

case succ.hf
R : Type u_1
inst✝ : CommRing R
f p : R[X]
m n : ℕ
hp : p.natDegree + m ≤ n
hf : f.natDegree ≤ m
k : ℕ
IH :
  ∀ (g : R[X]),
    k ≤ n - m + 1 → f.resultant (g + f * ∑ n ∈ Finset.range k, (monomial n) (p.coeff n)) m n = f.resultant g m n
g : R[X]
H : k + 1 ≤ n - m + 1
⊢ f.natDegree ≤ m
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]
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_self_iff_false, ↓reduceIte, Matrix.updateCol_apply,
        Fin.ext_iff, Pi.smul_apply, smul_eq_mul, M, M₂]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, Fin.eta, Matrix.of_apply,
          lt_add_iff_pos_right, zero_lt_one, coeff_C_mul, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ => simp
        | right i => simp at hi
      lia

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

Goal state before:
pp: case left
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
i : Fin (m + n)
i✝ : Fin m
⊢ f.sylvester (C r * g) m n i (Fin.castAdd n i✝) = M m i (Fin.castAdd n i✝)

pp: case right
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
i : Fin (m + n)
i✝ : Fin n
⊢ f.sylvester (C r * g) m n i (Fin.natAdd m i✝) = M m i (Fin.natAdd m i✝)

Tactic:
<;>

Goal state after:
case left
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
i : Fin (m + n)
i✝ : Fin m
⊢ f.sylvester (C r * g) m n i (Fin.castAdd n i✝) = M m i (Fin.castAdd n i✝)

case right
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
i : Fin (m + n)
i✝ : Fin n
⊢ f.sylvester (C r * g) m n i (Fin.natAdd m i✝) = M m i (Fin.natAdd m i✝)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + (m + 1)
h₃ : ↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = f.coeff (↑i - ↑j)

pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + (m + 1)
h₃ : ¬↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = 0

pp: case pos
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + (m + 1)
h₃ : ↑i ≤ ↑j + m
⊢ 0 = f.coeff (↑i - ↑j)

pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + (m + 1)
h₃ : ¬↑i ≤ ↑j + m
⊢ 0 = 0

pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ¬↑j ≤ ↑i
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + (m + 1)
h₃ : ↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = f.coeff (↑i - ↑j)

case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ↑j ≤ ↑i
h₂ : ↑i ≤ ↑j + (m + 1)
h₃ : ¬↑i ≤ ↑j + m
⊢ f.coeff (↑i - ↑j) = 0

case pos
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + (m + 1)
h₃ : ↑i ≤ ↑j + m
⊢ 0 = f.coeff (↑i - ↑j)

case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ↑j ≤ ↑i
h₂ : ¬↑i ≤ ↑j + (m + 1)
h₃ : ¬↑i ≤ ↑j + m
⊢ 0 = 0

case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i : Fin (m + (n + 1))
j : Fin (n + 1)
this : (Fin.castAdd (n + 1) (Fin.last m)).succAbove (Fin.cast ⋯ (Fin.natAdd m j)) = Fin.natAdd (m + 1) j
h₁ : ¬↑j ≤ ↑i
⊢ 0 = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Over

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✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
P' : Ideal S
inst✝¹ : P'.IsPrime
inst✝ : P'.LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ P'
H : (P.primesOver S).Finite
⊢ P' ∉ comap f '' P.primesOver T

Tactic:
rintro ⟨q, ⟨_, _⟩, rfl⟩

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✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
H : (P.primesOver S).Finite
q : Ideal T
left✝ : q.IsPrime
right✝ : q.LiesOver P
inst✝¹ : (comap f q).IsPrime
inst✝ : (comap f q).LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ comap f q
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Over

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✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
f : S →ₐ[R] T
Hf : Function.Surjective ⇑f
P : Ideal R
P' : Ideal S
inst✝¹ : P'.IsPrime
inst✝ : P'.LiesOver P
hkP' : ¬RingHom.ker f.toRingHom ≤ P'
H : (P.primesOver S).Finite
⊢ P' ∉ comap f '' P.primesOver T

Tactic:
· rintro ⟨q, ⟨_, _⟩, rfl⟩; exact hkP' (Ideal.ker_le_comap _)

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

Goal state before:
pp: case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
⊢ Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m) =
    Polynomial.map
      ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
              ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
              ⋯)).comp
        ↑Algebra.TensorProduct.includeLeft)
      (freeMonic R m)

pp: case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
⊢ Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k) =
    Polynomial.map
      ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
              ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
              ⋯)).comp
        ↑Algebra.TensorProduct.includeRight)
      (freeMonic R k)

Tactic:
<;>

Goal state after:
case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
⊢ Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m) =
    Polynomial.map
      ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
              ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
              ⋯)).comp
        ↑Algebra.TensorProduct.includeLeft)
      (freeMonic R m)

case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
⊢ Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k) =
    Polynomial.map
      ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
              ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
              ⋯)).comp
        ↑Algebra.TensorProduct.includeRight)
      (freeMonic R k)
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
n✝ : ℕ
⊢ (Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m)).coeff n✝ =
    (Polynomial.map
          ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                  ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                  ⋯)).comp
            ↑Algebra.TensorProduct.includeLeft)
          (freeMonic R m)).coeff
      n✝

pp: case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
n✝ : ℕ
⊢ (Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k)).coeff n✝ =
    (Polynomial.map
          ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                  ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                  ⋯)).comp
            ↑Algebra.TensorProduct.includeRight)
          (freeMonic R k)).coeff
      n✝

Tactic:
<;>

Goal state after:
case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
n✝ : ℕ
⊢ (Polynomial.map ((↑Algebra.TensorProduct.includeLeft).comp (map (algebraMap R S))) (freeMonic R m)).coeff n✝ =
    (Polynomial.map
          ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                  ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                  ⋯)).comp
            ↑Algebra.TensorProduct.includeLeft)
          (freeMonic R m)).coeff
      n✝

case hX.e_a.e_a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
n m k : ℕ
hn : n = m + k
i✝ : Fin n
n✝ : ℕ
⊢ (Polynomial.map ((↑Algebra.TensorProduct.includeRight).comp (map (algebraMap R S))) (freeMonic R k)).coeff n✝ =
    (Polynomial.map
          ((↑(Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId R S)))
                  ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId R S)))
                  ⋯)).comp
            ↑Algebra.TensorProduct.includeRight)
          (freeMonic R k)).coeff
      n✝
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case fst
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 S n
q : { q // ↑q.1 * ↑q.2 = ↑p }
n✝ : ℕ
⊢ (↑(↑((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                ((fun q ↦
                    ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2)
                        ⋯,
                      ⋯⟩)
                  q))).1).coeff
      n✝ =
    (↑(↑q).1).coeff n✝

pp: case snd
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 S n
q : { q // ↑q.1 * ↑q.2 = ↑p }
n✝ : ℕ
⊢ (↑(↑((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                ((fun q ↦
                    ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2)
                        ⋯,
                      ⋯⟩)
                  q))).2).coeff
      n✝ =
    (↑(↑q).2).coeff n✝

Tactic:
<;>

Goal state after:
case fst
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 S n
q : { q // ↑q.1 * ↑q.2 = ↑p }
n✝ : ℕ
⊢ (↑(↑((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                ((fun q ↦
                    ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2)
                        ⋯,
                      ⋯⟩)
                  q))).1).coeff
      n✝ =
    (↑(↑q).1).coeff n✝

case snd
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 S n
q : { q // ↑q.1 * ↑q.2 = ↑p }
n✝ : ℕ
⊢ (↑(↑((fun f ↦
                  ⟨((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
                      (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)),
                    ⋯⟩)
                ((fun q ↦
                    ⟨Algebra.TensorProduct.lift ((mapEquivMonic R S m).symm (↑q).1) ((mapEquivMonic R S k).symm (↑q).2)
                        ⋯,
                      ⋯⟩)
                  q))).2).coeff
      n✝ =
    (↑(↑q).2).coeff n✝
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
by_cases hf0 : f = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : f = 0
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hf0 : ¬f = 0
⊢ f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x ↦ eval x g) f.roots).prod
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case h₁
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 ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ f =
    coprod.inl ≫
      coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)) ≫
        coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))

pp: case h₂
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 ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ f =
    coprod.inr ≫
      coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)) ≫
        coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))

Tactic:
<;>

Goal state after:
case h₁
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 ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ f =
    coprod.inl ≫
      coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)) ≫
        coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))

case h₂
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 ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ f =
    coprod.inr ≫
      coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)) ≫
        coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))