Lean4
theorem 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) :=
by
trans z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
· refine ⟨(span_mono (by simp only [Set.union_assoc, Set.subset_union_left]) ·), fun h ↦ ?_⟩
refine mem_span_iff.mp h (span s) ?_
simp only [union_subset_iff, union_assoc]
exact
⟨subset_span, subset_mul_set subset_span _, set_mul_subset subset_span _,
subset_mul_set (set_mul_subset subset_span _) _⟩
· refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_
· rintro x y (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) | ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)
· exact .inl <| .inr <| ⟨x, mem_univ _, y, hy, rfl⟩
· exact .inr <| ⟨x * y, ⟨x, mem_univ _, y, hy, rfl⟩, r, mem_univ _, mul_assoc ..⟩
· exact .inl <| .inr <| ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩
· refine .inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩
all_goals simp [mul_assoc]
· rintro y x (((hy | ⟨y, hy, r, -, rfl⟩) | ⟨r, -, y, hy, rfl⟩) | ⟨-, ⟨r', -, y, hy, rfl⟩, r, -, rfl⟩)
· exact .inl <| .inl <| .inr ⟨y, hy, x, mem_univ _, rfl⟩
· exact .inl <| .inl <| .inr ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩
· exact .inr <| ⟨r * y, ⟨r, mem_univ _, y, hy, rfl⟩, x, mem_univ _, rfl⟩
· refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩
simp [mul_assoc]
