R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ Multiset.gcd (Multiset.map (coeff (X * p)) (support (X * p)).val) =
    Multiset.gcd (Multiset.map (coeff p) (support p).val)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ content (X * p) = content p
rw [content, content, Finset.gcd_def, Finset.gcd_def]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ Multiset.map (coeff (X * p)) (support (X * p)).val = Multiset.map (coeff p) (support p).val
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ Multiset.gcd (Multiset.map (coeff (X * p)) (support (X * p)).val) =
    Multiset.gcd (Multiset.map (coeff p) (support p).val)
refine' congr rfl _
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
⊢ Multiset.map (coeff (X * p)) (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)).val =
    Multiset.map (coeff p) (support p).val
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
⊢ Multiset.map (coeff (X * p)) (support (X * p)).val = Multiset.map (coeff p) (support p).val
rw [h]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
⊢ Multiset.map (fun x => coeff (X * p) (Nat.succ x)) (support p).val = Multiset.map (coeff p) (support p).val
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
⊢ Multiset.map (coeff (X * p)) (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)).val =
    Multiset.map (coeff p) (support p).val
simp only [Finset.map_val, Function.comp_apply, Function.Embedding.coeFn_mk, Multiset.map_map]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
⊢ (fun x => coeff (X * p) (Nat.succ x)) = coeff p
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
⊢ Multiset.map (fun x => coeff (X * p) (Nat.succ x)) (support p).val = Multiset.map (coeff p) (support p).val
refine' congr (congr rfl _) rfl
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
a : ℕ
⊢ coeff (X * p) (Nat.succ a) = coeff p a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
⊢ (fun x => coeff (X * p) (Nat.succ x)) = coeff p
ext a
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
a : ℕ
⊢ coeff (p * X) (Nat.succ a) = coeff p a
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
a : ℕ
⊢ coeff (X * p) (Nat.succ a) = coeff p a
rw [mul_comm]
no goals
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
a : ℕ
⊢ coeff (p * X) (Nat.succ a) = coeff p a
simp [coeff_mul_X]
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ a ∈ support (X * p) ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ support (X * p) = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
ext a
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬coeff (X * p) a = 0 ↔ ∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = a
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ a ∈ support (X * p) ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } (support p)
simp only [exists_prop, Finset.mem_map, Function.Embedding.coeFn_mk, Ne.def, mem_support_iff]
case a.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ¬coeff (X * p) Nat.zero = 0 ↔ ∃ a, ¬coeff p a = 0 ∧ Nat.succ a = Nat.zero

case a.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬coeff (X * p) (Nat.succ a) = 0 ↔ ∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = Nat.succ a
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬coeff (X * p) a = 0 ↔ ∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = a
cases' a with a
case a.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬coeff p a = 0 ↔ ∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = Nat.succ a
case a.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬coeff (X * p) (Nat.succ a) = 0 ↔ ∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = Nat.succ a
rw [mul_comm, coeff_mul_X]
case a.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬coeff p a = 0 → ∃ a_2, ¬coeff p a_2 = 0 ∧ Nat.succ a_2 = Nat.succ a

case a.succ.mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ (∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = Nat.succ a) → ¬coeff p a = 0
case a.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬coeff p a = 0 ↔ ∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = Nat.succ a
constructor
no goals
case a.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ¬coeff (X * p) Nat.zero = 0 ↔ ∃ a, ¬coeff p a = 0 ∧ Nat.succ a = Nat.zero
simp [coeff_X_mul_zero, Nat.succ_ne_zero]
case a.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬coeff p a = 0
⊢ ∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = Nat.succ a
case a.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬coeff p a = 0 → ∃ a_2, ¬coeff p a_2 = 0 ∧ Nat.succ a_2 = Nat.succ a
intro h
case a.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬coeff p a = 0
⊢ ¬coeff p a = 0 ∧ Nat.succ a = Nat.succ a
case a.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬coeff p a = 0
⊢ ∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = Nat.succ a
use a
no goals
case a.succ.mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
h : ¬coeff p a = 0
⊢ ¬coeff p a = 0 ∧ Nat.succ a = Nat.succ a
simp [h]
case a.succ.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬coeff p b = 0
h2 : Nat.succ b = Nat.succ a
⊢ ¬coeff p a = 0
case a.succ.mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ (∃ a_1, ¬coeff p a_1 = 0 ∧ Nat.succ a_1 = Nat.succ a) → ¬coeff p a = 0
rintro ⟨b, ⟨h1, h2⟩⟩
case a.succ.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬coeff p b = 0
h2 : Nat.succ b = Nat.succ a
⊢ ¬coeff p b = 0
case a.succ.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬coeff p b = 0
h2 : Nat.succ b = Nat.succ a
⊢ ¬coeff p a = 0
rw [← Nat.succ_injective h2]
no goals
case a.succ.mpr.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a b : ℕ
h1 : ¬coeff p b = 0
h2 : Nat.succ b = Nat.succ a
⊢ ¬coeff p b = 0
apply h1