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

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

State before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
⊢ x ∈ ↑(J ⊓ J') ↔ x ∈ ↑⟨↑J ⊓ ↑J', ⋯⟩
Tactic:
exact ⟨fun ⟨h, _⟩ => h, fun h => ⟨h, J.property h.left⟩⟩
State after:
no goals