awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
x : (i : ι ⊕ ι₂) → N i
H :
  ∀ (val : ι),
    Eq (α := N (Sum.inl val))
      (Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂))
        (Sum.inl val))
      (x (Sum.inl val))
H₁ :
  ∀ (val : ι₂),
    Eq (α := N (Sum.inr val))
      (Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂))
        (Sum.inr val))
      (x (Sum.inr val))
⊢ (fun (t : ι ⊕ ι₂) ↦
      Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂)) t) =
    x

Tactic:
ext (_ | _)
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
x : (i : ι ⊕ ι₂) → N i
val : ι
⊢ Eq (α := N (Sum.inl val))
    (Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂))
      (Sum.inl val))
    (x (Sum.inl val))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
x : (i : ι ⊕ ι₂) → N i
val : ι₂
⊢ Eq (α := N (Sum.inr val))
    (Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) (fun (i₁ : ι) ↦ x (Sum.inl i₁)) (fun (i₂ : ι₂) ↦ x (Sum.inr i₂))
      (Sum.inr val))
    (x (Sum.inr val))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
N : ι ⊕ ι₂ → Type u_12
inst_10 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_11 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
⊢ Eq (α :=
    (⨂[R] (i₁ : ι), N (Sum.inl i₁)) →ₗ[R]
      (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)) →ₗ[R] (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
    (LinearMap.compr₂ₛₗ (TensorProduct.mk R (⨂[R] (i₁ : ι), N (Sum.inl i₁)) (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
      ((lift (s := N) :
            (a : MultilinearMap R N ((⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))) →
              (⨂[R] (i : ι ⊕ ι₂), N i) →ₗ[R] (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
          (domCoprodDep (N := N) (tprod R (s := fun (i₁ : ι) ↦ N (Sum.inl i₁)))
            (tprod R (s := fun (i₂ : ι₂) ↦ N (Sum.inr i₂)))) ∘ₗ
        TensorProduct.lift
          {
            toFun := fun (a : ⨂[R] (i₁ : ι), N (Sum.inl i₁)) ↦
              (lift (s := fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) :
                  (a : MultilinearMap R (fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) (⨂[R] (i : ι ⊕ ι₂), N i)) →
                    (⨂[R] (i : ι₂), N (Sum.inr i)) →ₗ[R] ⨂[R] (i : ι ⊕ ι₂), N i)
                ((((lift (s := fun (i : ι) ↦ N (Sum.inl i)) :
                          (a :
                              MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i))
                                (MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))) →
                            (⨂[R] (i : ι), N (Sum.inl i)) →ₗ[R]
                              MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))
                        ((currySumEquiv (N := N) :
                            (a : MultilinearMap R N (⨂[R] (i : ι ⊕ ι₂), N i)) →
                              MultilinearMap R (fun (i : ι) ↦ N (Sum.inl i))
                                (MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i)))
                          (tprod R (s := N))) :
                      (⨂[R] (i : ι), N (Sum.inl i)) →ₗ[R]
                        MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i)) :
                    (a : ⨂[R] (i : ι), N (Sum.inl i)) →
                      MultilinearMap R (fun (i : ι₂) ↦ N (Sum.inr i)) (⨂[R] (i : ι ⊕ ι₂), N i))
                  a),
            map_add' := ⋯, map_smul' := ⋯ :
            (⨂[R] (i₁ : ι), N (Sum.inl i₁)) →ₗ[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)) →ₗ[R] ⨂[R] (i : ι ⊕ ι₂), N i }))
    (LinearMap.compr₂ₛₗ (TensorProduct.mk R (⨂[R] (i₁ : ι), N (Sum.inl i₁)) (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
      LinearMap.id)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
N : ι ⊕ ι₂ → Type u_12
inst_1 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_2 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
a : (i₁ : ι) → N (Sum.inl i₁)
b : (i₂ : ι₂) → N (Sum.inr i₂)
⊢ Eq (α := ⨂[R] (i : ι ⊕ ι₂), N i)
    ((tmulEquivDep R N :
          (a : (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂))) → ⨂[R] (i : ι ⊕ ι₂), N i)
        (((tprod R (s := fun (i₁ : ι) ↦ N (Sum.inl i₁)) : (a : (i : ι) → N (Sum.inl i)) → ⨂[R] (i : ι), N (Sum.inl i))
            fun (i₁ : ι) ↦ a i₁) ⊗ₜ[R]
          (tprod R (s := fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) :
              (a : (i : ι₂) → N (Sum.inr i)) → ⨂[R] (i : ι₂), N (Sum.inr i))
            fun (i₂ : ι₂) ↦ b i₂) :
      ⨂[R] (i : ι ⊕ ι₂), N i)
    (⨂ₜ[R] (i : ι ⊕ ι₂), Sum.rec (motive := fun (x : ι ⊕ ι₂) ↦ N x) a b i : ⨂[R] (i : ι ⊕ ι₂), N i)

Tactic:
simp [tmulEquivDep]

Premises used: PiTensorProduct.tmulEquivDep
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
N : ι ⊕ ι₂ → Type u_12
inst_1 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst_2 : (i : ι ⊕ ι₂) → Module.{u_4, u_12} R (N i)
f : (i : ι ⊕ ι₂) → N i
⊢ Eq (α := (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
    ((LinearEquiv.symm (tmulEquivDep R N) :
        (a : ⨂[R] (i : ι ⊕ ι₂), N i) → (⨂[R] (i₁ : ι), N (Sum.inl i₁)) ⊗[R] (⨂[R] (i₂ : ι₂), N (Sum.inr i₂)))
      (⨂ₜ[R] (i : ι ⊕ ι₂), f i))
    (((tprod R (s := fun (i₁ : ι) ↦ N (Sum.inl i₁)) : (a : (i : ι) → N (Sum.inl i)) → ⨂[R] (i : ι), N (Sum.inl i))
        fun (i₁ : ι) ↦ f (Sum.inl i₁)) ⊗ₜ[R]
      (tprod R (s := fun (i₂ : ι₂) ↦ N (Sum.inr i₂)) : (a : (i : ι₂) → N (Sum.inr i)) → ⨂[R] (i : ι₂), N (Sum.inr i))
        fun (i₂ : ι₂) ↦ f (Sum.inr i₂))

Tactic:
simp [tmulEquivDep]

Premises used: PiTensorProduct.tmulEquivDep
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
M : Type u_8
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : ι → M
b : ι₂ → M
⊢ Eq (α := ⨂[R] (x : ι ⊕ ι₂), M)
    ((tmulEquiv R M : (a : (⨂[R] (x : ι), M) ⊗[R] (⨂[R] (x : ι₂), M)) → ⨂[R] (x : ι ⊕ ι₂), M)
        (((tprod R (s := fun (x : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ a i) ⊗ₜ[R]
          (tprod R (s := fun (x : ι₂) ↦ M) : (a : (i : ι₂) → M) → ⨂[R] (i : ι₂), M) fun (i : ι₂) ↦ b i) :
      ⨂[R] (x : ι ⊕ ι₂), M)
    ((tprod R (s := fun (i : ι ⊕ ι₂) ↦ M) : (a : (i : ι ⊕ ι₂) → M) → ⨂[R] (i : ι ⊕ ι₂), M) fun (i : ι ⊕ ι₂) ↦
        Sum.elim a b i :
      ⨂[R] (i : ι ⊕ ι₂), M)

Tactic:
simp [tmulEquiv, Sum.elim]

Premises used: PiTensorProduct.tmulEquiv, Sum.elim
-- Module: Mathlib.LinearAlgebra.PiTensorProduct
Goal:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst : CommSemiring R
M : Type u_8
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : ι ⊕ ι₂ → M
⊢ Eq (α := (⨂[R] (x : ι), M) ⊗[R] (⨂[R] (x : ι₂), M))
    ((LinearEquiv.symm (tmulEquiv R M) : (a : ⨂[R] (x : ι ⊕ ι₂), M) → (⨂[R] (x : ι), M) ⊗[R] (⨂[R] (x : ι₂), M))
      ((tprod R (s := fun (x : ι ⊕ ι₂) ↦ M) : (a : (i : ι ⊕ ι₂) → M) → ⨂[R] (i : ι ⊕ ι₂), M) fun (i : ι ⊕ ι₂) ↦ a i))
    (((tprod R (s := fun (i : ι) ↦ M) : (a : (i : ι) → M) → ⨂[R] (i : ι), M) fun (i : ι) ↦ a (Sum.inl i)) ⊗ₜ[R]
      (tprod R (s := fun (i : ι₂) ↦ M) : (a : (i : ι₂) → M) → ⨂[R] (i : ι₂), M) fun (i : ι₂) ↦ a (Sum.inr i))

Tactic:
simp [tmulEquiv]

Premises used: PiTensorProduct.tmulEquiv
-- 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₂
⊢ (fst R M M₂ : (a : M × M₂) → M) x = x.1

Tactic:
rfl

Premises used: rfl
-- 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₂
⊢ (snd R M M₂ : (a : M × M₂) → M₂) x = x.2

Tactic:
rfl

Premises used: rfl
-- 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 (α := (a : M × M₂) → M) (⇑(fst R M M₂) : (a : M × M₂) → M) Prod.fst

Tactic:
rfl

Premises used: rfl
-- 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 (α := (a : M × M₂) → M₂) (⇑(snd R M M₂) : (a : M × M₂) → M₂) Prod.snd

Tactic:
rfl

Premises used: rfl
-- 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₂
⊢ Function.Surjective (α := M × M₂) (β := M) (⇑(fst R M M₂) : (a : M × M₂) → M)

Tactic:
fun x => ⟨(x, 0), rfl⟩

Premises used: Prod.mk, Exists.intro, OfNat.ofNat, Function.Surjective, rfl
-- 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₂
⊢ Function.Surjective (α := M × M₂) (β := M₂) (⇑(snd R M M₂) : (a : M × M₂) → M₂)

Tactic:
fun x => ⟨(0, x), rfl⟩

Premises used: Prod.mk, Exists.intro, OfNat.ofNat, Function.Surjective, rfl
-- 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 f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
x y : M
⊢ Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) (x + y) =
    HAdd.hAdd (α := M₂ × M₃) (β := M₂ × M₃)
      (Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) x :
        M₂ × M₃)
      (Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) y :
        M₂ × M₃)

Tactic:
simp only [Function.prod_apply, Prod.mk_add_mk, map_add]

Premises used: Prod.mk_add_mk, map_add, Function.prod_apply
-- 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 f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
c : R
x : M
⊢ Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) (c • x) =
    HSMul.hSMul (α := R) (β := M₂ × M₃) ((RingHom.id R : (a : R) → R) c : R)
      (Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : M) → M₃) x :
        M₂ × M₃)

Tactic:
simp only [Function.prod_apply, Prod.smul_mk, map_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, Function.prod_apply, Prod.smul_mk, map_smul
-- 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₃
⊢ Eq (α := (a : M) → M₂ × M₃) (⇑(f.prod g) : (a : M) → M₂ × M₃)
    (Function.prod (α := fun (a : M) ↦ M₂) (β := fun (a : M) ↦ M₃) (⇑f : (a : M) → M₂) (⇑g : (a : 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
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₃
⊢ fst R M₂ M₃ ∘ₗ f.prod g = f

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₃
⊢ snd R M₂ M₃ ∘ₗ f.prod g = g

Tactic:
rfl

Premises used: rfl
-- 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₂) (prod (fst R M M₂) (snd R M M₂)) id

Tactic:
rfl

Premises used: Function.prod, LinearMap.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₄
h : M →ₗ[R] M₂
⊢ f.prod g ∘ₗ h = (f ∘ₗ h).prod (g ∘ₗ h)

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, rfl
-- 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₂),
    Membership.mem (γ := Submodule R (M × M₂)) (range (inl R M M₂)) x ↔
      Membership.mem (γ := Submodule R (M × M₂)) (ker (snd R M M₂)) x
⊢ Eq (α := Submodule R (M × M₂)) (range (inl R M M₂)) (ker (snd R M M₂))

Tactic:
ext x
-- 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₂
h :
  (∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x) →
    Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂)
h₁ :
  Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂) →
    ∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x
⊢ (∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x) ↔
    Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂)

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₂
y : M
⊢ Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) ((inl R M M₂ : (a : M) → M × M₂) y : M × M₂) : M₂) (0 : M₂)

Tactic:
rfl
-- 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₂
h : Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂)
⊢ ∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x

Tactic:
⟨x.fst, Prod.ext rfl h.symm⟩

Premises used: Prod.fst, Prod.ext, Exists.intro, Eq.symm, rfl
-- 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₂
h : Eq.{w + 1} (α := M₂) ((snd R M M₂ : (a : M × M₂) → M₂) x : M₂) (0 : M₂)
⊢ ∃ (y : M), (inl R M M₂ : (a : M) → M × M₂) y = x

Tactic:
exact ⟨x.fst, Prod.ext rfl h.symm⟩
-- 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 (α := Submodule R (M × M₂)) (ker (snd R M M₂)) (range (inl R M M₂))

Tactic:
Eq.symm <| range_inl R M M₂

Premises used: LinearMap.range_inl, Eq.symm
-- 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₂),
    Membership.mem (γ := Submodule R (M × M₂)) (range (inr R M M₂)) x ↔
      Membership.mem (γ := Submodule R (M × M₂)) (ker (fst R M M₂)) x
⊢ Eq (α := Submodule R (M × M₂)) (range (inr R M M₂)) (ker (fst R M M₂))

Tactic:
ext x
-- 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₂
h :
  (∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x) →
    Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M)
h₁ :
  Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M) →
    ∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x
⊢ (∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x) ↔
    Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M)

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₂
y : M₂
⊢ Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) ((inr R M M₂ : (a : M₂) → M × M₂) y : M × M₂) : M) (0 : M)

Tactic:
rfl
-- 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₂
h : Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M)
⊢ ∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x

Tactic:
⟨x.snd, Prod.ext h.symm rfl⟩

Premises used: Prod.ext, Exists.intro, Eq.symm, Prod.snd, rfl
-- 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₂
h : Eq.{v + 1} (α := M) ((fst R M M₂ : (a : M × M₂) → M) x : M) (0 : M)
⊢ ∃ (y : M₂), (inr R M M₂ : (a : M₂) → M × M₂) y = x

Tactic:
exact ⟨x.snd, Prod.ext h.symm rfl⟩
-- 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 (α := Submodule R (M × M₂)) (ker (fst R M M₂)) (range (inr R M M₂))

Tactic:
Eq.symm <| range_inr R M M₂

Premises used: LinearMap.range_inr, Eq.symm
-- 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 →ₗ[R] M) (fst R M M₂ ∘ₗ inl R M M₂) id

Tactic:
rfl

Premises used: rfl
-- 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 →ₗ[R] M₂) (snd R M M₂ ∘ₗ inl R M M₂) 0

Tactic:
rfl

Premises used: rfl
-- 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₂ →ₗ[R] M) (fst R M M₂ ∘ₗ inr R M M₂) 0

Tactic:
rfl

Premises used: rfl
-- 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₂ →ₗ[R] M₂) (snd R M M₂ ∘ₗ inr R M M₂) id

Tactic:
rfl

Premises used: rfl
-- 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 (α := (a : M) → M × M₂) (⇑(inl R M M₂) : (a : M) → M × M₂) fun (x : M) ↦ (x, 0)

Tactic:
rfl

Premises used: Function.prod, rfl
-- 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 × M₂) ((inl R M M₂ : (a : M) → M × M₂) x : M × M₂) ((x, 0) : M × M₂)

Tactic:
rfl

Premises used: Function.prod, rfl
-- 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 (α := (a : M₂) → M × M₂) (⇑(inr R M M₂) : (a : M₂) → M × M₂) (Prod.mk 0)

Tactic:
rfl

Premises used: Function.prod, rfl
-- 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 × M₂) ((inr R M M₂ : (a : M₂) → M × M₂) x : M × M₂) ((0, x) : M × M₂)

Tactic:
rfl

Premises used: Function.prod, rfl
-- 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 →ₗ[R] M × M₂) (inl R M M₂) (prod id 0)

Tactic:
rfl

Premises used: LinearMap.inl, rfl
-- 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₂ →ₗ[R] M × M₂) (inr R M M₂) (prod 0 id)

Tactic:
rfl

Premises used: LinearMap.inr, rfl
-- 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
⊢ ∀ ⦃a₂ : M⦄,
    Eq (α := M × M₂) ((inl R M M₂ : (a : M) → M × M₂) x : M × M₂) ((inl R M M₂ : (a : M) → M × M₂) a₂ : M × M₂) → x = a₂

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₂
⊢ ∀ ⦃a₂ : M₂⦄,
    Eq (α := M × M₂) ((inr R M M₂ : (a : M₂) → M × M₂) x : M × M₂) ((inr R M M₂ : (a : M₂) → M × M₂) a₂ : M × M₂) →
      x = a₂

Tactic:
simp