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

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
⊢ J ⊔ J' = ⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
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 ∈ ↑⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩

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 ∈ ↑⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
Tactic:
refine' ⟨fun ⟨h, _⟩ => h, fun h => ⟨h, _⟩⟩
State after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
h : x ∈ ↑⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
⊢ x ∈ ↑I

State before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
h : x ∈ ↑⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
⊢ x ∈ ↑I
Tactic:
rw [coe_mk, Submodule.mem_sInf] at h
State after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
h : ∀ p ∈ {B | ↑J ≤ B ∧ ↑J' ≤ B}, x ∈ p
⊢ x ∈ ↑I

State before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
h : ∀ p ∈ {B | ↑J ≤ B ∧ ↑J' ≤ B}, x ∈ p
⊢ x ∈ ↑I
Tactic:
exact h I ⟨J.2, J'.2⟩
State after:
no goals