-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem support_integralNormalization {f : R[X]} :
    (integralNormalization f).support = f.support

Proof state:
case neg.h
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
⊢ f.coeff i ≠ 0 → (if f.degree = ↑i then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0

Tactic:
intro hfi

Result:
case neg.h
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
⊢ (if f.degree = ↑i then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0

Proof state:
case neg.h
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
⊢ i ∈ f.integralNormalization.support ↔ i ∈ f.support

Tactic:
refine ⟨fun h => support_integralNormalization_subset h, ?_⟩

Result:
case neg.h
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
⊢ i ∈ f.support → i ∈ f.integralNormalization.support

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
⊢ f.integralNormalization.support = f.support

Tactic:
by_cases hf : f = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : f = 0
⊢ f.integralNormalization.support = f.support

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
⊢ f.integralNormalization.support = f.support

Proof state:
case neg.h
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
hfi : f.coeff i ≠ 0
⊢ (if f.degree = ↑i then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0

Tactic:
split_ifs with hi <;> simp [hf, hfi, hi]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
⊢ f.integralNormalization.support = f.support

Tactic:
ext i

Result:
case neg.h
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
⊢ i ∈ f.integralNormalization.support ↔ i ∈ f.support

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
⊢ f.integralNormalization.support = f.support

Tactic:
nontriviality R using Subsingleton.eq_zero

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
⊢ f.integralNormalization.support = f.support

Proof state:
case neg.h
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
⊢ i ∈ f.support → i ∈ f.integralNormalization.support

Tactic:
simp only [integralNormalization_coeff, mem_support_iff]

Result:
case neg.h
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : ¬f = 0
i : ℕ
⊢ f.coeff i ≠ 0 → (if f.degree = ↑i then 1 else f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)) ≠ 0

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
hf : f = 0
⊢ f.integralNormalization.support = f.support

Tactic:
simp [hf]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
⊢ f.integralNormalization.support = f.support

Tactic:
have : IsDomain R := {}

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : IsCancelMulZero R
f : R[X]
a✝ : Nontrivial R
this : IsDomain R
⊢ f.integralNormalization.support = f.support