-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem closure_addSubmonoid_closure {s : Set R} :
    closure ↑(AddSubmonoid.closure s) = closure s

Proof state:
case h
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s

Tactic:
refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩

Result:
case h
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s

Proof state:
case h.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
⊢ x ∈ (fun t => ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H

Tactic:
rintro - ⟨J, rfl⟩

Result:
case h.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
⊢ x ∈ (fun h => ↑H) J

Proof state:
case h.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑H.toAddSubmonoid

Tactic:
refine (Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => ?_

Result:
case h.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubsemigroup

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s

Tactic:
ext x

Result:
case h
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s

Proof state:
case h.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubsemigroup

Tactic:
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

Result:
no goals

Proof state:
case h.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
⊢ x ∈ (fun h => ↑H) J

Tactic:
refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_

Result:
case h.intro.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑H.toAddSubmonoid

Proof state:
case h
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s

Tactic:
rintro - ⟨H, rfl⟩

Result:
case h.intro
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
⊢ x ∈ (fun t => ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H