case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
⊢ content (X ^ Nat.zero) = 1

case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
k : ℕ
hi : content (X ^ k) = 1
⊢ content (X ^ Nat.succ k) = 1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
k : ℕ
⊢ content (X ^ k) = 1
induction' k with k hi
no goals
case succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
k : ℕ
hi : content (X ^ k) = 1
⊢ content (X ^ Nat.succ k) = 1
rw [pow_succ, content_X_mul, hi]
no goals
case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
⊢ content (X ^ Nat.zero) = 1
simp