R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
⊢ ∀ (i : ℕ),
    ↑(algebraMap R S) (coeff (integerNormalization M p) i) =
      ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
⊢ ∃ b, ∀ (i : ℕ), ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
use Classical.choose (exist_integer_multiples_of_finset M (p.support.image p.coeff))
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ ↑(algebraMap R S) (coeff (integerNormalization M p) i) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
⊢ ∀ (i : ℕ),
    ↑(algebraMap R S) (coeff (integerNormalization M p) i) =
      ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
intro i
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ ↑(algebraMap R S) (coeff (integerNormalization M p) i) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
rw [integerNormalization_coeff, coeffIntegerNormalization]
case inl
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∈ support p
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i

case inr
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : ¬i ∈ support p
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
split_ifs with hi
case inl
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∈ support p
⊢ ↑(algebraMap R S)
      (choose
        (_ :
          IsInteger R
            (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
              coeff p i))) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
case inl
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∈ support p
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
rw [dif_pos hi]
no goals
case inl
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∈ support p
⊢ ↑(algebraMap R S)
      (choose
        (_ :
          IsInteger R
            (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
              coeff p i))) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
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⟩))
case inr
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : ¬i ∈ support p
⊢ ↑(algebraMap R S) 0 =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
case inr
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : ¬i ∈ support p
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
rw [dif_neg hi]
no goals
case inr
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.15519
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : ¬i ∈ support p
⊢ ↑(algebraMap R S) 0 =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
rw [RingHom.map_zero, not_mem_support_iff.mp hi, smul_zero]