-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_eq_closure {s : Set M} : (span R s).toAddSubmonoid = closure (@univ R • s)

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : M
hx✝ : x✝ ∈ closure (univ • s)
r : R
x : M
hx : x ∈ s
⊢ (fun x1 x2 => x1 • x2) r x ∈ ↑(span R s).toAddSubmonoid

Tactic:
exact smul_mem _ _ (subset_span hx)

Result:
no goals

Proof state:
case mem
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ x : M
hx : x ∈ s
⊢ x ∈ closure (univ • s)

Tactic:
exact subset_closure ⟨1, trivial, x, hx, one_smul R x⟩

Result:
no goals

Proof state:
case smul.one
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y : M
⊢ r₁ • 0 ∈ closure (univ • s)

Tactic:
simpa only [smul_zero] using zero_mem _

Result:
no goals

Proof state:
case smul.mem.intro.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : M
r₁ : R
y : M
r₂ : R
x : M
hx : x ∈ s
⊢ r₁ • (fun x1 x2 => x1 • x2) r₂ x ∈ closure (univ • s)

Tactic:
exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ span R s
⊢ x ∈ closure (univ • s)

Tactic:
induction hx using span_induction with
| mem x hx => exact subset_closure ⟨1, trivial, x, hx, one_smul R x⟩
| zero => exact zero_mem _
| add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
| smul r₁ y _h hy =>
  clear _h
  induction hy using AddSubmonoid.closure_induction with
  | mem _ h =>
    obtain ⟨r₂, -, x, hx, rfl⟩ := h
    exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
  | one => simpa only [smul_zero] using zero_mem _
  | mul _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂

Result:
no goals

Proof state:
case smul.mul
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y x✝ y✝ : M
hx✝ : x✝ ∈ closure (univ • s)
hy✝ : y✝ ∈ closure (univ • s)
h₁ : r₁ • x✝ ∈ closure (univ • s)
h₂ : r₁ • y✝ ∈ closure (univ • s)
⊢ r₁ • (x✝ + y✝) ∈ closure (univ • s)

Tactic:
simpa only [smul_add] using add_mem h₁ h₂

Result:
no goals

Proof state:
case smul
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y : M
hy : y ∈ closure (univ • s)
⊢ r₁ • y ∈ closure (univ • s)

Tactic:
induction hy using AddSubmonoid.closure_induction with
| mem _ h =>
  obtain ⟨r₂, -, x, hx, rfl⟩ := h
  exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
| one => simpa only [smul_zero] using zero_mem _
| mul _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂

Result:
no goals

Proof state:
case of_mem_span
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ span R s
⊢ x ∈ closure (univ • s)

case of_mem_closure
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ x ∈ (span R s).toAddSubmonoid

Tactic:
case of_mem_span =>
  induction hx using span_induction with
  | mem x hx => exact subset_closure ⟨1, trivial, x, hx, one_smul R x⟩
  | zero => exact zero_mem _
  | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
  | smul r₁ y _h hy =>
    clear _h
    induction hy using AddSubmonoid.closure_induction with
    | mem _ h =>
      obtain ⟨r₂, -, x, hx, rfl⟩ := h
      exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
    | one => simpa only [smul_zero] using zero_mem _
    | mul _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂

Result:
case of_mem_closure
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ x ∈ (span R s).toAddSubmonoid

Proof state:
case smul
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y : M
_h : y ∈ span R s
hy : y ∈ closure (univ • s)
⊢ r₁ • y ∈ closure (univ • s)

Tactic:
clear _h

Result:
case smul
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y : M
hy : y ∈ closure (univ • s)
⊢ r₁ • y ∈ closure (univ • s)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ univ • s ⊆ ↑(span R s).toAddSubmonoid

Tactic:
rintro - ⟨r, -, x, hx, rfl⟩

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : M
hx✝ : x✝ ∈ closure (univ • s)
r : R
x : M
hx : x ∈ s
⊢ (fun x1 x2 => x1 • x2) r x ∈ ↑(span R s).toAddSubmonoid

Proof state:
case zero
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ 0 ∈ closure (univ • s)

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ x ∈ (span R s).toAddSubmonoid

Tactic:
refine closure_le.2 ?_ hx

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ univ • s ⊆ ↑(span R s).toAddSubmonoid

Proof state:
case smul.mem
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y x✝ : M
h : x✝ ∈ univ • s
⊢ r₁ • x✝ ∈ closure (univ • s)

Tactic:
obtain ⟨r₂, -, x, hx, rfl⟩ := h

Result:
case smul.mem.intro.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : M
r₁ : R
y : M
r₂ : R
x : M
hx : x ∈ s
⊢ r₁ • (fun x1 x2 => x1 • x2) r₂ x ∈ closure (univ • s)

Proof state:
case of_mem_closure
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ x ∈ (span R s).toAddSubmonoid

Tactic:
case of_mem_closure =>
  refine closure_le.2 ?_ hx
  rintro - ⟨r, -, x, hx, rfl⟩
  exact smul_mem _ _ (subset_span hx)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).toAddSubmonoid = closure (univ • s)

Tactic:
refine le_antisymm (fun x (hx : x ∈ span R s) ↦ ?of_mem_span) (fun x hx ↦ ?of_mem_closure)

Result:
case of_mem_span
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ span R s
⊢ x ∈ closure (univ • s)

case of_mem_closure
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
hx : x ∈ closure (univ • s)
⊢ x ∈ (span R s).toAddSubmonoid

Proof state:
case add
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x x✝ y✝ : M
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
h₁ : x✝ ∈ closure (univ • s)
h₂ : y✝ ∈ closure (univ • s)
⊢ x✝ + y✝ ∈ closure (univ • s)

Tactic:
exact add_mem h₁ h₂

Result:
no goals