Theorem: Ideal.spanIntNorm_eq_bot_iff (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
I : Ideal S
⊢ spanIntNorm R I = ⊥ ↔ I = ⊥
Tactic:
simp only [spanIntNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def]
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
I : Ideal S
⊢ (∀ a ∈ I, a = 0) ↔ ∀ ⦃x : S⦄, x ∈ I → x ∈ ⊥

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
I : Ideal S
⊢ (∀ a ∈ I, a = 0) ↔ ∀ ⦃x : S⦄, x ∈ I → x ∈ ⊥
Tactic:
rfl
State after:
no goals