-- Mathlib/NumberTheory/KummerDedekind.lean
theorem normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map (hI : IsMaximal I)
    (hI' : I ≠ ⊥) (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) :
    normalizedFactors (I.map (algebraMap R S)) =
      Multiset.map
        (fun f =>
          ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f : Ideal S))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach

Proof state:
case pos.hb
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  ↑(Multiset.count (normalize J) (normalizedFactors (Ideal.map (algebraMap R S) I))) =
    emultiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0

Tactic:
exact Polynomial.map_monic_ne_zero (minpoly.monic hx')

Result:
no goals

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ' : (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
⊢ Multiset.count (↑J') (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) =
    Multiset.count J
      (Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)

Tactic:
have : ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J' : Ideal S) =
    J := by
  rw [← hJ', Equiv.symm_apply_apply _ _, Subtype.coe_mk]

Result:
case pos
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this✝ :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ' : (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
this : ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') = J
⊢ Multiset.count (↑J') (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) =
    Multiset.count J
      (Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∉ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ ¬∃ a ∈ (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach,
      ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm a) = J

Tactic:
simp only [not_exists]

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∉ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ ∀ (x_1 : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}),
    ¬(x_1 ∈ (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach ∧
        ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm x_1) = J)

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
⊢ Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count J
      (Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)

Tactic:
refine this.trans ?_

Result:
case pos
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
⊢ Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) =
    Multiset.count J
      (Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)