-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem prime_C_iff : Prime (C r : MvPolynomial σ R) ↔ Prime r :=
  ⟨comap_prime C constantCoeff (constantCoeff_C _), fun hr =>
    ⟨fun h => hr.1 <| by
        rw [← C_inj, h]
        simp,
      fun h =>
      hr.2.1 <| by
        rw [← constantCoeff_C _ r]
        exact h.map _,
      fun a b hd => by
      obtain ⟨s, a', b', rfl, rfl⟩ := exists_finset_rename₂ a b
      rw [← algebraMap_eq] at hd
      have : algebraMap R _ r ∣ a' * b'

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'
f : MvPolynomial { x // x ∈ s } R →+* MvPolynomial σ R := (rename Subtype.val).toRingHom
⊢ (rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'

Tactic:
exact (((prime_C_iff_of_fintype s).2 hr).2.2 a' b' this).imp f.map_dvd f.map_dvd

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : C r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Tactic:
rw [← algebraMap_eq] at hd

Result:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ r = 0

Tactic:
rw [← C_inj, h]

Result:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ 0 = C 0

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'
⊢ (rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'

Tactic:
let f := (rename (R := R) ((↑) : s → σ)).toRingHom

Result:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'
f : MvPolynomial { x // x ∈ s } R →+* MvPolynomial σ R := (rename Subtype.val).toRingHom
⊢ (rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Tactic:
rw [← rename_C ((↑) : s → σ)]

Result:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'
⊢ (rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit (constantCoeff (C r))

R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ Type ?u.183619

Tactic:
exact h.map _

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : C r = 0
⊢ 0 = C 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
a b : MvPolynomial σ R
hd : C r ∣ a * b
⊢ C r ∣ a ∨ C r ∣ b

Tactic:
obtain ⟨s, a', b', rfl, rfl⟩ := exists_finset_rename₂ a b

Result:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : C r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Proof state:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Tactic:
have : algebraMap R _ r ∣ a' * b' := by
  convert killCompl Subtype.coe_injective |>.toRingHom.map_dvd hd <;> simp

Result:
case intro.intro.intro.intro
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit r

Tactic:
rw [← constantCoeff_C _ r]

Result:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit (constantCoeff (C r))

R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ Type ?u.183619

Proof state:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial { x // x ∈ s } R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
⊢ (algebraMap R (MvPolynomial { x // x ∈ s } R)) r ∣ a' * b'

Tactic:
convert killCompl Subtype.coe_injective |>.toRingHom.map_dvd hd <;> simp

Result:
no goals