-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem mem_closure_iff {s : Set R} {x} :
    x ∈ closure s ↔ x ∈ AddSubgroup.closure (Subsemigroup.closure s : Set R) :=
  ⟨fun h => by
    induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)
    | zero => exact zero_mem _
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg x _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | one_left => simpa using zero_mem _
      | one_right => simpa using zero_mem _
      | mul_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | mul_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | inv_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | inv_right _ _ _ _ h => simpa [mul_neg] using neg_mem h,
  fun h => by
    induction h using AddSubgroup.closure_induction with
    | mem _ hx => induction hx using Subsemigroup.closure_induction with
      | mem _ h => exact subset_closure h
      | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
    | one => exact zero_mem _
    | mul _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
    | inv _ _ h => exact neg_mem h⟩

Proof state:
case add
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ + y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
exact add_mem hx hy

Result:
no goals

Proof state:
case mul.inv_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * -y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa [mul_neg] using neg_mem h

Result:
no goals

Proof state:
case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
_hx : x✝ ∈ closure s
_hy : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
clear _hx _hy

Result:
case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Proof state:
case mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ : R
hx : x✝ ∈ s
⊢ x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)

Result:
no goals

Proof state:
case mul.one_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝ x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ 0 * x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa using zero_mem _

Result:
no goals

Proof state:
case one
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ 0 ∈ closure s

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
case mem.mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ Subsemigroup.closure s
hy✝ : y✝ ∈ Subsemigroup.closure s
h₁ : x✝ ∈ closure s
h₂ : y✝ ∈ closure s
⊢ x✝ * y✝ ∈ closure s

Tactic:
exact mul_mem h₁ h₂

Result:
no goals

Proof state:
case mul
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ ∈ closure s
h₂ : y✝ ∈ closure s
⊢ x✝ + y✝ ∈ closure s

Tactic:
exact add_mem h₁ h₂

Result:
no goals

Proof state:
case mul.mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx : x✝ ∈ ↑(Subsemigroup.closure s)
hy : y✝ ∈ ↑(Subsemigroup.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
exact AddSubgroup.subset_closure (mul_mem hx hy)

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ 0 ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ x : R
hx✝ : x ∈ closure s
hx : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
exact neg_mem hx

Result:
no goals

Proof state:
case inv
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ ∈ closure s
⊢ -x✝ ∈ closure s

Tactic:
exact neg_mem h

Result:
no goals

Proof state:
case mul.mul_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ y✝ z✝ x✝ : R
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * (y✝ + z✝) ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa [mul_add] using add_mem h₁ h₂

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x ∈ closure s

Tactic:
induction h using AddSubgroup.closure_induction with
| mem _ hx => induction hx using Subsemigroup.closure_induction with
  | mem _ h => exact subset_closure h
  | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
| one => exact zero_mem _
| mul _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
| inv _ _ h => exact neg_mem h

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ closure s
⊢ x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
induction h using closure_induction with
| mem _ hx => exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)
| zero => exact zero_mem _
| add _ _ _ _ hx hy => exact add_mem hx hy
| neg x _ hx => exact neg_mem hx
| mul _ _ _hx _hy hx hy =>
  clear _hx _hy
  induction hx, hy using AddSubgroup.closure_induction₂ with
  | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
  | one_left => simpa using zero_mem _
  | one_right => simpa using zero_mem _
  | mul_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
  | mul_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
  | inv_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
  | inv_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

Result:
no goals

Proof state:
case mem
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ : R
hx : x✝ ∈ ↑(Subsemigroup.closure s)
⊢ x✝ ∈ closure s

Tactic:
induction hx using Subsemigroup.closure_induction with
| mem _ h => exact subset_closure h
| mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂

Result:
no goals

Proof state:
case mul.inv_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ -x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa [neg_mul] using neg_mem h

Result:
no goals

Proof state:
case mul.mul_left
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ z✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hz✝ : z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₂ : y✝ * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ (x✝ + y✝) * z✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa [add_mul] using add_mem h₁ h₂

Result:
no goals