-- Mathlib/NumberTheory/KummerDedekind.lean
theorem normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span
    (hI : I.IsMaximal) {Q : R[X]}
    (hQ : Q.map (Ideal.Quotient.mk I) ∈ normalizedFactors ((minpoly R x).map (Ideal.Quotient.mk I)))
    (hI' : I ≠ ⊥) (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) :
    ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨_, hQ⟩).val =
    span (I.map (algebraMap R S) ∪ {Q.aeval x})

Proof state:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) (Ideal.map (algebraMap R S) I) ≤
    span {(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)}

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : S ⧸ Ideal.map (algebraMap R S) I
ha' :
  (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) a =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q) * a'
b : S
hb : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) b = a'
⊢ a ∈ span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
rw [← hb, ← _root_.map_mul, Quotient.mk_eq_mk_iff_sub_mem] at ha'

Result:
case intro.intro
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : S ⧸ Ideal.map (algebraMap R S) I
b : S
ha' : a - (aeval x) Q * b ∈ Ideal.map (algebraMap R S) I
hb : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) b = a'
⊢ a ∈ span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Proof state:
case intro
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : S ⧸ Ideal.map (algebraMap R S) I
ha' :
  (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) a =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q) * a'
⊢ a ∈ span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective a'

Result:
case intro.intro
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : S ⧸ Ideal.map (algebraMap R S) I
ha' :
  (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) a =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q) * a'
b : S
hb : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) b = a'
⊢ a ∈ span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Proof state:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
ha :
  (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q) ∣
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) a
⊢ a ∈ span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
obtain ⟨a', ha'⟩ := ha

Result:
case intro
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : S ⧸ Ideal.map (algebraMap R S) I
ha' :
  (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) a =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q) * a'
⊢ a ∈ span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Proof state:
case intro.intro
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
a' : S ⧸ Ideal.map (algebraMap R S) I
b : S
ha' : a - (aeval x) Q * b ∈ Ideal.map (algebraMap R S) I
hb : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) b = a'
⊢ ∃ a_1, ∃ b ∈ Ideal.map (algebraMap R S) I, a_1 * (aeval x) Q + b = a

Tactic:
exact ⟨b, a - Q.aeval x * b, ha', by ring⟩

Result:
no goals

Proof state:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
ha :
  a ∈
    comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (span {(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)})
⊢ a ∈ span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
rw [mem_comap, Ideal.mem_span_singleton] at ha

Result:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
a : S
ha :
  (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q) ∣
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) a
⊢ a ∈ span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})