Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: 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✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ :
  ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') ∈
    normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'))
      (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count
      (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
          ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
hJ' :
  (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
      ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩ =
    J'
⊢ Multiset.count (↑J') (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) =
    Multiset.count J' (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach

pp: case pos.hf
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✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ :
  ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') ∈
    normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'))
      (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count
      (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
          ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
hJ' :
  (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
      ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩ =
    J'
⊢ Function.Injective fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)

Tactic:
Multiset.count_attach

Goal state after:
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✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ :
  ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') ∈
    normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'))
      (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count
      (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
          ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
hJ' :
  (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
      ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩ =
    J'
⊢ Multiset.count (↑J') (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))) =
    Multiset.count (↑J') (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))

case pos.hf
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✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ :
  ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') ∈
    normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'))
      (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count
      (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
          ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
hJ' :
  (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx')
      ⟨↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J'), hJ⟩ =
    J'
⊢ Function.Injective fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)