-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanNorm_mul_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
    spanNorm R (I * J) = spanNorm R I * spanNorm R J

Proof state:
case inr.inl
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R J

Tactic:
rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J

Tactic:
rcases eq_bot_or_top (spanNorm R J) with hJ | hJ

Result:
case inr.inl
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R J

case inr.inr
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J

Proof state:
case inl
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ ⊥ ≤ ⊥ * spanNorm R J

Tactic:
exact bot_le

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J

Tactic:
rw [hI, Ideal.top_mul]

Result:
case inr
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J

Proof state:
case inl
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J

Tactic:
rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]

Result:
case inl
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ ⊥ ≤ ⊥ * spanNorm R J

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J

Tactic:
rcases eq_bot_or_top (spanNorm R I) with hI | hI

Result:
case inl
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊥
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J

case inr
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J

Proof state:
case inr.inr
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case inr.inr
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ spanNorm R J

Tactic:
rw [hJ]

Result:
case inr.inr
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤
I J : Ideal S
hI : spanNorm R I = ⊤
hJ : spanNorm R J = ⊤
⊢ spanNorm R (I * J) ≤ ⊤