-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
mpr :
  ∀ (x : M) (hx : x ∈ S),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x ⋯) :
        N)
mpr₁ :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) 0 ⋯) :
      N)
mpr₂ :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x)
    (hy : Membership.mem (γ := Submodule R M) (span R S) y)
    (hx' :
      Eq.{u_8 + 1} (α := N)
        ((f : (a : ↥(span R S)) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
          N)
        ((g : (a : ↥(span R S)) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
          N))
    (hy' :
      Eq.{u_8 + 1} (α := N)
        ((f : (a : ↥(span R S)) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
          N)
        ((g : (a : ↥(span R S)) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
          N)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (x + y) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (x + y) ⋯) :
        N)
mpr₃ :
  ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R S) x)
    (hx' :
      Eq.{u_8 + 1} (α := N)
        ((f : (a : ↥(span R S)) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
          N)
        ((g : (a : ↥(span R S)) → N)
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
          N)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (a • x) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (a • x) ⋯) :
        N)
⊢ Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)

Tactic:
induction hx using span_induction with
    | mem x hx => exact h ⟨x, hx⟩
    | zero => erw [map_zero, map_zero]
    | add x y hx hy hx' hy' =>
        erw [f.map_add ⟨x, hx⟩ ⟨y, hy⟩, g.map_add ⟨x, hx⟩ ⟨y, hy⟩]
        rw [hx', hy']
    | smul a x hx hx' =>
        erw [f.map_smul a ⟨x, hx⟩, g.map_smul a ⟨x, hx⟩]
        rw [hx']

Premises used: map_zero, Submodule.smul, Submodule.zero, Submodule.add