-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.map [Semiring S] (f : R →+* S) (hp : Monic p) : Monic (p.map f)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
⊢ (Polynomial.map f p).leadingCoeff = 1

Tactic:
nontriviality

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
⊢ (Polynomial.map f p).leadingCoeff = 1

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
this : f p.leadingCoeff ≠ 0
⊢ (Polynomial.map f p).leadingCoeff = 1

Tactic:
rw [Polynomial.leadingCoeff, coeff_map]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
this : f p.leadingCoeff ≠ 0
⊢ f (p.coeff (Polynomial.map f p).natDegree) = 1

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
this : f p.leadingCoeff ≠ 0
⊢ p.coeff (Polynomial.map f p).natDegree = 1

Tactic:
rwa [natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f this)]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
⊢ (Polynomial.map f p).Monic

Tactic:
unfold Monic

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
⊢ (Polynomial.map f p).leadingCoeff = 1

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
⊢ f p.leadingCoeff ≠ 0

Tactic:
rw [show _ = _ from hp, f.map_one]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
⊢ 1 ≠ 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
this : f p.leadingCoeff ≠ 0
⊢ f (p.coeff (Polynomial.map f p).natDegree) = 1

Tactic:
suffices p.coeff (p.map f).natDegree = 1 by simp [this]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
this : f p.leadingCoeff ≠ 0
⊢ p.coeff (Polynomial.map f p).natDegree = 1

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
⊢ (Polynomial.map f p).leadingCoeff = 1

Tactic:
have : f p.leadingCoeff ≠ 0 := by
  rw [show _ = _ from hp, f.map_one]
  exact one_ne_zero

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
this : f p.leadingCoeff ≠ 0
⊢ (Polynomial.map f p).leadingCoeff = 1

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hp : p.Monic
a✝ : Nontrivial S
this✝ : f p.leadingCoeff ≠ 0
this : p.coeff (Polynomial.map f p).natDegree = 1
⊢ f (p.coeff (Polynomial.map f p).natDegree) = 1

Tactic:
simp [this]

Result:
no goals