Theorem: Ideal.spanIntNorm_singleton (FltRegular/NumberTheory/IdealNorm.lean)

State before:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
r : S
x : R
hx : x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ x
Tactic:
obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
State after:
case intro.intro
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
r x : S
hx' : x ∈ ↑(span {r})
hx : (Algebra.intNorm R S) x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ (Algebra.intNorm R S) x

State before:
case intro.intro
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain R
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹ : IsIntegrallyClosed S
inst✝ : IsSeparable (FractionRing R) (FractionRing S)
r x : S
hx' : x ∈ ↑(span {r})
hx : (Algebra.intNorm R S) x ∈ ⇑(Algebra.intNorm R S) '' ↑(span {r})
⊢ (Algebra.intNorm R S) r ∣ (Algebra.intNorm R S) x
Tactic:
exact map_dvd _ (mem_span_singleton.mp hx')
State after:
no goals