Theorem: Ideal.spanIntNorm_mul_of_bot_or_top (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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Tactic:
refine le_antisymm ?_ (spanIntNorm_mul_spanIntNorm_le R _ _)
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R 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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J
Tactic:
cases' eq_bot_or_top (spanIntNorm R I) with hI hI
State after:
case inl
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊥
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J

case inr
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J

State before:
case inr
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J
Tactic:
rw [hI, Ideal.top_mul]
State after:
case inr
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J

State before:
case inr
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J
Tactic:
cases' eq_bot_or_top (spanIntNorm R J) with hJ hJ
State after:
case inr.inl
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊥
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J

case inr.inr
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J

State before:
case inr.inr
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊤
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J
Tactic:
rw [hJ]
State after:
case inr.inr
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊤
⊢ spanIntNorm R (I * J) ≤ ⊤

State before:
case inr.inr
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊤
⊢ spanIntNorm R (I * J) ≤ ⊤
Tactic:
exact le_top
State after:
no goals

State before:
case inl
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊥
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R I * spanIntNorm R J
Tactic:
rw [hI, spanIntNorm_eq_bot_iff.mp hI, bot_mul, spanIntNorm_bot]
State after:
case inl
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊥
⊢ ⊥ ≤ ⊥ * spanIntNorm R J

State before:
case inl
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊥
⊢ ⊥ ≤ ⊥ * spanIntNorm R J
Tactic:
exact bot_le
State after:
no goals

State before:
case inr.inl
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)
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanIntNorm R I = ⊤
hJ : spanIntNorm R J = ⊥
⊢ spanIntNorm R (I * J) ≤ spanIntNorm R J
Tactic:
rw [hJ, spanIntNorm_eq_bot_iff.mp hJ, mul_bot, spanIntNorm_bot]
State after:
no goals