awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x y : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
hy : Membership.mem (γ := Submodule R M) (span R s) y
h :
  ∀ (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)
h_1 :
  ∀ (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
h_2 : 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)

Tactic:
simp only [*, add_mem, smul_mem, zero_mem, map_zero, map_add,
        LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply, map_smul]

Premises used: LinearMap.zero_apply, LinearMap.smul_apply, LinearMap.add_apply, map_zero, map_add, AddMemClass.add_mem, ZeroMemClass.zero_mem, Submodule.smul_mem, map_smul
-- 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 : R
x : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
h :
  ∀ (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
h_1 : 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)

Tactic:
simp only [*, add_mem, smul_mem, zero_mem, map_zero, map_add,
        LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply, map_smul]

Premises used: LinearMap.zero_apply, LinearMap.smul_apply, LinearMap.add_apply, map_zero, map_add, AddMemClass.add_mem, ZeroMemClass.zero_mem, Submodule.smul_mem, map_smul
-- 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 ∈ s,
    ∀ y ∈ t,
      Membership.mem (α := P) (↑(map₂ f (span R s) (span R t)) : Set P)
        ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) y : 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) ≤
    map₂ f (span R s) (span R t)

Tactic:
rw [span_le, image2_subset_iff]

Premises used: Set.image2_subset_iff, Submodule.span_le
-- 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 : M
ha : a ∈ s
b : N
hb : b ∈ t
⊢ Membership.mem (α := P) (↑(map₂ f (span R s) (span R t)) : Set P)
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) b : P)

Tactic:
apply_mem_map₂ _ (subset_span ha) (subset_span hb)

Premises used: Submodule.apply_mem_map₂, Submodule.subset_span
-- 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 : M
ha : a ∈ s
b : N
hb : b ∈ t
⊢ Membership.mem (α := P) (↑(map₂ f (span R s) (span R t)) : Set P)
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) b : P)

Tactic:
exact apply_mem_map₂ _ (subset_span ha) (subset_span hb)

Premises used: Submodule.apply_mem_map₂, Submodule.subset_span
-- 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
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : Membership.mem (γ := Submodule R N) ⊥ n
⊢ n = 0

Tactic:
rw [Submodule.mem_bot] at hn

Premises used: Submodule.mem_bot
-- 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
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
rw : Membership.mem (γ := Submodule R P) ⊥ 0
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P) ⊥
    ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
rw [hn, map_zero]

Premises used: map_zero
-- 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
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ Membership.mem (γ := Submodule R P) ⊥ 0

Tactic:
simp only [mem_bot]

Premises used: Submodule.mem_bot
-- 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
q : Submodule R N
m : M
hm : Membership.mem (γ := Submodule R M) ⊥ m
n : N
h : n ∈ q
rw :
  ∀ (hm : m = 0),
    ∀ n ∈ q, Eq.{u_4 + 1} (α := P) ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P) (0 : P)
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P) ⊥
    ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)

Tactic:
rw [Submodule.mem_bot] at hm ⊢

Premises used: Submodule.mem_bot
-- 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
q : Submodule R N
m : M
hm : m = 0
n : N
h : n ∈ q
rw : Eq.{u_4 + 1} (α := P) (((f : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) n : P) (0 : P)
rw₁ rw₂ : Eq.{u_4 + 1} (α := P) 0 0
⊢ Eq.{u_4 + 1} (α := P) ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P) (0 : P)

Tactic:
rw [hm, LinearMap.map_zero₂]

Premises used: LinearMap.map_zero₂
-- 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
p₁ p₂ : Submodule R M
q₁ q₂ : Submodule R N
hp : p₁ ≤ p₂
hq : q₁ ≤ q₂
⊢ map₂ f p₁ q₁ ≤ map₂ f p₂ q₂

Tactic:
map₂_le.2 fun _m hm _n hn => apply_mem_map₂ _ (hp hm) (hq hn)

Premises used: Iff.mpr, Submodule.apply_mem_map₂, Submodule.map₂_le
-- 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
p₁ p₂ : Submodule R M
q : Submodule R N
h : p₁ ≤ p₂
⊢ map₂ f p₁ q ≤ map₂ f p₂ q

Tactic:
map₂_le_map₂ h (le_refl q)

Premises used: le_refl, Submodule.map₂_le_map₂
-- 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
p : Submodule R M
q₁ q₂ : Submodule R N
h : q₁ ≤ q₂
⊢ map₂ f p q₁ ≤ map₂ f p q₂

Tactic:
map₂_le_map₂ (le_refl p) h

Premises used: le_refl, Submodule.map₂_le_map₂
-- 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
p : Submodule R M
q₁ q₂ : Submodule R N
⊢ map₂ f p (q₁ ⊔ q₂) = map₂ f p q₁ ⊔ map₂ f p q₂

Tactic:
le_antisymm
    (map₂_le.2 fun _m hm _np hnp =>
      let ⟨_n, hn, _p, hp, hnp⟩ := mem_sup.1 hnp
      mem_sup.2 ⟨_, apply_mem_map₂ _ hm hn, _, apply_mem_map₂ _ hm hp, hnp ▸ (map_add _ _ _).symm⟩)
    (sup_le (map₂_le_map₂_right le_sup_left) (map₂_le_map₂_right le_sup_right))

Premises used: Iff.mpr, le_sup_left, _private.0.Submodule.map₂_sup_right.match_1, Membership.mem, Eq.rec, map_add, le_sup_right, Submodule.apply_mem_map₂, le_antisymm, Submodule.map₂_le, Max.max, And.intro, Exists.intro, Iff.mp, Submodule.map₂, sup_le, Submodule.mem_sup, Eq.symm, DFunLike.coe, Submodule.map₂_le_map₂_right
-- 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
p₁ p₂ : Submodule R M
q : Submodule R N
⊢ map₂ f (p₁ ⊔ p₂) q = map₂ f p₁ q ⊔ map₂ f p₂ q

Tactic:
le_antisymm
    (map₂_le.2 fun _mn hmn _p hp =>
      let ⟨_m, hm, _n, hn, hmn⟩ := mem_sup.1 hmn
      mem_sup.2
        ⟨_, apply_mem_map₂ _ hm hp, _, apply_mem_map₂ _ hn hp,
          hmn ▸ (LinearMap.map_add₂ _ _ _ _).symm⟩)
    (sup_le (map₂_le_map₂_left le_sup_left) (map₂_le_map₂_left le_sup_right))

Premises used: Iff.mpr, le_sup_left, _private.0.Submodule.map₂_sup_right.match_1, Membership.mem, Eq.rec, le_sup_right, Submodule.apply_mem_map₂, le_antisymm, Submodule.map₂_le, Max.max, And.intro, LinearMap.map_add₂, Exists.intro, Iff.mp, Submodule.map₂, sup_le, Submodule.mem_sup, Eq.symm, Submodule.map₂_le_map₂_left, DFunLike.coe
-- 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
p : Submodule R M
q : Submodule R N
i : M
hi : i ∈ (↑p : Set M)
j : N
hj : j ∈ (↑q : Set N)
⊢ (fun (m : M) (n : N) ↦ ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)) i j ∈
    (↑(map₂ f p q) : Set P)

Tactic:
apply_mem_map₂ _ hi hj

Premises used: Set.Mem, Submodule.apply_mem_map₂
-- 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
p : Submodule R M
q : Submodule R N
i : M
hi : i ∈ (↑p : Set M)
j : N
hj : j ∈ (↑q : Set N)
⊢ (fun (m : M) (n : N) ↦ ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)) i j ∈
    (↑(map₂ f p q) : Set P)

Tactic:
exact apply_mem_map₂ _ hi hj

Premises used: Submodule.apply_mem_map₂
-- 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
p : Submodule R M
q : Submodule R N
rw : map₂ f p q = map₂ f (span R (↑p : Set M)) (span R (↑q : Set N))
rw₁ : map₂ f p q = map₂ f p (span R (↑q : Set N))
rw₂ rw₃ : map₂ f p q = map₂ f p q
⊢ map₂ f p q =
    span R
      (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑p : Set M)
        (↑q : Set N))

Tactic:
rw [← map₂_span_span, span_eq, span_eq]

Premises used: Submodule.span_eq, Submodule.map₂_span_span
-- 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
p : Submodule R M
q : Submodule R N
rw :
  Eq.{u_4 + 1} (α := Submodule R P)
    (span R
      (image2 (fun (a : M) (b : N) ↦ (((f.flip : (a : N) → M →ₗ[R] P) b : M →ₗ[R] P) : (a : M) → P) a) (↑p : Set M)
        (↑q : Set N)))
    (span R
      (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑p : Set M)
        (↑q : Set N)))
⊢ map₂ f.flip q p = map₂ f p q

Tactic:
rw [map₂_eq_span_image2, map₂_eq_span_image2, Set.image2_swap]

Premises used: Submodule.map₂_eq_span_image2, Set.image2_swap
-- 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
p : Submodule R M
q : Submodule R N
⊢ Eq.{u_4 + 1} (α := Submodule R P)
    (span R
      (image2 (fun (a : M) (b : N) ↦ (((f.flip : (a : N) → M →ₗ[R] P) b : M →ₗ[R] P) : (a : M) → P) a) (↑p : Set M)
        (↑q : Set N)))
    (span R
      (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑p : Set M)
        (↑q : Set N)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
ι : Sort uι
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 : ι → Submodule R M
t : Submodule R N
this :
  map₂ f (⨆ (i : ι), span R (↑(s i) : Set M)) (span R (↑t : Set N)) =
    ⨆ (i : ι), map₂ f (span R (↑(s i) : Set M)) (span R (↑t : Set N))
⊢ map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), map₂ f (s i) t

Tactic:
simpa only [span_eq] using this

Premises used: Submodule.span_eq
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
ι : Sort uι
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 : ι → Submodule R M
t : Submodule R N
suffices :
  map₂ f (⨆ (i : ι), span R (↑(s i) : Set M)) (span R (↑t : Set N)) =
    ⨆ (i : ι), map₂ f (span R (↑(s i) : Set M)) (span R (↑t : Set N))
⊢ map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), map₂ f (s i) t

Tactic:
suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
    simpa only [span_eq] using this
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
ι : Sort uι
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 : ι → Submodule R M
t : Submodule R N
simp_rw :
  map₂ f (⨆ (i : ι), span R (↑(s i) : Set M)) (span R (↑t : Set N)) =
    ⨆ (i : ι),
      span R
        (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑(s i) : Set M)
          (↑t : Set N))
simp_rw₁ :
  map₂ f (span R (⋃ (i : ι), (↑(s i) : Set M))) (span R (↑t : Set N)) =
    span R
      (⋃ (i : ι),
        image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑(s i) : Set M)
          (↑t : Set N))
simp_rw₂ :
  Eq.{u_4 + 1} (α := 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)
        (⋃ (i : ι), (↑(s i) : Set M)) (↑t : Set N)))
    (span R
      (⋃ (i : ι),
        image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑(s i) : Set M)
          (↑t : Set N)))
⊢ map₂ f (⨆ (i : ι), span R (↑(s i) : Set M)) (span R (↑t : Set N)) =
    ⨆ (i : ι), map₂ f (span R (↑(s i) : Set M)) (span R (↑t : Set N))

Tactic:
simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]

Premises used: Submodule.span_iUnion, Submodule.map₂_span_span, Set.image2_iUnion_left
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
ι : Sort uι
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 : Submodule R M
t : ι → Submodule R N
this :
  map₂ f (span R (↑s : Set M)) (⨆ (i : ι), span R (↑(t i) : Set N)) =
    ⨆ (i : ι), map₂ f (span R (↑s : Set M)) (span R (↑(t i) : Set N))
⊢ map₂ f s (⨆ (i : ι), t i) = ⨆ (i : ι), map₂ f s (t i)

Tactic:
simpa only [span_eq] using this

Premises used: Submodule.span_eq
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
ι : Sort uι
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 : Submodule R M
t : ι → Submodule R N
suffices :
  map₂ f (span R (↑s : Set M)) (⨆ (i : ι), span R (↑(t i) : Set N)) =
    ⨆ (i : ι), map₂ f (span R (↑s : Set M)) (span R (↑(t i) : Set N))
⊢ map₂ f s (⨆ (i : ι), t i) = ⨆ (i : ι), map₂ f s (t i)

Tactic:
suffices map₂ f (span R s) (⨆ i, span R (t i : Set N)) = ⨆ i, map₂ f (span R s) (span R (t i)) by
    simpa only [span_eq] using this
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
ι : Sort uι
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 : Submodule R M
t : ι → Submodule R N
simp_rw :
  map₂ f (span R (↑s : Set M)) (⨆ (i : ι), span R (↑(t i) : Set N)) =
    ⨆ (i : ι),
      span R
        (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑s : Set M)
          (↑(t i) : Set N))
simp_rw₁ :
  map₂ f (span R (↑s : Set M)) (span R (⋃ (i : ι), (↑(t i) : Set N))) =
    span R
      (⋃ (i : ι),
        image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑s : Set M)
          (↑(t i) : Set N))
simp_rw₂ :
  Eq.{u_4 + 1} (α := 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 : Set M)
        (⋃ (i : ι), (↑(t i) : Set N))))
    (span R
      (⋃ (i : ι),
        image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) (↑s : Set M)
          (↑(t i) : Set N)))
⊢ map₂ f (span R (↑s : Set M)) (⨆ (i : ι), span R (↑(t i) : Set N)) =
    ⨆ (i : ι), map₂ f (span R (↑s : Set M)) (span R (↑(t i) : Set N))

Tactic:
simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_right]

Premises used: Set.image2_iUnion_right, Submodule.span_iUnion, Submodule.map₂_span_span
-- 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
m : M
h : ∀ (s : Submodule R N), map₂ f (R ∙ m) s = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) s
⊢ map₂ f (R ∙ m) = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m)

Tactic:
funext s
-- 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
m : M
s : Submodule R N
h : map₂ f (R ∙ m) (span R (↑s : Set N)) = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N))
h₁ :
  Eq.{u_4 + 1} (α := 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) {m} (↑s : Set N)))
    (map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N)))
h₂ :
  Eq.{u_4 + 1} (α := Submodule R P)
    (span R ((fun (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) '' (↑s : Set N)))
    (map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) (span R (↑s : Set N)))
h₃ h₄ :
  Eq.{u_4 + 1} (α := Submodule R P)
    (span R ((fun (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) '' (↑s : Set N)))
    (span R ((⇑((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) '' (↑s : Set N)))
⊢ map₂ f (R ∙ m) s = map (σ₁₂ := RingHom.id R) ((f : (a : M) → N →ₗ[R] P) m) s

Tactic:
rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]

Premises used: Set.image2_singleton_left, Submodule.span_eq, Submodule.map₂_span_span, Submodule.map_span
-- 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 : Submodule R M
n : N
rw : map₂ f s (R ∙ n) = map₂ f.flip (R ∙ n) s
rw₁ rw₂ : map₂ f s (R ∙ n) = map₂ f s (R ∙ n)
⊢ map₂ f s (R ∙ n) = map (σ₁₂ := RingHom.id R) ((f.flip : (a : N) → M →ₗ[R] P) n) s

Tactic:
rw [← map₂_span_singleton_eq_map, map₂_flip]

Premises used: Submodule.map₂_span_singleton_eq_map, Submodule.map₂_flip
-- 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
P₂ : Type u_7
inst_7 : AddCommMonoid P₂
inst_8 : Module R P₂
f : P →ₗ[R] P₂
g : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map f (map₂ g p q) = map₂ (g.compr₂ f) p q

Tactic:
map_iSup _ _ |>.trans <| iSup_congr fun _ => map_comp _ _ _ |>.symm

Premises used: Submodule.map_iSup, Submodule.map_comp, Submodule.map₂, iSup_congr, Eq.symm, Subtype.val, DFunLike.coe, Eq.trans
-- 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
N₂ : Type u_6
inst_7 : AddCommMonoid N₂
inst_8 : Module R N₂
f : M →ₗ[R] N₂ →ₗ[R] P
g : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
⊢ map₂ f p (map g q) = map₂ (f.compl₂ g) p q

Tactic:
iSup_congr fun _ => map_comp _ _ _ |>.symm

Premises used: Submodule.map_comp, Submodule.map₂, iSup_congr, Eq.symm, Subtype.val, DFunLike.coe