awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
a₁ :
  ∀ (x : N) (h : x ∈ t),
    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 : N →ₗ[R] P) : (a : N) → P) x : P)
a₂ :
  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 : N →ₗ[R] P) : (a : N) → P) 0 : 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 : N →ₗ[R] P) : (a : N) → P) n : P)
have a₃ : ∀ (x y : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x)
  (hy : Membership.mem (γ := Submodule R N) (span R t) y),
  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 : N →ₗ[R] P) : (a : N) → P) x : P) →
    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 : N →ₗ[R] P) : (a : N) → P) y : P) →
      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 : N →ₗ[R] P) : (a : N) → P) (x + y) : P)
Tactic: apply @span_induction R N _ _ _ t
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
a₁ :
  ∀ (x : N) (h : x ∈ t),
    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 : N →ₗ[R] P) : (a : N) → P) x : P)
a₂ :
  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 : N →ₗ[R] P) : (a : N) → P) 0 : P)
a₃ :
  ∀ (x y : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y),
    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 : N →ₗ[R] P) : (a : N) → P) x : P) →
      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 : N →ₗ[R] P) : (a : N) → P) y : P) →
        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 : N →ₗ[R] P) : (a : N) → P) (x + y) : 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 : N →ₗ[R] P) : (a : N) → P) n : P)
have a₄ : ∀ (a_1 : R) (x : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x),
  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 : N →ₗ[R] P) : (a : N) → P) x : P) →
    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 : N →ₗ[R] P) : (a : N) → P) (a_1 • x) : P)
Tactic: apply @span_induction R N _ _ _ t
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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 : 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)
have a : ∀ (a : M) (ha : a ∈ s),
  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 : N →ₗ[R] P) : (a : N) → P) 0 : P)
Tactic: on_goal 1 =>
      intro a ha
      apply @span_induction R N _ _ _ t
      · intro b hb
        exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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 :
  ∀ (a : M) (ha : a ∈ s),
    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 : N →ₗ[R] P) : (a : N) → P) 0 : P)
⊢ ∀ (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)
have a₁ : ∀ (a : M) (ha : a ∈ s) (x y : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x)
  (hy : Membership.mem (γ := Submodule R N) (span R t) y),
  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 : N →ₗ[R] P) : (a : N) → P) x : P) →
    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 : N →ₗ[R] P) : (a : N) → P) y : P) →
      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 : N →ₗ[R] P) : (a : N) → P) (x + y) : P)
Tactic: on_goal 1 =>
      intro a ha
      apply @span_induction R N _ _ _ t
      · intro b hb
        exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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 :
  ∀ (a : M) (ha : a ∈ s),
    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 : N →ₗ[R] P) : (a : N) → P) 0 : P)
a₁ :
  ∀ (a : M) (ha : a ∈ s) (x y : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x)
    (hy : Membership.mem (γ := Submodule R N) (span R t) y),
    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 : N →ₗ[R] P) : (a : N) → P) x : P) →
      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 : N →ₗ[R] P) : (a : N) → P) y : P) →
        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 : N →ₗ[R] P) : (a : N) → P) (x + y) : P)
⊢ ∀ (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)
have a₂ : ∀ (a : M) (ha : a ∈ s) (a_1 : R) (x : N) (hx : Membership.mem (γ := Submodule R N) (span R t) x),
  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 : N →ₗ[R] P) : (a : N) → P) x : P) →
    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 : N →ₗ[R] P) : (a : N) → P) (a_1 • x) : P)
Tactic: on_goal 1 =>
      intro a ha
      apply @span_induction R N _ _ _ t
      · intro b hb
        exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ 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)
have 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)
Tactic: rw [span_le, image2_subset_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (hypothesis)
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
⊢ 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)
have hn₁ : n = 0
Tactic: rw [Submodule.mem_bot] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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.{u_4, u_4} (α := P) (γ := Submodule R P) ⊥
    ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)
have rw : Membership.mem (γ := Submodule R P) ⊥ 0
Tactic: rw [hn, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ 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)
have 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)
Tactic: rw [Submodule.mem_bot] at hm ⊢
Cleared hypotheses: hm, n, h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ Eq.{u_4 + 1} (α := P) ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P) (0 : P)
have rw : Eq.{u_4 + 1} (α := P) (((f : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) n : P) (0 : P)
Tactic: rw [hm, LinearMap.map_zero₂]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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)
⊢ Eq.{u_4 + 1} (α := P) ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P) (0 : P)
have rw₁ : Eq.{u_4 + 1} (α := P) 0 0
Tactic: rw [hm, LinearMap.map_zero₂]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ 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))
have rw : map₂ f p q = map₂ f (span R (↑p : Set M)) (span R (↑q : Set N))
Tactic: rw [← map₂_span_span, span_eq, span_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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))
⊢ 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))
have rw₁ : map₂ f p q = map₂ f p (span R (↑q : Set N))
Tactic: rw [← map₂_span_span, span_eq, span_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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))
⊢ 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))
have rw₂ : map₂ f p q = map₂ f p q
Tactic: rw [← map₂_span_span, span_eq, span_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ map₂ f.flip q p = map₂ f p q
have 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)))
Tactic: rw [map₂_eq_span_image2, map₂_eq_span_image2, Set.image2_swap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), map₂ f (s i) t
have 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))
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
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ 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))
have 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))
Tactic: simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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))
⊢ 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))
have 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))
Tactic: simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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))
⊢ 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))
have 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)))
Tactic: simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ map₂ f s (⨆ (i : ι), t i) = ⨆ (i : ι), map₂ f s (t i)
have 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))
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
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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
⊢ 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))
have 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))
Tactic: simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
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))
⊢ 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))
have 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))
Tactic: simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_right]