-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma mem_span_iff_mem_addSubgroup_closure {s : Set R} {z : R} :
    z ∈ span s ↔ z ∈ AddSubgroup.closure (univ * s * univ)

Proof state:
case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
hz : z ∈ span (univ * s * univ)
⊢ z ∈ span s

Tactic:
exact mem_span_iff.mp hz (span s) <| subset_mul_set (set_mul_subset subset_span _) _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ (fun x1 x2 => x1 * x2) (1 * x) 1 = x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ AddSubgroup.closure (univ * s * univ)

Tactic:
trans z ∈ span (univ * s * univ)

Result:
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ span (univ * s * univ)

R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span (univ * s * univ) ↔ z ∈ AddSubgroup.closure (univ * s * univ)

Proof state:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (x y : R), y ∈ univ * s * univ → x * y ∈ univ * s * univ

Tactic:
intro x y hy

Result:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s * univ
⊢ x * y ∈ univ * s * univ

Proof state:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z x y : R
hy : y ∈ univ * (s * univ)
⊢ x * y ∈ univ * (s * univ)

Tactic:
obtain ⟨r, -, y, hy, rfl⟩ := hy

Result:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Ring R
s : Set R
z x r y : R
hy : y ∈ s * univ
⊢ x * (fun x1 x2 => x1 * x2) r y ∈ univ * (s * univ)

Proof state:
case refine_2.intro.intro.intro.intro
R : Type u_1
inst✝ : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s
r : R
⊢ (fun x1 x2 => x1 * x2) y r * x ∈ univ * s * univ

Tactic:
exact ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s * univ
⊢ x * y ∈ univ * s * univ

Tactic:
rw [mul_assoc] at hy ⊢

Result:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z x y : R
hy : y ∈ univ * (s * univ)
⊢ x * y ∈ univ * (s * univ)

Proof state:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ x ∈ univ * s * univ

Tactic:
exact ⟨1 * x, ⟨1, mem_univ _, x, hx, rfl⟩, 1, mem_univ _, by simp⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ z ∈ span (univ * s * univ) ↔ z ∈ AddSubgroup.closure (univ * s * univ)

Tactic:
refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_

Result:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (x y : R), y ∈ univ * s * univ → x * y ∈ univ * s * univ

case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ

Proof state:
case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ

Tactic:
rintro - x ⟨y, hy, r, -, rfl⟩

Result:
case refine_2.intro.intro.intro.intro
R : Type u_1
inst✝ : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s
r : R
⊢ (fun x1 x2 => x1 * x2) y r * x ∈ univ * s * univ

Proof state:
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Ring R
s : Set R
z x r y : R
hy : y ∈ s * univ
⊢ x * (fun x1 x2 => x1 * x2) r y ∈ univ * (s * univ)

Tactic:
exact ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩

Result:
no goals