case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s
ext x
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
refine' ⟨fun hx => _, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
case h.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
⊢ x ∈ (fun t => ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s
rintro - ⟨H, rfl⟩
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
⊢ x ∈ (fun h => ↑H) J
case h.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
⊢ x ∈ (fun t => ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H
rintro - ⟨J, rfl⟩
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑(toAddSubmonoid H)
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
⊢ x ∈ (fun h => ↑H) J
refine' (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => _
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubmonoid
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑(toAddSubmonoid H)
refine' (Submonoid.mem_closure.mp hy) H.toSubmonoid fun z hz => _
no goals
case h.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubmonoid
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw