case h
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
⊢ x✝ ∈ nonUnitalSubsemiringClosure M ↔ x✝ ∈ NonUnitalSubsemiring.closure ↑M
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
⊢ nonUnitalSubsemiringClosure M = NonUnitalSubsemiring.closure ↑M
ext
case h.refine_1.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ nonUnitalSubsemiringClosure M
H1 : NonUnitalSubsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h => ↑H1) H2

case h.refine_2.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h => ↑H1) H2
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
⊢ x✝ ∈ nonUnitalSubsemiringClosure M ↔ x✝ ∈ NonUnitalSubsemiring.closure ↑M
refine ⟨fun hx => ?_,
  fun hx => (NonUnitalSubsemiring.mem_closure.mp hx) M.nonUnitalSubsemiringClosure fun s sM => ?_⟩
<;> rintro - ⟨H1, rfl⟩
<;> rintro - ⟨H2, rfl⟩
no goals
case h.refine_1.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ nonUnitalSubsemiringClosure M
H1 : NonUnitalSubsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h => ↑H1) H2
exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
no goals
case h.refine_2.intro.intro
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h => ↑H1) H2
exact H2 sM