Theorem: Ideal.spanIntNorm_mul_spanIntNorm_le (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)
I J : Ideal S
⊢ spanIntNorm R I * spanIntNorm R J ≤ spanIntNorm R (I * J)
Tactic:
rw [spanIntNorm, spanIntNorm, spanIntNorm, Ideal.span_mul_span', ← Set.image_mul]
State after:
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)
I J : Ideal S
⊢ span (⇑(Algebra.intNorm R S) '' (↑I * ↑J)) ≤ span (⇑(Algebra.intNorm R S) '' ↑(I * J))

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)
I J : Ideal S
⊢ span (⇑(Algebra.intNorm R S) '' (↑I * ↑J)) ≤ span (⇑(Algebra.intNorm R S) '' ↑(I * J))
Tactic:
refine Ideal.span_mono (Set.monotone_image ?_)
State after:
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)
I J : Ideal S
⊢ ↑I * ↑J ≤ ↑(I * J)

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)
I J : Ideal S
⊢ ↑I * ↑J ≤ ↑(I * J)
Tactic:
rintro _ ⟨x, hxI, y, hyJ, rfl⟩
State after:
case intro.intro.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)
I J : Ideal S
x : S
hxI : x ∈ ↑I
y : S
hyJ : y ∈ ↑J
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(I * J)

State before:
case intro.intro.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)
I J : Ideal S
x : S
hxI : x ∈ ↑I
y : S
hyJ : y ∈ ↑J
⊢ (fun x x_1 => x * x_1) x y ∈ ↑(I * J)
Tactic:
exact Ideal.mul_mem_mul hxI hyJ
State after:
no goals