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

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
⊢ sInf S = ⟨sInf (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 ∈ ↑(sInf S) ↔ x ∈ ↑⟨sInf (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 ∈ ↑(sInf S) ↔ x ∈ ↑⟨sInf (val '' S) ⊓ I, ⋯⟩
Tactic:
rfl
State after:
no goals