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
pos : ∀ (h : 0 ∈ s), Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
neg : ∀ (h : 0 ∉ s), Eq (α := Submodule R M) (span R (s \ {0})) (span R s)
⊢ Eq (α := Submodule R M) (span R (s \ {0})) (span R s)

Tactic:
by_cases h : 0 ∈ s
-- 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
h : 0 ∈ s
⊢ insert 0 (s \ {0}) = s

Tactic:
simp [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
h : 0 ∈ s
pos : Eq (α := Submodule R M) (span R (insert 0 (s \ {0}))) (span R s)
pos₁ pos₂ : Eq (α := Submodule R M) (span R s) (span R s)
⊢ Eq (α := Submodule R M) (span R (s \ {0})) (span R s)

Tactic:
rw [← span_insert_zero, show insert 0 (s \ {0}) = s by simp [h]]

Premises used: Submodule.span_insert_zero
-- 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
h : 0 ∉ s
⊢ Eq (α := Submodule R M) (span R (s \ {0})) (span R s)

Tactic:
simp [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
⊢ (↑(AddSubmonoid.closure s) : Set M) ⊆ (↑(span R s) : Set M)

Tactic:
(@AddSubmonoid.closure_le _ _ _ (span R s).toAddSubmonoid).mpr subset_span

Premises used: Iff.mpr, Set.Mem, Set.Subset, AddSubmonoid.closure_le, Submodule.subset_span
-- 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
⊢ LE.le (α := AddSubmonoid M) (AddSubmonoid.closure s) (toAddSubmonoid (span R s))

Tactic:
closure_subset_span

Premises used: Set.Mem, Set.Subset, Submodule.closure_subset_span
-- 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 (α := Submodule R M) (span R (↑(AddSubmonoid.closure s) : Set M)) (span R s)

Tactic:
le_antisymm (span_le.mpr closure_subset_span) (span_mono AddSubmonoid.subset_closure)

Premises used: Iff.mpr, AddSubmonoid.subset_closure, Submodule.closure_subset_span, le_antisymm, Submodule.span_mono, Submodule.span_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
p : (x : M) → Membership.mem (γ := Submodule R M) (span R s) x → Prop
mem : ∀ (x : M) (h : x ∈ s), p x ⋯
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 : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p x hx → p (a • x) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
let : p x hx
⊢ p x hx

Tactic:
let p : Submodule R M :=
    { carrier := { x | ∃ hx, p x hx }
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩
      smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩ }
-- 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_1 : (x : M) → Membership.mem (γ := Submodule R M) (span R s) x → Prop
mem : ∀ (x : M) (h : x ∈ s), p_1 x ⋯
zero : p_1 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_1 x hx → p_1 y hy → p_1 (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p_1 x hx → p_1 (a • x) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
p : Submodule R M :=
  { carrier := {x : M | ∃ (hx : Membership.mem (γ := Submodule R M) (span R s) x), p_1 x hx}, add_mem' := ⋯,
    zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ p_1 x hx

Tactic:
span_le (p := p) |>.mpr (fun y hy ↦ ⟨subset_span hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, id, Exists.intro, Submodule.subset_span, Submodule.span_le, Exists.elim
-- 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_1 : (x : M) → Membership.mem (γ := Submodule R M) (span R s) x → Prop
mem : ∀ (x : M) (h : x ∈ s), p_1 x ⋯
zero : p_1 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_1 x hx → p_1 y hy → p_1 (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), p_1 x hx → p_1 (a • x) ⋯
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
p : Submodule R M :=
  { carrier := {x : M | ∃ (hx : Membership.mem (γ := Submodule R M) (span R s) x), p_1 x hx}, add_mem' := ⋯,
    zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ p_1 x hx

Tactic:
exact span_le (p := p) |>.mpr (fun y hy ↦ ⟨subset_span hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Premises used: Iff.mpr, Exists.intro, Submodule.subset_span, Submodule.span_le, Exists.elim
-- 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 z : N
hz : z ∈ t
x : M
h : x ∈ s
⊢ p x z ⋯ ⋯

Tactic:
mem_mem _ _ h hz
-- 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 z : N
hz : z ∈ t
x : M
h : x ∈ s
⊢ p x z ⋯ ⋯

Tactic:
exact mem_mem _ _ h hz
-- 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 z : N
hz : z ∈ t
⊢ p 0 z ⋯ ⋯

Tactic:
zero_left _ _
-- 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 z : N
hz : z ∈ t
⊢ p 0 z ⋯ ⋯

Tactic:
exact zero_left _ _
-- 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 z : N
hz : z ∈ t
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 ⋯ ⋯

Tactic:
add_left _ _ _ _ _ _ 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 z : N
hz : z ∈ t
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 ⋯ ⋯

Tactic:
exact add_left _ _ _ _ _ _ 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 z : N
hz : z ∈ t
a_1 : R
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
h : p x z hx ⋯
⊢ p (a_1 • x) z ⋯ ⋯

Tactic:
smul_left _ _ _ _ _ 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 z : N
hz : z ∈ t
a_1 : R
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
h : p x z hx ⋯
⊢ p (a_1 • x) z ⋯ ⋯

Tactic:
exact smul_left _ _ _ _ _ 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
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 ⋯ ⋯
mem₃ : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x) (h : p x z hx ⋯), p (a • x) z ⋯ ⋯
⊢ p a z ha ⋯

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

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
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
⊢ p a 0 ha ⋯

Tactic:
zero_right a ha
-- 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
⊢ p a 0 ha ⋯

Tactic:
exact zero_right a ha