awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
z : N
hz : z ∈ t
mem : ∀ (x : M) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : p 0 z ⋯ ⋯
⊢ p a z ha ⋯
have mem₂ : ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
  (hy : Membership.mem (γ := Submodule R M) (span R s) y) (h₁ : p x z hx sorry) (h₂ : p y z hy sorry), p (x + y) z sorry sorry
Tactic: 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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
z : N
hz : z ∈ t
mem : ∀ (x : M) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : p 0 z ⋯ ⋯
mem₂ :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y) (h₁ : p x z hx ⋯) (h₂ : p y z hy ⋯), p (x + y) z ⋯ ⋯
⊢ p a z ha ⋯
have mem₃ : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x) (h : p x z hx sorry), p (a • x) z sorry sorry
Tactic: 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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ p a b ha hb
have mem : ∀ (z : N) (hz : z ∈ t), p a z ha sorry
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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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 ⋯
⊢ p a b ha hb
have zero : p a 0 ha sorry
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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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 ⋯
⊢ p a b ha hb
have 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 sorry
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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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 ⋯
⊢ p a b ha hb
have 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 sorry
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
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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))
have 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
Tactic: refine le_antisymm (fun x (hx : x ∈ span R s) ↦ ?of_mem_span) (fun x hx ↦ ?of_mem_closure)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Eq (α := AddSubmonoid M) (toAddSubmonoid (span R s)) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))
have 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
Tactic: refine le_antisymm (fun x (hx : x ∈ span R s) ↦ ?of_mem_span) (fun x hx ↦ ?of_mem_closure)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • x_1)
have 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))
Tactic: obtain ⟨r₂, -, x, hx, rfl⟩ := h
Cleared hypotheses: x_1, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • y)
have 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)
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₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • y)
have smul₁ : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s))
  (HSMul.hSMul (β := M) r₁ 0)
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₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) (r₁ • y)
have 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))
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₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
have mem : ∀ (x : M) (hx : x ∈ s),
  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₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
have zero : Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) 0
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₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Defs (goal)
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
⊢ Membership.mem (γ := AddSubmonoid M) (closure (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) univ s)) x
have 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)
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₂
Cleared hypotheses: hx