-- Module: Mathlib.LinearAlgebra.Span.Basic
Goal:
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
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
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)
x : M
y : N
hx : Membership.mem (γ := Submodule R M) (span R s) x
hy : Membership.mem (γ := Submodule R N) (span R t) y
mem_mem :
  ∀ (u : M) (v : N) (hu : u ∈ s) (hv : v ∈ t),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)
zero_left :
  ∀ (v : N) (hv : Membership.mem (γ := Submodule R N) (span R t) v),
    Membership.mem (α := P) P' (((B : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) v : P)
zero_right :
  ∀ (u : M) (hu : Membership.mem (γ := Submodule R M) (span R s) u),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) 0 : P)
add_left :
  ∀ (u₁ u₂ : M) (v : N) (hu₁ : Membership.mem (γ := Submodule R M) (span R s) u₁)
    (hu₂ : Membership.mem (γ := Submodule R M) (span R s) u₂) (hv : Membership.mem (γ := Submodule R N) (span R t) v)
    (huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₁ : N →ₗ[R] P) : (a : N) → P) v : P))
    (huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u₂ : N →ₗ[R] P) : (a : N) → P) v : P)),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) (u₁ + u₂) : N →ₗ[R] P) : (a : N) → P) v : P)
add_right :
  ∀ (u : M) (v₁ v₂ : N) (hu : Membership.mem (γ := Submodule R M) (span R s) u)
    (hv₁ : Membership.mem (γ := Submodule R N) (span R t) v₁) (hv₂ : Membership.mem (γ := Submodule R N) (span R t) v₂)
    (huv₁ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v₁ : P))
    (huv₂ : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v₂ : P)),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) (v₁ + v₂) : P)
smul_left :
  ∀ (t_1 : R) (u : M) (v : N) (hu : Membership.mem (γ := Submodule R M) (span R s) u)
    (hv : Membership.mem (γ := Submodule R N) (span R t) v)
    (huv : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) (t_1 • u) : N →ₗ[R] P) : (a : N) → P) v : P)
smul_right :
  ∀ (t_1 : R) (u : M) (v : N) (hu : Membership.mem (γ := Submodule R M) (span R s) u)
    (hv : Membership.mem (γ := Submodule R N) (span R t) v)
    (huv : Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) v : P)),
    Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) u : N →ₗ[R] P) : (a : N) → P) (t_1 • v) : P)
⊢ Membership.mem (α := P) P' ((((B : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : P)

Tactic:
induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv

Premises used: Submodule.span_induction₂