Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
⊢ ∃ g, φ (derivative f) * φ y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

Tactic:
have H'' : IsIntegral R[X] (f.derivative * y %ₘ f) := by
    refine .tower_bot (B := S'[X]) (map_injective _ (FaithfulSMul.algebraMap_injective S S')) ?_
    simp only [algebraMap_def, coe_mapRingHom, H]
    refine .multiset_sum ?_
    simp only [Multiset.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    refine fun a ham ↦ .mul (.multiset_prod ?_) ?_
    · simp only [Multiset.mem_map, Polynomial.isIntegral_iff_isIntegral_coeff, forall_exists_index,
        and_imp, forall_apply_eq_imp_iff₂, coeff_sub]
      exact fun b hbm n ↦ .sub (by simp [coeff_X, apply_ite, isIntegral_one, isIntegral_zero])
        (by simp [coeff_C, apply_ite, isIntegral_zero, hm' b (Multiset.mem_of_mem_erase hbm)])
    · simpa [isIntegral_iff_isIntegral_coeff, coeff_C, apply_ite, isIntegral_zero] using H' a ham

Goal state after:
case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
H'' : IsIntegral R[X] (derivative f * y %ₘ f)
⊢ ∃ g, φ (derivative f) * φ y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)