mathlib-initiative/mathlib-tactics huggingface dataset:
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 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
⊢ φ ((f'.scaleRoots r).resultant (g'.scaleRoots r) f'.natDegree g'.natDegree) =
    φ r ^ (f'.natDegree * g'.natDegree) * f.resultant g f'.natDegree g'.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ (map φ (f'.scaleRoots g'.leadingCoeff)).resultant (map φ g'.integralNormalization) f'.natDegree g'.natDegree =
    φ g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * (map φ f').resultant (map φ g') f'.natDegree g'.natDegree

Tactic:
resultant_map_map,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
hf0 : ¬f = 0
hg0 : ¬g = 0
S : Type (max 0 u_1) := MvPolynomial R ℤ
φ : S →+* R := MvPolynomial.eval₂Hom (algebraMap ℤ R) id
hφ : Function.Surjective ⇑φ
f' : S[X]
hf' : map φ f' = f
ef : f'.degree = f.degree
g' : S[X]
hg' : map φ g' = g
eg : g'.degree = g.degree
hfl : f.leadingCoeff = φ f'.leadingCoeff
hgl : g.leadingCoeff = φ g'.leadingCoeff
⊢ φ ((f'.scaleRoots g'.leadingCoeff).resultant g'.integralNormalization f'.natDegree g'.natDegree) =
    φ g'.leadingCoeff ^ (f'.natDegree * (g'.natDegree - 1)) * (map φ f').resultant (map φ g') f'.natDegree g'.natDegree
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 g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
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 φ ((taylor r) f')).resultant (map φ ((taylor r) g')) (map φ f').natDegree (map φ g').natDegree =
    (map φ f').resultant (map φ g')

Tactic:
resultant_map_map,

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 g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
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
⊢ φ (((taylor r) f').resultant ((taylor r) g') (map φ f').natDegree (map φ g').natDegree) =
    (map φ f').resultant (map φ g')
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 g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
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
⊢ φ (((taylor r) f').resultant ((taylor r) g') (map φ f').natDegree (map φ g').natDegree) =
    (map φ f').resultant (map φ g')

Tactic:
resultant_map_map,

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 g : R[X]) (r : R), ((taylor r) q).resultant ((taylor r) g) = q.resultant g
g : S[X]
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
⊢ φ (((taylor r) f').resultant ((taylor r) g') (map φ f').natDegree (map φ g').natDegree) =
    φ (f'.resultant g' (map φ f').natDegree (map φ g').natDegree)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
p : R[X]
hp : p ∈ R[X]_m
q : R[X]
hq : q ∈ R[X]_n
hf' : ¬f = 0
⊢ (f * ↑(⟨p, hp⟩, ⟨q, hq⟩).2).degree < ↑(m + n)

Tactic:
exact (degree_mul_le _ _).trans_lt (WithBot.add_lt_add_of_le_of_lt (by simpa)
        (degree_le_of_natDegree_le hf) (by simpa using hq))

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

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 0 < 5
⊢ (if j < 2 then if j = 0 then f.coeff (0 - j) else 0
    else if j ≤ 2 then f.coeff (0 - (j - 2) + 1) * (↑(0 - (j - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨j, hj⟩

Tactic:
fin_cases hj'

Goal state after:
case «0».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 0 < 5
⊢ (if 0 < 2 then if 0 = 0 then f.coeff (0 - 0) else 0
    else if 0 ≤ 2 then f.coeff (0 - (0 - 2) + 1) * (↑(0 - (0 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨0, hj⟩

case «0».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 = 0 then f.coeff (0 - 1) else 0
    else if 1 ≤ 2 then f.coeff (0 - (1 - 2) + 1) * (↑(0 - (1 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨1, hj⟩

case «0».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 = 0 then f.coeff (0 - 2) else 0
    else if 2 ≤ 2 then f.coeff (0 - (2 - 2) + 1) * (↑(0 - (2 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨2, hj⟩

case «0».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 = 0 then f.coeff (0 - 3) else 0
    else if 3 ≤ 2 then f.coeff (0 - (3 - 2) + 1) * (↑(0 - (3 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨3, hj⟩

case «0».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 0 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 = 0 then f.coeff (0 - 4) else 0
    else if 4 ≤ 2 then f.coeff (0 - (4 - 2) + 1) * (↑(0 - (4 - 2)) + 1) else 0) =
    ![f.coeff 0, 0, f.coeff 1, 0, 0] ⟨4, hj⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 1 < 5
⊢ (if j < 2 then if j ≤ 1 then f.coeff (1 - j) else 0
    else if j ≤ 3 then f.coeff (1 - (j - 2) + 1) * (↑(1 - (j - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨j, hj⟩

Tactic:
fin_cases hj'

Goal state after:
case «1».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 1 then f.coeff (1 - 0) else 0
    else if 0 ≤ 3 then f.coeff (1 - (0 - 2) + 1) * (↑(1 - (0 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨0, hj⟩

case «1».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 1 then f.coeff (1 - 1) else 0
    else if 1 ≤ 3 then f.coeff (1 - (1 - 2) + 1) * (↑(1 - (1 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨1, hj⟩

case «1».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 1 then f.coeff (1 - 2) else 0
    else if 2 ≤ 3 then f.coeff (1 - (2 - 2) + 1) * (↑(1 - (2 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨2, hj⟩

case «1».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 1 then f.coeff (1 - 3) else 0
    else if 3 ≤ 3 then f.coeff (1 - (3 - 2) + 1) * (↑(1 - (3 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨3, hj⟩

case «1».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 1 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 1 then f.coeff (1 - 4) else 0
    else if 4 ≤ 3 then f.coeff (1 - (4 - 2) + 1) * (↑(1 - (4 - 2)) + 1) else 0) =
    ![f.coeff 1, f.coeff 0, 2 * f.coeff 2, f.coeff 1, 0] ⟨4, hj⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 2 < 5
⊢ (if j < 2 then if j ≤ 2 then f.coeff (2 - j) else 0
    else if j ≤ 4 then f.coeff (2 - (j - 2) + 1) * (↑(2 - (j - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨j, hj⟩

Tactic:
fin_cases hj'

Goal state after:
case «2».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 2 then f.coeff (2 - 0) else 0
    else if 0 ≤ 4 then f.coeff (2 - (0 - 2) + 1) * (↑(2 - (0 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨0, hj⟩

case «2».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 2 then f.coeff (2 - 1) else 0
    else if 1 ≤ 4 then f.coeff (2 - (1 - 2) + 1) * (↑(2 - (1 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨1, hj⟩

case «2».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 2 then f.coeff (2 - 2) else 0
    else if 2 ≤ 4 then f.coeff (2 - (2 - 2) + 1) * (↑(2 - (2 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨2, hj⟩

case «2».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 2 then f.coeff (2 - 3) else 0
    else if 3 ≤ 4 then f.coeff (2 - (3 - 2) + 1) * (↑(2 - (3 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨3, hj⟩

case «2».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 2 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 2 then f.coeff (2 - 4) else 0
    else if 4 ≤ 4 then f.coeff (2 - (4 - 2) + 1) * (↑(2 - (4 - 2)) + 1) else 0) =
    ![f.coeff 2, f.coeff 1, 3 * f.coeff 3, 2 * f.coeff 2, f.coeff 1] ⟨4, hj⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 3 < 5
⊢ (if j < 2 then if j ≤ 3 then f.coeff (3 - j) else 0
    else if j ≤ 5 ∧ 1 ≤ j - 2 then f.coeff (3 - (j - 2) + 1) * (↑(3 - (j - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨j, hj⟩

Tactic:
fin_cases hj'

Goal state after:
case «3».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 0 < 5
⊢ (if 0 < 2 then if 0 ≤ 3 then f.coeff (3 - 0) else 0
    else if 0 ≤ 5 ∧ 1 ≤ 0 - 2 then f.coeff (3 - (0 - 2) + 1) * (↑(3 - (0 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨0, hj⟩

case «3».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 1 < 5
⊢ (if 1 < 2 then if 1 ≤ 3 then f.coeff (3 - 1) else 0
    else if 1 ≤ 5 ∧ 1 ≤ 1 - 2 then f.coeff (3 - (1 - 2) + 1) * (↑(3 - (1 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨1, hj⟩

case «3».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 2 < 5
⊢ (if 2 < 2 then if 2 ≤ 3 then f.coeff (3 - 2) else 0
    else if 2 ≤ 5 ∧ 1 ≤ 2 - 2 then f.coeff (3 - (2 - 2) + 1) * (↑(3 - (2 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨2, hj⟩

case «3».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 3 < 5
⊢ (if 3 < 2 then if 3 ≤ 3 then f.coeff (3 - 3) else 0
    else if 3 ≤ 5 ∧ 1 ≤ 3 - 2 then f.coeff (3 - (3 - 2) + 1) * (↑(3 - (3 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨3, hj⟩

case «3».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 3 < 5
hj : 4 < 5
⊢ (if 4 < 2 then if 4 ≤ 3 then f.coeff (3 - 4) else 0
    else if 4 ≤ 5 ∧ 1 ≤ 4 - 2 then f.coeff (3 - (4 - 2) + 1) * (↑(3 - (4 - 2)) + 1) else 0) =
    ![f.coeff 3, f.coeff 2, 0, 3 * f.coeff 3, 2 * f.coeff 2] ⟨4, hj⟩
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case «4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
j : ℕ
hj : j < 5
hj' : j ∈ Finset.range 5
hi : 4 < 5
⊢ (if j = 1 then 1 else if j = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨j, hj⟩

Tactic:
fin_cases hj'

Goal state after:
case «4».«0»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 0 < 5
⊢ (if 0 = 1 then 1 else if 0 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨0, hj⟩

case «4».«1»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 1 < 5
⊢ (if 1 = 1 then 1 else if 1 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨1, hj⟩

case «4».«2»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 2 < 5
⊢ (if 2 = 1 then 1 else if 2 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨2, hj⟩

case «4».«3»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi : 4 < 5
hj : 3 < 5
⊢ (if 3 = 1 then 1 else if 3 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨3, hj⟩

case «4».«4»
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
hi hj : 4 < 5
⊢ (if 4 = 1 then 1 else if 4 = 4 then 3 else 0) = ![0, 1, 0, 0, 3] ⟨4, hj⟩
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝¹ : Nonempty ↥G.left
this✝ : IsProper (G ⊗ G).hom
this : JacobsonSpace ↥(G ⊗ G).left
⊢ IsCommMonObj G

Tactic:
have : Surjective G.hom := ⟨Function.surjective_to_subsingleton (α := G.left) (β := Spec _) _⟩

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝² : Nonempty ↥G.left
this✝¹ : IsProper (G ⊗ G).hom
this✝ : JacobsonSpace ↥(G ⊗ G).left
this : Surjective G.hom
⊢ IsCommMonObj G
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
⊢ IsCommMonObj X

Tactic:
let : MonObj X := .ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
  have : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) := rfl
  constructor
  simp_rw [this, ← α.homEquiv'.apply_eq_iff_eq, α.homEquiv'_comp,
    Equiv.apply_symm_apply, map_mul, ← α.homEquiv'_comp, op_tensorObj,
    braiding_hom_fst, braiding_hom_snd, _root_.mul_comm]

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf :
  (Localization.awayMapₐ
      (ofId R' (Localization.Away ((TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀)))
      f).Finite
⊢ ∃ f ∉ P,
    Module.Finite (Localization.Away f)
      (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))

Tactic:
rw [he₀e] at hf

Goal state after:
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this : Algebra.IsIntegral R' (Localization.Away e₀)
f : R'
hfP : f ∉ P
hf : (Localization.awayMapₐ (ofId R' (Localization.Away e)) f).Finite
⊢ ∃ f ∉ P,
    Module.Finite (Localization.Away f)
      (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
⊢ P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom

Tactic:
let e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
      colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
    preservesColimitIso (Over.forget S) _

Goal state after:
X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
⊢ P (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ η.symm.hom = η.inv

Tactic:
simp only [Iso.symm_hom]

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

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ Surjective f

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @Surjective X.isoSpec.inv]

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ Surjective (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case hf₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Flat

Tactic:
· exact RingHom.Flat.id ↑R

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Nontrivial R
⊢ ∀ (x y : R),
    (if x * y ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R (x * y)) else 0) =
      (if x ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R x) else 0) *
        if y ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x ↦ ↑(Multiplicative.ofAdd ↑x)) (ord R y) else 0

Tactic:
by
    intro x y
    split_ifs with _ _ b
    · rw [ord_mul _ b]
      generalize ord R x = x'
      generalize ord R y = y'
      cases x' <;> cases y'
      on_goal 4 =>
        simp only [← ENat.natCast_add, ENat.recTopCoe_natCast, Nat.cast_add (R := ℤ),
          ofAdd_add, WithZero.coe_mul]
      all_goals simp
    all_goals simp_all [mul_mem_nonZeroDivisors]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
U : X.Opens
inst✝ : Nonempty ↥↑U
f : ↑Γ(X, U)
hf : IsUnit f
x : ↥X
hx' : x ∈ U
⊢ ord ((ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

Tactic:
by
  by_cases! hx : coheight x ≠ 1
  · simp [hx]
  simp [map_ne_zero_iff, germToFunctionField_injective, IsUnit.ne_zero hf,
    ord_eq_iff hx, ordHom_of_isUnit hf hx hx']

Goal state after: