Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: case a.mem
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ x ∈ s, ∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.zero
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ n ∈ span R t, (f 0) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.add
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ (x y : M),
    x ∈ span R s →
      y ∈ span R s →
        (∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
          (∀ n ∈ span R t, (f y) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
            ∀ n ∈ span R t, (f (x + y)) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

pp: case a.smul
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ (a : R),
    ∀ x ∈ span R s,
      (∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
        ∀ n ∈ span R t, (f (a • x)) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
on_goal 1 =>
      intro a ha
      apply @span_induction R N _ _ _ t
      · intro b hb
        exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩

Goal state after:
case a.mem.zero
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ (f a) 0 ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.mem.add
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (x y : N),
    x ∈ span R t →
      y ∈ span R t →
        (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) →
          (f a) y ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (x + y) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.mem.smul
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (a_1 : R),
    ∀ x ∈ span R t,
      (f a) x ∈ span R (image2 (fun m n ↦ (f m) n) s t) → (f a) (a_1 • x) ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.zero
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ n ∈ span R t, (f 0) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.add
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ (x y : M),
    x ∈ span R s →
      y ∈ span R s →
        (∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
          (∀ n ∈ span R t, (f y) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
            ∀ n ∈ span R t, (f (x + y)) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)

case a.smul
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ (a : R),
    ∀ x ∈ span R s,
      (∀ n ∈ span R t, (f x) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)) →
        ∀ n ∈ span R t, (f (a • x)) n ∈ span R (image2 (fun m n ↦ (f m) n) s t)