-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a :
  ∀ (x : M) (h : x ∈ s) (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) n : P)
a₁ :
  ∀ (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        (((f : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) n : P)
a₂ :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y),
    (∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) n : P)) →
      (∀ (n : N),
          Membership.mem (γ := Submodule R N) (span R t) n →
            Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
              (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
              ((((f : (a : M) → N →ₗ[R] P) y : N →ₗ[R] P) : (a : N) → P) n : P)) →
        ∀ (n : N),
          Membership.mem (γ := Submodule R N) (span R t) n →
            Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
              (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
              ((((f : (a : M) → N →ₗ[R] P) (x + y) : N →ₗ[R] P) : (a : N) → P) n : P)
a₃ :
  ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x),
    (∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) n : P)) →
      ∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) (a • x) : N →ₗ[R] P) : (a : N) → P) n : P)
⊢ ∀ (m : M),
    Membership.mem (γ := Submodule R M) (span R s) m →
      ∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
apply @span_induction R M _ _ _ s

Premises used: Submodule.span_induction