Theorem: Subideal.sSup_def (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
⊢ sSup S = ⟨sSup (val '' S) ⊓ I, ⋯⟩
Tactic:
ext x
State after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
x : A
⊢ x ∈ ↑(sSup S) ↔ x ∈ ↑⟨sSup (val '' S) ⊓ I, ⋯⟩

State before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
x : A
⊢ x ∈ ↑(sSup S) ↔ x ∈ ↑⟨sSup (val '' S) ⊓ I, ⋯⟩
Tactic:
rfl
State after:
no goals