awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x : M × M₂
⊢ (f.coprod g : (a : M × M₂) → M₃) x =
    HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) x.1 : M₃) ((g : (a : M₂) → M₃) x.2 : M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
h : ∀ (x : M), Eq.{y + 1} (α := M₃) ((f.coprod g ∘ₗ inl R M M₂ : (a : M) → M₃) x : M₃) ((f : (a : M) → M₃) x : M₃)
⊢ f.coprod g ∘ₗ inl R M M₂ = f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x : M
⊢ Eq.{y + 1} (α := M₃) ((f.coprod g ∘ₗ inl R M M₂ : (a : M) → M₃) x : M₃) ((f : (a : M) → M₃) x : M₃)

Tactic:
simp only [map_zero, add_zero, coprod_apply, inl_apply, comp_apply]

Premises used: LinearMap.coprod_apply, LinearMap.comp_apply, map_zero, LinearMap.inl_apply, add_zero
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
h : ∀ (x : M₂), Eq.{y + 1} (α := M₃) ((f.coprod g ∘ₗ inr R M M₂ : (a : M₂) → M₃) x : M₃) ((g : (a : M₂) → M₃) x : M₃)
⊢ f.coprod g ∘ₗ inr R M M₂ = g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x : M₂
⊢ Eq.{y + 1} (α := M₃) ((f.coprod g ∘ₗ inr R M M₂ : (a : M₂) → M₃) x : M₃) ((g : (a : M₂) → M₃) x : M₃)

Tactic:
simp only [map_zero, coprod_apply, inr_apply, zero_add, comp_apply]

Premises used: LinearMap.inr_apply, LinearMap.coprod_apply, LinearMap.comp_apply, map_zero, zero_add
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
h :
  ∀ (x : M × M₂),
    Eq.{v + 1} (α := M) ((coprod (inl R M M₂) (inr R M M₂) : (a : M × M₂) → M × M₂) x).1
      ((id : (a : M × M₂) → M × M₂) x).1
h₁ :
  ∀ (x : M × M₂),
    Eq.{w + 1} (α := M₂) ((coprod (inl R M M₂) (inr R M M₂) : (a : M × M₂) → M × M₂) x).2
      ((id : (a : M × M₂) → M × M₂) x).2
⊢ Eq (α := M × M₂ →ₗ[R] M × M₂) (coprod (inl R M M₂) (inr R M M₂)) id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
x : M × M₂
⊢ Eq.{v + 1} (α := M) ((coprod (inl R M M₂) (inr R M M₂) : (a : M × M₂) → M × M₂) x).1
    ((id : (a : M × M₂) → M × M₂) x).1

Tactic:
simp only [Prod.mk_add_mk, add_zero, id_apply, coprod_apply, inl_apply, inr_apply, zero_add]

Premises used: LinearMap.inr_apply, Prod.mk_add_mk, LinearMap.id_apply, LinearMap.coprod_apply, zero_add, LinearMap.inl_apply, add_zero
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
x : M × M₂
⊢ Eq.{w + 1} (α := M₂) ((coprod (inl R M M₂) (inr R M M₂) : (a : M × M₂) → M × M₂) x).2
    ((id : (a : M × M₂) → M × M₂) x).2

Tactic:
simp only [Prod.mk_add_mk, add_zero, id_apply, coprod_apply, inl_apply, inr_apply, zero_add]

Premises used: LinearMap.inr_apply, Prod.mk_add_mk, LinearMap.id_apply, LinearMap.coprod_apply, zero_add, LinearMap.inl_apply, add_zero
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
g : M₂ →ₗ[R] M₃
⊢ Eq (α := M × M₂ →ₗ[R] M₃) (coprod 0 g) (g ∘ₗ snd R M M₂)

Tactic:
zero_add _

Premises used: LinearMap.coprod, zero_add
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
⊢ Eq (α := M × M₂ →ₗ[R] M₃) (f.coprod 0) (f ∘ₗ fst R M M₂)

Tactic:
add_zero _

Premises used: LinearMap.coprod, add_zero
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M₃ →ₗ[R] M₄
g₁ : M →ₗ[R] M₃
g₂ : M₂ →ₗ[R] M₃
⊢ f ∘ₗ g₁.coprod g₂ = (f ∘ₗ g₁).coprod (f ∘ₗ g₂)

Tactic:
ext fun x => f.map_add (g₁ x.1) (g₂ x.2)

Premises used: LinearMap.map_add, LinearMap.ext, Prod.fst, Prod.snd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
h : ∀ (x : M × M₂), Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) ((coprod id 0 : (a : M × M₂) → M) x : M)
⊢ Eq (α := M × M₂ →ₗ[R] M) (fst R M M₂) (coprod id 0)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
x : M × M₂
⊢ Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) ((coprod id 0 : (a : M × M₂) → M) x : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
h :
  ∀ (x : M × M₂),
    Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) ((coprod 0 id : (a : M × M₂) → M₂) x : M₂)
⊢ Eq (α := M × M₂ →ₗ[R] M₂) (snd R M M₂) (coprod 0 id)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
x : M × M₂
⊢ Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) ((coprod 0 id : (a : M × M₂) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M₂ →ₗ[R] M₄
g : M₃ →ₗ[R] M₄
f' : M →ₗ[R] M₂
g' : M →ₗ[R] M₃
⊢ f.coprod g ∘ₗ f'.prod g' = f ∘ₗ f' + g ∘ₗ g'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
simp :
  (fun (a : M × M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a.1 : M₃) ((g : (a : M₂) → M₃) a.2 : M₃)) ''
      (↑(S.prod S') : Set (M × M₂)) =
    HAdd.hAdd (α := Set M₃) ((⇑f : (a : M) → M₃) '' (↑S : Set M)) ((⇑g : (a : M₂) → M₃) '' (↑S' : Set M₂))
⊢ (↑(Submodule.map (f.coprod g) (S.prod S')) : Set M₃) = (↑(Submodule.map f S ⊔ Submodule.map g S') : Set M₃)

Tactic:
simp only [LinearMap.coprod_apply, Submodule.coe_sup, Submodule.map_coe]

Premises used: Submodule.coe_sup, LinearMap.coprod_apply, Submodule.map_coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
rw :
  Eq.{y + 1} (α := Set M₃)
    ((fun (a : M × M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a.1 : M₃) ((g : (a : M₂) → M₃) a.2 : M₃)) ''
      (↑(S.prod S') : Set (M × M₂)))
    (Set.image2
      (fun (a : M) (b : M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a : M₃) ((g : (a : M₂) → M₃) b : M₃))
      (↑S : Set M) (↑S' : Set M₂))
⊢ (fun (a : M × M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a.1 : M₃) ((g : (a : M₂) → M₃) a.2 : M₃)) ''
      (↑(S.prod S') : Set (M × M₂)) =
    HAdd.hAdd (α := Set M₃) ((⇑f : (a : M) → M₃) '' (↑S : Set M)) ((⇑g : (a : M₂) → M₃) '' (↑S' : Set M₂))

Tactic:
rw [← Set.image2_add, Set.image2_image_left, Set.image2_image_right]

Premises used: Set.image2_image_right, Set.image2_image_left, Set.image2_add
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ Eq.{y + 1} (α := Set M₃)
    ((fun (a : M × M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a.1 : M₃) ((g : (a : M₂) → M₃) a.2 : M₃)) ''
      (↑(S.prod S') : Set (M × M₂)))
    (Set.image2
      (fun (a : M) (b : M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a : M₃) ((g : (a : M₂) → M₃) b : M₃))
      (↑S : Set M) (↑S' : Set M₂))

Tactic:
Set.image_prod fun m m₂ => f m + g m₂

Premises used: setOf, Set.image_prod, Set.prod, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ Eq.{y + 1} (α := Set M₃)
    ((fun (a : M × M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a.1 : M₃) ((g : (a : M₂) → M₃) a.2 : M₃)) ''
      (↑(S.prod S') : Set (M × M₂)))
    (Set.image2
      (fun (a : M) (b : M₂) ↦ HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M) → M₃) a : M₃) ((g : (a : M₂) → M₃) b : M₃))
      (↑S : Set M) (↑S' : Set M₂))

Tactic:
exact Set.image_prod fun m m₂ => f m + g m₂

Premises used: Set.image_prod, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f : M × M₂ →ₗ[R] M₃
rw : f ∘ₗ coprod (inl R M M₂) (inr R M M₂) = f
rw₁ : f ∘ₗ id = f
rw₂ rw₃ : f = f
⊢ (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f

Tactic:
rw [← comp_coprod, coprod_inl_inr, comp_id]

Premises used: LinearMap.coprod_inl_inr, LinearMap.comp_id, LinearMap.comp_coprod
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
a b : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
h :
  ∀ (x : M × M₂),
    Eq.{y + 1} (α := M₃) (((a + b).1.coprod (a + b).2 : (a : M × M₂) → M₃) x : M₃)
      ((a.1.coprod a.2 + b.1.coprod b.2 : (a : M × M₂) → M₃) x : M₃)
⊢ (a + b).1.coprod (a + b).2 = a.1.coprod a.2 + b.1.coprod b.2

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
a b : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
x : M × M₂
⊢ Eq.{y + 1} (α := M₃) (((a + b).1.coprod (a + b).2 : (a : M × M₂) → M₃) x : M₃)
    ((a.1.coprod a.2 + b.1.coprod b.2 : (a : M × M₂) → M₃) x : M₃)

Tactic:
simp only [Prod.snd_add, add_apply, coprod_apply, Prod.fst_add, add_add_add_comm]

Premises used: LinearMap.add_apply, LinearMap.coprod_apply, Prod.fst_add, add_add_add_comm, Prod.snd_add
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
r : S
a : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
dsimp : (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2
⊢ (r • a).1.coprod (r • a).2 = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) (a.1.coprod a.2)

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
r : S
a : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
h :
  ∀ (x : M × M₂),
    Eq.{y + 1} (α := M₃) (((r • a.1).coprod (r • a.2) : (a : M × M₂) → M₃) x : M₃)
      ((r • a.1.coprod a.2 : (a : M × M₂) → M₃) x : M₃)
⊢ (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
r : S
a : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
x : M × M₂
⊢ Eq.{y + 1} (α := M₃) (((r • a.1).coprod (r • a.2) : (a : M × M₂) → M₃) x : M₃)
    ((r • a.1.coprod a.2 : (a : M × M₂) → M₃) x : M₃)

Tactic:
simp only [smul_add, smul_apply, coprod_apply]

Premises used: LinearMap.smul_apply, LinearMap.coprod_apply, smul_add
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f_1 : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
⊢ (fun (f : M × M₂ →ₗ[R] M₃) ↦ (f ∘ₗ inl R M M₂, f ∘ₗ inr R M M₂))
      ((fun (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ↦ f.1.coprod f.2) f) =
    f

Tactic:
simp only [coprod_inl, coprod_inr]

Premises used: LinearMap.coprod_inr, LinearMap.coprod_inl
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M₅
inst_7 : AddCommMonoid M₆
inst_8 : Module R M
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M₅
inst_13 : Module R M₆
f_1 : M →ₗ[R] M₂
inst_14 : Module S M₃
inst_15 : SMulCommClass R S M₃
f : M × M₂ →ₗ[R] M₃
⊢ (fun (f : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)) ↦ f.1.coprod f.2)
      ((fun (f : M × M₂ →ₗ[R] M₃) ↦ (f ∘ₗ inl R M M₂, f ∘ₗ inr R M M₂)) f) =
    f

Tactic:
simp only [← comp_coprod, comp_id, coprod_inl_inr]

Premises used: LinearMap.coprod_inl_inr, LinearMap.comp_id, LinearMap.comp_coprod
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f g : M × M₂ →ₗ[R] M₃
⊢ f = g ↔ f ∘ₗ inl R M M₂ = g ∘ₗ inl R M M₂ ∧ f ∘ₗ inr R M M₂ = g ∘ₗ inr R M M₂

Tactic:
(coprodEquiv ℕ).symm.injective.eq_iff.symm.trans Prod.ext_iff

Premises used: LinearEquiv.symm, Function.Injective.eq_iff, Prod.ext_iff, Nat, Iff.trans, LinearMap.coprodEquiv, LinearEquiv.injective, Iff.symm
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R M₃
f g : M × M₂ →ₗ[R] M₃
hl : f ∘ₗ inl R M M₂ = g ∘ₗ inl R M M₂
hr : f ∘ₗ inr R M M₂ = g ∘ₗ inr R M M₂
⊢ f = g

Tactic:
prod_ext_iff.2 ⟨hl, hr⟩

Premises used: Iff.mpr, LinearMap.prod_ext_iff, And.intro
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
⊢ Eq (α := (a : M × M₂) → M₃ × M₄) (⇑(f.prodMap g) : (a : M × M₂) → M₃ × M₄)
    (Prod.map (⇑f : (a : M) → M₃) (⇑g : (a : M₂) → M₄))

Tactic:
rfl

Premises used: Prod.map, Function.prod, rfl
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
x : M × M₂
⊢ Eq (α := M₃ × M₄) ((f.prodMap g : (a : M × M₂) → M₃ × M₄) x : M₃ × M₄)
    (((f : (a : M) → M₃) x.1, (g : (a : M₂) → M₄) x.2) : M₃ × M₄)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
S : Submodule R M₂
S' : Submodule R M₄
⊢ Submodule.comap (f.prodMap g) (S.prod S') = (Submodule.comap f S).prod (Submodule.comap g S')

Tactic:
SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _

Premises used: SetLike.coe_injective, Set.preimage_prod_map_prod, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
S : Submodule R M
S' : Submodule R M₃
⊢ Submodule.map (f.prodMap g) (S.prod S') = (Submodule.map f S).prod (Submodule.map g S')

Tactic:
SetLike.coe_injective <| Set.prodMap_image_prod f g _ _

Premises used: Set.prodMap_image_prod, SetLike.coe_injective, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
rw : Submodule.comap (f.prodMap g) ⊥ = Submodule.comap (f.prodMap g) (Submodule.prod ⊥ ⊥)
rw₁ rw₂ : Submodule.comap (f.prodMap g) ⊥ = Submodule.comap (f.prodMap g) ⊥
⊢ Submodule.comap (f.prodMap g) ⊥ = (Submodule.comap f ⊥).prod (Submodule.comap g ⊥)

Tactic:
rw [← prodMap_comap_prod, Submodule.prod_bot]

Premises used: LinearMap.prodMap_comap_prod, Submodule.prod_bot
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
h : ∀ (fst : M₃) (snd : M₄), (fst, snd) ∈ (f.prodMap g).range ↔ (fst, snd) ∈ f.range.prod g.range
⊢ (f.prodMap g).range = f.range.prod g.range

Tactic:
ext ⟨_, _⟩
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
fst : M₃
snd : M₄
⊢ (fst, snd) ∈ (f.prodMap g).range ↔ (fst, snd) ∈ f.range.prod g.range

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
⊢ Eq (α := M × M₂ →ₗ[R] M × M₂) (prodMap id id) id

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl, LinearMap.prodMap
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
⊢ Eq (α := M × M₂ →ₗ[R] M × M₂) (prodMap 1 1) 1

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl, LinearMap.prodMap
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
M₅ : Type u_1
M₆ : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : AddCommMonoid M₅
inst_6 : AddCommMonoid M₆
inst_7 : Module R M
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M₄
inst_11 : Module R M₅
inst_12 : Module R M₆
f₁₂ : M →ₗ[R] M₂
f₂₃ : M₂ →ₗ[R] M₃
g₁₂ : M₄ →ₗ[R] M₅
g₂₃ : M₅ →ₗ[R] M₆
⊢ f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂)

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl, LinearMap.prodMap
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f₁₂ f₂₃ : M →ₗ[R] M
g₁₂ g₂₃ : M₂ →ₗ[R] M₂
⊢ f₂₃.prodMap g₂₃ * f₁₂.prodMap g₁₂ = (f₂₃ * f₁₂).prodMap (g₂₃ * g₁₂)

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl, LinearMap.prodMap