-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem mem_closure_iff {s : Set R} {x} :
    x ∈ closure s ↔ x ∈ AddSubgroup.closure (Submonoid.closure s : Set R) :=
  ⟨fun h => by
    induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)
    | zero => exact zero_mem _
    | one => exact AddSubgroup.subset_closure (one_mem _)
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg _ _ 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 x hx =>
        induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | 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 one
R : Type u
inst✝ : Ring R
s : Set R
x : R
⊢ 0 ∈ closure s

Tactic:
exact zero_mem _

Result:
no goals

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

Tactic:
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 mul
R : Type u
inst✝ : Ring R
s : Set R
x x✝ y✝ : R
_hx : x✝ ∈ closure s
_hy : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
clear _hx _hy

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

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

Tactic:
exact zero_mem _

Result:
no goals

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

Tactic:
simpa using zero_mem _

Result:
no goals

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

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

Result:
no goals

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

Tactic:
simpa using zero_mem _

Result:
no goals

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

Tactic:
exact neg_mem hx

Result:
no goals

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

Tactic:
simpa [neg_mul] using neg_mem h

Result:
no goals

Proof state:
case one
R : Type u
inst✝ : Ring R
s : Set R
x : R
⊢ 1 ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
exact AddSubgroup.subset_closure (one_mem _)

Result:
no goals

Proof state:
case mem.mul
R : Type u
inst✝ : Ring R
s : Set R
x✝¹ x x✝ y✝ : R
hx✝ : x✝ ∈ Submonoid.closure s
hy✝ : y✝ ∈ Submonoid.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.inv_right
R : Type u
inst✝ : Ring R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * -y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa [mul_neg] using neg_mem h

Result:
no goals

Proof state:
case mul
R : Type u
inst✝ : Ring R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.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:
R : Type u
inst✝ : Ring R
s : Set R
x : R
h : x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x ∈ closure s

Tactic:
induction h using AddSubgroup.closure_induction with
| mem x hx =>
  induction hx using Submonoid.closure_induction with
  | mem _ h => exact subset_closure h
  | one => exact one_mem _
  | 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:
case mem
R : Type u
inst✝ : Ring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
⊢ x ∈ closure s

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

Result:
no goals

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

Tactic:
exact AddSubgroup.subset_closure (mul_mem hx hy)

Result:
no goals

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

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

Result:
no goals

Proof state:
case mem.mem
R : Type u
inst✝ : Ring R
s : Set R
x✝¹ x x✝ : R
h : x✝ ∈ s
⊢ x✝ ∈ closure s

Tactic:
exact subset_closure h

Result:
no goals

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

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

Result:
no goals