-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem prime_C_iff_of_fintype {R : Type u} (σ : Type v) {r : R} [CommRing R] [Fintype σ] :
    Prime (C r : MvPolynomial σ R) ↔ Prime r

Proof state:
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime r

Tactic:
convert_to Prime (C r) ↔ _

Result:
case h.e'_1.a
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime (C r)

case convert_1
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Type ?u.169932

case convert_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime (C r) ↔ Prime r

Proof state:
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime (C r) ↔ Prime r

Tactic:
rw [← MulEquiv.prime_iff (renameEquiv R (Fintype.equivFin σ))]

Result:
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime r

Proof state:
case h.e'_1.h.e'_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ C r = (finSuccEquiv R d).symm (Polynomial.C (C r))

Tactic:
simp [← finSuccEquiv_comp_C_eq_C]

Result:
no goals

Proof state:
case convert_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime (C r) ↔ Prime r

Tactic:
induction' Fintype.card σ with d hd

Result:
case convert_3.zero
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime (C r) ↔ Prime r

case convert_3.succ
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ Prime (C r) ↔ Prime r

Proof state:
case h.e'_1.a.a.h.e'_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ (renameEquiv R (Fintype.equivFin σ)) (C r) = C r

Tactic:
simp only [renameEquiv_apply, algHom_C, algebraMap_eq]

Result:
no goals

Proof state:
case convert_3.succ
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ Prime (C r) ↔ Prime r

Tactic:
convert MulEquiv.prime_iff (finSuccEquiv R d).symm (p := Polynomial.C (C r))

Result:
case h.e'_1.h.e'_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ C r = (finSuccEquiv R d).symm (Polynomial.C (C r))

case h.e'_2.a
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ Prime r ↔ Prime (Polynomial.C (C r))

Proof state:
case h.e'_1.a
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime ((renameEquiv R (Fintype.equivFin σ)) (C r)) ↔ Prime (C r)

Tactic:
congr!

Result:
case h.e'_1.a.a.h.e'_3
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ (renameEquiv R (Fintype.equivFin σ)) (C r) = C r

Proof state:
case convert_3.zero
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
⊢ Prime (C r) ↔ Prime r

Tactic:
exact MulEquiv.prime_iff (isEmptyAlgEquiv R (Fin 0)).symm (p := r)

Result:
no goals

Proof state:
case h.e'_2.a
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ Prime r ↔ Prime (Polynomial.C (C r))

Tactic:
simp [← hd, Polynomial.prime_C_iff]

Result:
no goals