case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : f = 0
⊢ support (integralNormalization f) = support f

case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
⊢ support (integralNormalization f) = support f
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
⊢ support (integralNormalization f) = support f
by_cases hf : f = 0
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ i ∈ support (integralNormalization f) ↔ i ∈ support f
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
⊢ support (integralNormalization f) = support f
ext i
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ i ∈ support f → i ∈ support (integralNormalization f)
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ i ∈ support (integralNormalization f) ↔ i ∈ support f
refine' ⟨fun h => integralNormalization_support h, _⟩
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ coeff f i ≠ 0 → (if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)) ≠ 0
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ i ∈ support f → i ∈ support (integralNormalization f)
simp only [integralNormalization_coeff, mem_support_iff]
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
hfi : coeff f i ≠ 0
⊢ (if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)) ≠ 0
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
⊢ coeff f i ≠ 0 → (if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)) ≠ 0
intro hfi
no goals
case neg.a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : ¬f = 0
i : ℕ
hfi : coeff f i ≠ 0
⊢ (if degree f = ↑i then 1 else coeff f i * leadingCoeff f ^ (natDegree f - 1 - i)) ≠ 0
split_ifs with hi <;> simp [hfi, hi, pow_ne_zero _ (leadingCoeff_ne_zero.mpr hf)]
no goals
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Ring R
inst✝ : IsDomain R
f : R[X]
hf : f = 0
⊢ support (integralNormalization f) = support f
simp [hf]