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

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

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

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

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

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

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

Result:
no goals

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

Tactic:
exact .inr <| ⟨x * y, ⟨x, mem_univ _, y, hy, rfl⟩, r, mem_univ _, mul_assoc ..⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ s ⊆ ↑(span s) ∧ s * univ ⊆ ↑(span s) ∧ univ * s ⊆ ↑(span s) ∧ univ * s * univ ⊆ ↑(span s)

Tactic:
exact ⟨subset_span, subset_mul_set subset_span _, set_mul_subset subset_span _,
  subset_mul_set (set_mul_subset subset_span _) _⟩

Result:
no goals

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

Tactic:
exact .inl <| .inr <| ⟨x, mem_univ _, y, hy, rfl⟩

Result:
no goals

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

Tactic:
simp [mul_assoc]

Result:
no goals

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

Tactic:
refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_

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

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

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

case refine_1.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 => x1 * x2) (x * r' * y) r = x * (fun x1 x2 => x1 * x2) ((fun x1 x2 => x1 * x2) r' y) r

Tactic:
all_goals simp [mul_assoc]

Result:
no goals

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

Tactic:
refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩

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

Proof state:
case refine_2.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z y x : R
hy : y ∈ s
⊢ y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inl <| .inl <| .inr ⟨y, hy, x, mem_univ _, rfl⟩

Result:
no goals

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

Tactic:
exact .inr <| ⟨r * y, ⟨r, mem_univ _, y, hy, rfl⟩, x, mem_univ _, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ z ∈ span s

Tactic:
refine mem_span_iff.mp h (span s) ?_

Result:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ s ∪ s * univ ∪ univ * s ∪ univ * s * univ ⊆ ↑(span s)

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
x✝ : z ∈ span s
⊢ s ⊆ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
simp only [Set.union_assoc, Set.subset_union_left]

Result:
no goals

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

Tactic:
refine .inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩

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

case refine_1.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 => x1 * x2) (x * r' * y) r = x * (fun x1 x2 => x1 * x2) ((fun x1 x2 => x1 * x2) r' y) r

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

Tactic:
rintro y x (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) |
  ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)

Result:
case refine_2.inl.inl.inl
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z y x : R
hy : y ∈ s
⊢ y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

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

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

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

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ s ∪ s * univ ∪ univ * s ∪ univ * s * univ ⊆ ↑(span s)

Tactic:
simp only [union_subset_iff, union_assoc]

Result:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
h : z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
⊢ s ⊆ ↑(span s) ∧ s * univ ⊆ ↑(span s) ∧ univ * s ⊆ ↑(span s) ∧ univ * s * univ ⊆ ↑(span s)

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

Tactic:
simp [mul_assoc]

Result:
no goals