-- Mathlib/RingTheory/Localization/Integral.lean
theorem integerNormalization_spec (p : S[X]) :
    ∃ b : M, ∀ i, algebraMap R S ((integerNormalization M p).coeff i) = (b : R) • p.coeff i

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∈ p.support
⊢ (algebraMap R S) (Classical.choose ⋯) = ↑(Classical.choose ⋯) • p.coeff i

Tactic:
exact
  Classical.choose_spec
    (Classical.choose_spec (exist_integer_multiples_of_finset M (p.support.image p.coeff))
      (p.coeff i) (Finset.mem_image.mpr ⟨i, hi, rfl⟩))

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ (algebraMap R S) ((integerNormalization M p).coeff i) = ↑(Classical.choose ⋯) • p.coeff i

Tactic:
rw [integerNormalization_coeff, coeffIntegerNormalization]

Result:
case h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ (algebraMap R S) (if hi : i ∈ p.support then Classical.choose ⋯ else 0) = ↑(Classical.choose ⋯) • p.coeff i

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
⊢ ∃ b, ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i

Tactic:
use Classical.choose (exist_integer_multiples_of_finset M (p.support.image p.coeff))

Result:
case h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
⊢ ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑(Classical.choose ⋯) • p.coeff i

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∉ p.support
⊢ (algebraMap R S) 0 = ↑(Classical.choose ⋯) • p.coeff i

Tactic:
rw [RingHom.map_zero, not_mem_support_iff.mp hi, smul_zero]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
⊢ ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑(Classical.choose ⋯) • p.coeff i

Tactic:
intro i

Result:
case h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ (algebraMap R S) ((integerNormalization M p).coeff i) = ↑(Classical.choose ⋯) • p.coeff i

Proof state:
case h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ (algebraMap R S) (if hi : i ∈ p.support then Classical.choose ⋯ else 0) = ↑(Classical.choose ⋯) • p.coeff i

Tactic:
split_ifs with hi

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∈ p.support
⊢ (algebraMap R S) (Classical.choose ⋯) = ↑(Classical.choose ⋯) • p.coeff i

case neg
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∉ p.support
⊢ (algebraMap R S) 0 = ↑(Classical.choose ⋯) • p.coeff i