-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_X_mul {p : R[X]} : content (X * p) = content p

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(X * p).coeff a = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a

Tactic:
rcases a with - | a

Result:
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ¬(X * p).coeff 0 = 0 ↔ ∃ a, ¬p.coeff a = 0 ∧ a.succ = 0

case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(X * p).coeff (a + 1) = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
a : ℕ
⊢ (p * X).coeff a.succ = p.coeff a

Tactic:
simp [coeff_mul_X]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (X * p).content = p.content

Tactic:
rw [content, content, Finset.gcd_def, Finset.gcd_def]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (Multiset.map (X * p).coeff (X * p).support.val).gcd = (Multiset.map p.coeff p.support.val).gcd

Proof state:
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ¬(X * p).coeff 0 = 0 ↔ ∃ a, ¬p.coeff a = 0 ∧ a.succ = 0

Tactic:
simp [coeff_X_mul_zero, Nat.succ_ne_zero]

Result:
no goals

Proof state:
case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
constructor

Result:
case h.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 → ∃ a_2, ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1

case h.succ.mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ (∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1) → ¬p.coeff a = 0

Proof state:
case h.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬p.coeff a = 0
⊢ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
use a

Result:
no goals

Proof state:
case h.succ.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬p.coeff b = 0
h2 : b.succ = a + 1
⊢ ¬p.coeff a = 0

Tactic:
rw [← Nat.succ_injective h2]

Result:
case h.succ.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬p.coeff b = 0
h2 : b.succ = a + 1
⊢ ¬p.coeff b = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ (fun x => (X * p).coeff x.succ) = p.coeff

Tactic:
ext a

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
a : ℕ
⊢ (X * p).coeff a.succ = p.coeff a

Proof state:
case h.succ.mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ (∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1) → ¬p.coeff a = 0

Tactic:
rintro ⟨b, ⟨h1, h2⟩⟩

Result:
case h.succ.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬p.coeff b = 0
h2 : b.succ = a + 1
⊢ ¬p.coeff a = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (X * p).coeff (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support).val =
    Multiset.map p.coeff p.support.val

Tactic:
simp only [Finset.map_val, Function.comp_apply, Function.Embedding.coeFn_mk, Multiset.map_map]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (fun x => (X * p).coeff x.succ) p.support.val = Multiset.map p.coeff p.support.val

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ a ∈ (X * p).support ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support

Tactic:
simp only [exists_prop, Finset.mem_map, Function.Embedding.coeFn_mk, Ne, mem_support_iff]

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(X * p).coeff a = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
a : ℕ
⊢ (X * p).coeff a.succ = p.coeff a

Tactic:
rw [mul_comm]

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
a : ℕ
⊢ (p * X).coeff a.succ = p.coeff a

Proof state:
case h.succ.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬p.coeff b = 0
h2 : b.succ = a + 1
⊢ ¬p.coeff b = 0

Tactic:
apply h1

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support

Tactic:
ext a

Result:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ a ∈ (X * p).support ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support

Proof state:
case h.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 → ∃ a_2, ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1

Tactic:
intro h

Result:
case h.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬p.coeff a = 0
⊢ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (Multiset.map (X * p).coeff (X * p).support.val).gcd = (Multiset.map p.coeff p.support.val).gcd

Tactic:
refine congr rfl ?_

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val

Tactic:
rw [h]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (X * p).coeff (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support).val =
    Multiset.map p.coeff p.support.val