-- Mathlib/RingTheory/Localization/Integral.lean
theorem integerNormalization_eq_zero_iff {p : K[X]} :
    integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0

Proof state:
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
⊢ (∀ (n : ℕ), p.coeff n = coeff 0 n) ↔ ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n

Tactic:
obtain ⟨⟨b, nonzero⟩, hb⟩ := integerNormalization_spec (nonZeroDivisors A) p

Result:
case intro.mk
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
⊢ (∀ (n : ℕ), p.coeff n = coeff 0 n) ↔ ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n

Proof state:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (algebraMap A K) ↑⟨b, nonzero⟩ * p.coeff i = 0
⊢ ¬(algebraMap A K) ↑⟨b, nonzero⟩ = 0

Tactic:
intro h

Result:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h✝ : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (algebraMap A K) ↑⟨b, nonzero⟩ * p.coeff i = 0
h : (algebraMap A K) ↑⟨b, nonzero⟩ = 0
⊢ False

Proof state:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (integerNormalization (nonZeroDivisors A) p).coeff i = coeff 0 i
⊢ p.coeff i = coeff 0 i

Tactic:
rw [Polynomial.coeff_zero, ← @to_map_eq_zero_iff A _ K, hb i, Algebra.smul_def] at hi

Result:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (algebraMap A K) ↑⟨b, nonzero⟩ * p.coeff i = 0
⊢ p.coeff i = coeff 0 i

Proof state:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
⊢ p.coeff i = coeff 0 i

Tactic:
have hi := h i

Result:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (integerNormalization (nonZeroDivisors A) p).coeff i = coeff 0 i
⊢ p.coeff i = coeff 0 i

Proof state:
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
⊢ integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0

Tactic:
refine Polynomial.ext_iff.trans (Polynomial.ext_iff.trans ?_).symm

Result:
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
⊢ (∀ (n : ℕ), p.coeff n = coeff 0 n) ↔ ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n

Proof state:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h✝ : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (algebraMap A K) ↑⟨b, nonzero⟩ * p.coeff i = 0
h : (algebraMap A K) ↑⟨b, nonzero⟩ = 0
⊢ False

Tactic:
apply mem_nonZeroDivisors_iff_ne_zero.mp nonzero

Result:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h✝ : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (algebraMap A K) ↑⟨b, nonzero⟩ * p.coeff i = 0
h : (algebraMap A K) ↑⟨b, nonzero⟩ = 0
⊢ b = 0

Proof state:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (algebraMap A K) ↑⟨b, nonzero⟩ * p.coeff i = 0
⊢ p.coeff i = coeff 0 i

Tactic:
apply Or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hi)

Result:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (algebraMap A K) ↑⟨b, nonzero⟩ * p.coeff i = 0
⊢ ¬(algebraMap A K) ↑⟨b, nonzero⟩ = 0

Proof state:
case intro.mk.mp
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), p.coeff n = coeff 0 n
i : ℕ
⊢ (integerNormalization (nonZeroDivisors A) p).coeff i = coeff 0 i

Tactic:
rw [coeff_zero, ← to_map_eq_zero_iff (K := K), hb i, h i, coeff_zero, smul_zero]

Result:
no goals

Proof state:
case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h✝ : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
hi : (algebraMap A K) ↑⟨b, nonzero⟩ * p.coeff i = 0
h : (algebraMap A K) ↑⟨b, nonzero⟩ = 0
⊢ b = 0

Tactic:
exact to_map_eq_zero_iff.mp h

Result:
no goals