awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
mp : map (inl R M M₂) p₁ ≤ q
mp₁ : map (inr R M M₂) p₂ ≤ q
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q

Tactic:
constructor
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M
hx : x ∈ (↑p₁ : Set M)
mp : Membership.mem (α := M × M₂) (p₁.prod p₂) ((inl R M M₂ : (a : M) → M × M₂) x : M × M₂)
⊢ Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x : M × M₂)

Tactic:
apply h
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M
hx : x ∈ (↑p₁ : Set M)
⊢ Membership.mem (α := M × M₂) (p₁.prod p₂) ((inl R M M₂ : (a : M) → M × M₂) x : M × M₂)

Tactic:
⟨hx, zero_mem p₂⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro, ZeroMemClass.zero_mem
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M
hx : x ∈ (↑p₁ : Set M)
⊢ Membership.mem (α := M × M₂) (p₁.prod p₂) ((inl R M M₂ : (a : M) → M × M₂) x : M × M₂)

Tactic:
exact ⟨hx, zero_mem p₂⟩
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M₂
hx : x ∈ (↑p₂ : Set M₂)
mp : Membership.mem (α := M × M₂) (p₁.prod p₂) ((inr R M M₂ : (a : M₂) → M × M₂) x : M × M₂)
⊢ Membership.mem (α := M × M₂) q ((inr R M M₂ : (a : M₂) → M × M₂) x : M × M₂)

Tactic:
apply h
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M₂
hx : x ∈ (↑p₂ : Set M₂)
⊢ Membership.mem (α := M × M₂) (p₁.prod p₂) ((inr R M M₂ : (a : M₂) → M × M₂) x : M × M₂)

Tactic:
⟨zero_mem p₁, hx⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro, ZeroMemClass.zero_mem
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : p₁.prod p₂ ≤ q
x : M₂
hx : x ∈ (↑p₂ : Set M₂)
⊢ Membership.mem (α := M × M₂) (p₁.prod p₂) ((inr R M M₂ : (a : M₂) → M × M₂) x : M × M₂)

Tactic:
exact ⟨zero_mem p₁, hx⟩
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
a :
  Membership.mem (α := M × M₂) (γ := Submodule R (M × M₂)) (map (inl R M M₂) p₁)
    ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
⊢ Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)

Tactic:
apply hH
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
⊢ Membership.mem (α := M × M₂) (γ := Submodule R (M × M₂)) (map (inl R M M₂) p₁)
    ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)

Tactic:
simpa using h1
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
⊢ Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)

Tactic:
have h1' : (LinearMap.inl R _ _) x1 ∈ q := by
      apply hH
      simpa using h1
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
h1' : Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
a :
  Membership.mem (α := M × M₂) (γ := Submodule R (M × M₂)) (map (inr R M M₂) p₂)
    ((inr R M M₂ : (a : M₂) → M × M₂) x2 : M × M₂)
⊢ Membership.mem (α := M × M₂) q ((inr R M M₂ : (a : M₂) → M × M₂) x2 : M × M₂)

Tactic:
apply hK
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
h1' : Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
⊢ Membership.mem (α := M × M₂) (γ := Submodule R (M × M₂)) (map (inr R M M₂) p₂)
    ((inr R M M₂ : (a : M₂) → M × M₂) x2 : M × M₂)

Tactic:
simpa using h2
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
h1' : Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
⊢ Membership.mem (α := M × M₂) q ((inr R M M₂ : (a : M₂) → M × M₂) x2 : M × M₂)

Tactic:
have h2' : (LinearMap.inr R _ _) x2 ∈ q := by
      apply hK
      simpa using h2
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ (↑p₁ : Set M)
h2 : (x1, x2).2 ∈ (↑p₂ : Set M₂)
h1' : Membership.mem (α := M × M₂) q ((inl R M M₂ : (a : M) → M × M₂) x1 : M × M₂)
h2' : Membership.mem (α := M × M₂) q ((inr R M M₂ : (a : M₂) → M × M₂) x2 : M × M₂)
⊢ (x1, x2) ∈ q

Tactic:
simpa using add_mem h1' h2'

Premises used: AddMemClass.add_mem
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
⊢ p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥

Tactic:
simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot, ker_inl, ker_inr]

Premises used: Submodule.prod_le_iff, Submodule.ker_inl, GaloisConnection.le_iff_le, Submodule.gc_map_comap, eq_bot_iff, Submodule.ker_inr, Submodule.comap_bot
-- 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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
⊢ p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤

Tactic:
simp only [eq_top_iff, le_prod_iff, map_top, range_fst, range_snd]

Premises used: Submodule.range_snd, eq_top_iff, Submodule.map_top, Submodule.le_prod_iff, Submodule.range_fst
-- 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₂
hl :
  ∀ (x : M),
    Eq.{w + 1} (α := M₂)
      (((LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inl R M M₂ : (a : M) → M₂) x :
        M₂)
      ((LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂ : (a : M) → M₂) x : M₂)
hr :
  ∀ (x : M₂),
    Eq (α := M₂)
      (((LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M₂)
          x :
        M₂)
      ((LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M₂) x : M₂)
⊢ Eq (α := M × M₂ →ₗ[R] M₂) (LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) (LinearMap.snd R M M₂)

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
⊢ Eq.{w + 1} (α := M₂)
    (((LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inl R M M₂ : (a : M) → M₂) x :
      M₂)
    ((LinearMap.snd R M M₂ ∘ₗ LinearMap.inl R M M₂ : (a : 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₂
x : M₂
⊢ Eq (α := M₂)
    (((LinearMap.fst R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M₂) x :
      M₂)
    ((LinearMap.snd R M M₂ ∘ₗ LinearMap.inr R M M₂ : (a : 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₂
hl :
  ∀ (x : M),
    Eq (α := M)
      (((LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inl R M M₂ : (a : M) → M) x :
        M)
      ((LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂ : (a : M) → M) x : M)
hr :
  ∀ (x : M₂),
    Eq.{v + 1} (α := M)
      (((LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M) x :
        M)
      ((LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M) x : M)
⊢ Eq (α := M × M₂ →ₗ[R] M) (LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) (LinearMap.fst R M M₂)

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
⊢ Eq (α := M)
    (((LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inl R M M₂ : (a : M) → M) x : M)
    ((LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂ : (a : 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₂
x : M₂
⊢ Eq.{v + 1} (α := M)
    (((LinearMap.snd R M₂ M ∘ₗ (↑(prodComm R M M₂) : M × M₂ →ₗ[R] M₂ × M)) ∘ₗ LinearMap.inr R M M₂ : (a : M₂) → M) x :
      M)
    ((LinearMap.fst R M M₂ ∘ₗ LinearMap.inr R M M₂ : (a : 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₂
⊢ Eq (α := (M₂ × M) ≃ₗ[R] M × M₂) (symm (prodComm R M M₂)) (prodComm R M₂ M)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.prodComm, Prod.swap, rfl
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq (α := M₁)
      ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₁)
          x :
        M₁)
      ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₁)
          x :
        M₁)
hl₁ :
  ∀ (x : M₂),
    Eq.{u_3 + 1} (α := M₁)
      ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₁)
          x :
        M₁)
      ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₁)
          x :
        M₁)
hr :
  ∀ (x : M₃),
    Eq.{u_3 + 1} (α := M₁)
      (((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inr R (M₁ × M₂) M₃ :
            (a : M₃) → M₁)
          x :
        M₁)
      (((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₁) x : M₁)
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₁)
    (LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₁
⊢ Eq (α := M₁)
    ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₁)
        x :
      M₁)
    ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₁)
        x :
      M₁)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₂
⊢ Eq.{u_3 + 1} (α := M₁)
    ((((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₁)
        x :
      M₁)
    ((((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₁)
        x :
      M₁)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₃
⊢ Eq.{u_3 + 1} (α := M₁)
    (((LinearMap.fst R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
            LinearMap.inr R (M₁ × M₂) M₃ :
          (a : M₃) → M₁)
        x :
      M₁)
    (((LinearMap.fst R M₁ M₂ ∘ₗ LinearMap.fst R (M₁ × M₂) M₃) ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₁) x : M₁)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
hl :
  ∀ (x : M₁),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).1
hl₁ :
  ∀ (x : M₁),
    Eq.{y + 1} (α := M₃)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inl R M₁ M₂ :
            (a : M₁) → M₂ × M₃)
          x).2
hl₂ :
  ∀ (x : M₂),
    Eq.{w + 1} (α := M₂)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).1
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).1
hl₃ :
  ∀ (x : M₂),
    Eq.{y + 1} (α := M₃)
      ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
                LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).2
      (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
              LinearMap.inr R M₁ M₂ :
            (a : M₂) → M₂ × M₃)
          x).2
hr :
  ∀ (x : M₃),
    Eq.{w + 1} (α := M₂)
      (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inr R (M₁ × M₂) M₃ :
            (a : M₃) → M₂ × M₃)
          x).1
      ((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₂ × M₃)
          x).1
hr₁ :
  ∀ (x : M₃),
    Eq.{y + 1} (α := M₃)
      (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inr R (M₁ × M₂) M₃ :
            (a : M₃) → M₂ × M₃)
          x).2
      ((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₂ × M₃)
          x).2
⊢ Eq (α := (M₁ × M₂) × M₃ →ₗ[R] M₂ × M₃)
    (LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃))
    (LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₁
⊢ Eq.{w + 1} (α := M₂)
    ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₂ × M₃)
        x).1
    (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₂ × M₃)
        x).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₁
⊢ Eq.{y + 1} (α := M₃)
    ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₂ × M₃)
        x).2
    (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inl R M₁ M₂ :
          (a : M₁) → M₂ × M₃)
        x).2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₂
⊢ Eq.{w + 1} (α := M₂)
    ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₂ × M₃)
        x).1
    (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₂ × M₃)
        x).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₂
⊢ Eq.{y + 1} (α := M₃)
    ((((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
              LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₂ × M₃)
        x).2
    (((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inl R (M₁ × M₂) M₃) ∘ₗ
            LinearMap.inr R M₁ M₂ :
          (a : M₂) → M₂ × M₃)
        x).2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₃
⊢ Eq.{w + 1} (α := M₂)
    (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
            LinearMap.inr R (M₁ × M₂) M₃ :
          (a : M₃) → M₂ × M₃)
        x).1
    ((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₂ × M₃) x).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
M₁ : Type u_3
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₃
x : M₃
⊢ Eq.{y + 1} (α := M₃)
    (((LinearMap.snd R M₁ (M₂ × M₃) ∘ₗ (↑(prodAssoc R M₁ M₂ M₃) : (M₁ × M₂) × M₃ →ₗ[R] M₁ × M₂ × M₃)) ∘ₗ
            LinearMap.inr R (M₁ × M₂) M₃ :
          (a : M₃) → M₂ × M₃)
        x).2
    ((LinearMap.prodMap (LinearMap.snd R M₁ M₂) LinearMap.id ∘ₗ LinearMap.inr R (M₁ × M₂) M₃ : (a : M₃) → M₂ × M₃) x).2

Tactic:
simp
-- 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
N : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
x x_1 : M × N
⊢ (-(x + x_1).2, (x + x_1).1) = (-x.2, x.1) + (-x_1.2, x_1.1)

Tactic:
simp [add_comm]

Premises used: add_comm
-- 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
N : Type u_3
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
x : R
x_1 : M × N
⊢ (-(x • x_1).2, (x • x_1).1) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (-x_1.2, x_1.1)

Tactic:
simp