awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
t : Set N
p :
  (x : M) →
    (y : N) → Membership.mem (γ := Submodule R M) (span R s) x → Membership.mem (γ := Submodule R N) (span R t) y → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : Membership.mem (γ := Submodule R N) (span R t) y), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : Membership.mem (γ := Submodule R M) (span R s) a
x y : N
hx : Membership.mem (γ := Submodule R N) (span R t) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
h₁ : p a x ha hx
h₂ : p a y ha hy
⊢ p a (x + y) ha ⋯

Tactic:
add_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
t : Set N
p :
  (x : M) →
    (y : N) → Membership.mem (γ := Submodule R M) (span R s) x → Membership.mem (γ := Submodule R N) (span R t) y → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : Membership.mem (γ := Submodule R N) (span R t) y), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : Membership.mem (γ := Submodule R M) (span R s) a
x y : N
hx : Membership.mem (γ := Submodule R N) (span R t) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
h₁ : p a x ha hx
h₂ : p a y ha hy
⊢ p a (x + y) ha ⋯

Tactic:
exact add_right _ _ _ _ _ _ h₁ h₂
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
t : Set N
p :
  (x : M) →
    (y : N) → Membership.mem (γ := Submodule R M) (span R s) x → Membership.mem (γ := Submodule R N) (span R t) y → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : Membership.mem (γ := Submodule R N) (span R t) y), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : Membership.mem (γ := Submodule R M) (span R s) a
a_1 : R
x : N
hx : Membership.mem (γ := Submodule R N) (span R t) x
h : p a x ha hx
⊢ p a (a_1 • x) ha ⋯

Tactic:
smul_right _ _ _ _ _ h
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
t : Set N
p :
  (x : M) →
    (y : N) → Membership.mem (γ := Submodule R M) (span R s) x → Membership.mem (γ := Submodule R N) (span R t) y → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : Membership.mem (γ := Submodule R N) (span R t) y), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : Membership.mem (γ := Submodule R M) (span R s) a
a_1 : R
x : N
hx : Membership.mem (γ := Submodule R N) (span R t) x
h : p a x ha hx
⊢ p a (a_1 • x) ha ⋯

Tactic:
exact smul_right _ _ _ _ _ h
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
t : Set N
p :
  (x : M) →
    (y : N) → Membership.mem (γ := Submodule R M) (span R s) x → Membership.mem (γ := Submodule R N) (span R t) y → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : Membership.mem (γ := Submodule R N) (span R t) y), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y) (hz : Membership.mem (γ := Submodule R N) (span R t) z),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x : M) (y : N) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : Membership.mem (γ := Submodule R M) (span R s) a
hb : Membership.mem (γ := Submodule R N) (span R t) b
mem : ∀ (z : N) (hz : z ∈ t), p a z ha ⋯
zero : p a 0 ha ⋯
add :
  ∀ (x y : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y) (h₁ : p a x ha hx) (h₂ : p a y ha hy), p a (x + y) ha ⋯
smul : ∀ (a_1 : R) (x : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x) (h : p a x ha hx), p a (a_1 • x) ha ⋯
⊢ p a b ha hb

Tactic:
induction hb using span_induction with
  | mem z hz => induction ha using span_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | zero => exact zero_left _ _
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
  | zero => exact zero_right a ha
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | smul _ _ _ h => exact smul_right _ _ _ _ _ h

Premises used: Submodule.smul, Submodule.zero, Submodule.add
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ Eq (α := AddSubmonoid M) (toAddSubmonoid (span R s)) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))

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

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
refine :
  ∀ (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x),
    Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
refine₁ :
  ∀ (x : M) (hx : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x),
    Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid (span R s)) x
⊢ Eq (α := AddSubmonoid M) (toAddSubmonoid (span R s)) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))

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

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x_1 x : M
hx : x ∈ s
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x

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

Premises used: trivial, AddSubmonoid.subset_closure, one_smul, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x_1 x : M
hx : x ∈ s
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x

Tactic:
exact subset_closure ⟨1, trivial, x, hx, one_smul R x⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x x_1 y : M
hx : Membership.mem (γ := Submodule R M) (span R s) x_1
hy : Membership.mem (γ := Submodule R M) (span R s) y
h₁ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x_1
h₂ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (x_1 + y)

Tactic:
add_mem h₁ h₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x x_1 y : M
hx : Membership.mem (γ := Submodule R M) (span R s) x_1
hy : Membership.mem (γ := Submodule R M) (span R s) y
h₁ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x_1
h₂ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (x_1 + y)

Tactic:
exact add_mem h₁ h₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
r₁ : R
y x_1 : M
h : x_1 ∈ HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s
smul :
  ∀ (r₂ : R) (x : M) (hx : x ∈ s),
    Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))
      (HSMul.hSMul (β := M) r₁ ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ x))
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • x_1)

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

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x_1 : M
r₁ : R
y : M
r₂ : R
x : M
hx : x ∈ s
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))
    (HSMul.hSMul (β := M) r₁ ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ x))

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

Premises used: trivial, HMul.hMul, AddSubmonoid.subset_closure, And.intro, Exists.intro, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x_1 : M
r₁ : R
y : M
r₂ : R
x : M
hx : x ∈ s
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))
    (HSMul.hSMul (β := M) r₁ ((fun (x1 : R) (x2 : M) ↦ x1 • x2) r₂ x))

Tactic:
exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
r₁ : R
y : M
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))
    (HSMul.hSMul (β := M) r₁ 0)

Tactic:
simp only [smul_zero, zero_mem]

Premises used: smul_zero, ZeroMemClass.zero_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
r₁ : R
y x_1 y_1 : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x_1
hy : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y_1
h₁ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • x_1)
h₂ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • y_1)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • (x_1 + y_1))

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

Premises used: AddMemClass.add_mem, smul_add
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
r₁ : R
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y
smul :
  ∀ (x : M) (h : x ∈ HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s),
    Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • x)
smul₁ :
  Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))
    (HSMul.hSMul (β := M) r₁ 0)
smul₂ :
  ∀ (x y : M),
    Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x →
      Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y →
        ∀
          (h₁ :
            Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • x))
          (h₂ :
            Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • y)),
          Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))
            (r₁ • (x + y))
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • y)

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

Premises used: smul_zero, Submodule.zero, ZeroMemClass.zero_mem, Submodule.add, smul_add, rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
mem :
  ∀ (x : M) (hx : x ∈ s),
    Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
zero : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) 0
add :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (span R s) x →
      Membership.mem (γ := Submodule R M) (span R s) y →
        ∀ (h₁ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x)
          (h₂ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y),
          Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (x + y)
smul :
  ∀ (r₁ : R) (y : M) (_h : Membership.mem (γ := Submodule R M) (span R s) y)
    (hy : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) y),
    Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • y)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x

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 closure_induction with
      | mem _ h =>
        obtain ⟨r₂, -, x, hx, rfl⟩ := h
        exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
      | zero => simp only [smul_zero, zero_mem]
      | add _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂

Premises used: smul_zero, Submodule.smul, Submodule.zero, ZeroMemClass.zero_mem, Submodule.add, smul_add, rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x

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 closure_induction with
      | mem _ h =>
        obtain ⟨r₂, -, x, hx, rfl⟩ := h
        exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩
      | zero => simp only [smul_zero, zero_mem]
      | add _ _ _ _ h₁ h₂ => simpa only [smul_add] using add_mem h₁ h₂

Premises used: smul_zero, Submodule.smul, Submodule.zero, ZeroMemClass.zero_mem, Submodule.add, smul_add, rfl
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
⊢ Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid (span R s)) x

Tactic:
closure_le.2 ?_ hx

Premises used: Iff.mpr, AddSubmonoid.closure_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
refine : HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s ⊆ (↑(toAddSubmonoid (span R s)) : Set M)
⊢ Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid (span R s)) x

Tactic:
refine closure_le.2 ?_ hx

Premises used: Iff.mpr, AddSubmonoid.closure_le
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x_1 : M
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x_1
r : R
x : M
hx : x ∈ s
⊢ (fun (x1 : R) (x2 : M) ↦ x1 • x2) r x ∈ (↑(toAddSubmonoid (span R s)) : Set M)

Tactic:
smul_mem _ _ (subset_span hx)

Premises used: Set.Mem, Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x_1 : M
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x_1
r : R
x : M
hx : x ∈ s
⊢ (fun (x1 : R) (x2 : M) ↦ x1 • x2) r x ∈ (↑(toAddSubmonoid (span R s)) : Set M)

Tactic:
exact smul_mem _ _ (subset_span hx)

Premises used: Submodule.subset_span, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
case : HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s ⊆ (↑(toAddSubmonoid (span R s)) : Set M)
case₁ : ∀ (r : R) (x : M) (hx : x ∈ s), (fun (x1 : R) (x2 : M) ↦ x1 • x2) r x ∈ (↑(toAddSubmonoid (span R s)) : Set M)
⊢ Membership.mem (γ := AddSubmonoid M) (toAddSubmonoid (span R s)) x

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

Premises used: Iff.mpr, AddSubmonoid.closure_le, Submodule.subset_span, rfl, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Span.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
p : (x : M) → Membership.mem (γ := Submodule R M) (span R s) x → Prop
zero : p 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y), p x hx → p y hy → p (x + y) ⋯
smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
v : M
⊢ Membership.mem (γ := Submodule R M) (span R s) v ↔
    Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) v

Tactic:
simp [← span_eq_closure]

Premises used: Submodule.span_eq_closure