awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Free R N
inst_12 : Module.Finite R N
m : M →ₗ[R] P
n : N →ₗ[R] Q
x : M
x_1 : N
⊢ Eq (α := P ⊗[R] Q)
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                  ((((compr₂ₛₗ (TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q))
                              (↑(homTensorHomEquiv R M N P Q) :
                                (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                            (a : M →ₗ[R] P) → (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                          m :
                        (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                      (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                    n) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                  ((((compr₂ₛₗ (TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)) (homTensorHomMap (RingHom.id R) M N P Q) :
                            (a : M →ₗ[R] P) → (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                          m :
                        (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                      (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                    n) :
                (a : M) → N →ₗ[R] P ⊗[R] Q)
              x :
            N →ₗ[R] P ⊗[R] Q) :
          (a : N) → P ⊗[R] Q)
        x_1 :
      P ⊗[R] Q)

Tactic:
simp only [homTensorHomEquiv, compr₂ₛₗ_apply, mk_apply, LinearEquiv.coe_toLinearMap,
    LinearEquiv.trans_apply, lift.equiv_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.refl_symm,
    LinearEquiv.refl_apply, rTensorHomEquivHomRTensor_apply, lTensorHomEquivHomLTensor_apply,
    lTensorHomToHomLTensor_apply, rTensorHomToHomRTensor_apply, homTensorHomMap_apply,
    map_tmul]

Premises used: homTensorHomEquiv, lTensorHomEquivHomLTensor_apply, TensorProduct.mk_apply, rTensorHomEquivHomRTensor_apply, LinearEquiv.trans_apply, LinearEquiv.refl_symm, TensorProduct.lTensorHomToHomLTensor_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.refl_apply, TensorProduct.map_tmul, TensorProduct.homTensorHomMap_apply, LinearEquiv.coe_toLinearMap, TensorProduct.rTensorHomToHomRTensor_apply, LinearMap.compr₂ₛₗ_apply, TensorProduct.lift.equiv_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Free R N
inst_12 : Module.Finite R N
x : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)
rw :
  Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    (((↑(homTensorHomEquiv R M N P Q) : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
          (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
        x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
rw₁ rw₂ :
  Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
⊢ Eq (α := M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomEquiv R M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    ((homTensorHomMap (RingHom.id R) M N P Q : (a : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q)) → M ⊗[R] N →ₗ[R] P ⊗[R] Q) x :
      M ⊗[R] N →ₗ[R] P ⊗[R] Q)

Tactic:
rw [← LinearEquiv.coe_toLinearMap, homTensorHomEquiv_toLinearMap]

Premises used: homTensorHomEquiv_toLinearMap, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Countable R
inst_4 : Countable ι
v : ι → M
⊢ Countable.{u_1 + 1} ↥(Submodule.span R (Set.range v))

Tactic:
Set.countable_coe_iff.mpr (Set.Countable.mono ?_ (Set.countable_range
      (fun c : (ι →₀ R) => c.sum fun i _ => (c i) • v i)))

Premises used: Iff.mpr, Finsupp.sum, Set.countable_coe_iff, Set.countable_range, Set.Countable.mono, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Countable R
inst_4 : Countable ι
v : ι → M
refine :
  (↑(Submodule.span R (Set.range v)) : Set M) ⊆
    Set.range fun (c : ι →₀ R) ↦
      c.sum fun (i : ι) (x : R) ↦ HSMul.hSMul.{u_2, u_1, u_1} (α := R) ((c : (a : ι) → R) i : R) (v i)
⊢ Countable.{u_1 + 1} ↥(Submodule.span R (Set.range v))

Tactic:
refine Set.countable_coe_iff.mpr (Set.Countable.mono ?_ (Set.countable_range
      (fun c : (ι →₀ R) => c.sum fun i _ => (c i) • v i)))

Premises used: Iff.mpr, Finsupp.sum, Set.countable_coe_iff, Set.countable_range, Set.Countable.mono, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Countable R
inst_4 : Countable ι
v : ι → M
⊢ (↑(Submodule.span R (Set.range v)) : Set M) ⊆
    Set.range fun (c : ι →₀ R) ↦
      c.sum fun (i : ι) (x : R) ↦ HSMul.hSMul.{u_2, u_1, u_1} (α := R) ((c : (a : ι) → R) i : R) (v i)

Tactic:
fun _ h => Finsupp.mem_span_range_iff_exists_finsupp.mp (SetLike.mem_coe.mp h)

Premises used: Set.Mem, setOf, Finsupp.sum, Set.Subset, SetLike.mem_coe, Finsupp.mem_span_range_iff_exists_finsupp, Iff.mp, Set.range
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
inst_3 : Countable R
inst_4 : Countable ι
v : ι → M
⊢ (↑(Submodule.span R (Set.range v)) : Set M) ⊆
    Set.range fun (c : ι →₀ R) ↦
      c.sum fun (i : ι) (x : R) ↦ HSMul.hSMul.{u_2, u_1, u_1} (α := R) ((c : (a : ι) → R) i : R) (v i)

Tactic:
exact fun _ h => Finsupp.mem_span_range_iff_exists_finsupp.mp (SetLike.mem_coe.mp h)

Premises used: SetLike.mem_coe, Finsupp.mem_span_range_iff_exists_finsupp, Iff.mp
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Countable R
inst_4 : Module.Finite R M
obtain : ∀ (n : ℕ) (s : Fin n → M) (h : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤), Countable M
⊢ Countable M

Tactic:
obtain ⟨n, s, h⟩ := Module.Finite.exists_fin (R := R) (M := M)

Premises used: Module.Finite.exists_fin
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Countable R
inst_4 : Module.Finite R M
n : ℕ
s : Fin n → M
h : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
rw : Set.Countable.{u_1} (α := M) Set.univ
⊢ Countable M

Tactic:
rw [← Set.countable_univ_iff]

Premises used: Set.countable_univ_iff
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Countable R
inst_4 : Module.Finite R M
n : ℕ
s : Fin n → M
h : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
⊢ Countable.{u_1 + 1} ↥(Submodule.span R (Set.range s))

Tactic:
have : Countable (Submodule.span R (Set.range s)) := inferInstance
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Countable R
inst_4 : Module.Finite R M
n : ℕ
s : Fin n → M
h : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : Countable.{u_1 + 1} ↥(Submodule.span R (Set.range s))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Countable.{u_1 + 1} ↥⊤), Set.Countable.{u_1} (α := M) Set.univ
⊢ Set.Countable.{u_1} (α := M) Set.univ

Tactic:
rwa [h] at this
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hM : Uncountable M
inst_3 : Module.Finite R M
by_contra! : ∀ (this : Countable R), False
⊢ Uncountable R

Tactic:
by_contra!
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hM : Uncountable M
inst_3 : Module.Finite R M
this : Countable R
⊢ False

Tactic:
(uncountable_iff_not_countable _).mp hM <| Countable.of_moduleFinite (R := R)

Premises used: uncountable_iff_not_countable, Iff.mp, Finsupp.Countable.of_moduleFinite
-- Module: Mathlib.LinearAlgebra.Countable
Goal:
M : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hM : Uncountable M
inst_3 : Module.Finite R M
this : Countable R
⊢ False

Tactic:
exact (uncountable_iff_not_countable _).mp hM <| Countable.of_moduleFinite (R := R)

Premises used: uncountable_iff_not_countable, Iff.mp, Finsupp.Countable.of_moduleFinite
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
H1 :
  ∀ (m₁ m₂ n : Fin 3 → R),
    ![(m₁ + m₂) 1 * n 2 - (m₁ + m₂) 2 * n 1, (m₁ + m₂) 2 * n 0 - (m₁ + m₂) 0 * n 2,
        (m₁ + m₂) 0 * n 1 - (m₁ + m₂) 1 * n 0] =
      ![m₁ 1 * n 2 - m₁ 2 * n 1, m₁ 2 * n 0 - m₁ 0 * n 2, m₁ 0 * n 1 - m₁ 1 * n 0] +
        ![m₂ 1 * n 2 - m₂ 2 * n 1, m₂ 2 * n 0 - m₂ 0 * n 2, m₂ 0 * n 1 - m₂ 1 * n 0]
H2 :
  ∀ (c : R) (m n : Fin 3 → R),
    ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]
H3 :
  ∀ (m n₁ n₂ : Fin 3 → R),
    ![m 1 * (n₁ + n₂) 2 - m 2 * (n₁ + n₂) 1, m 2 * (n₁ + n₂) 0 - m 0 * (n₁ + n₂) 2,
        m 0 * (n₁ + n₂) 1 - m 1 * (n₁ + n₂) 0] =
      ![m 1 * n₁ 2 - m 2 * n₁ 1, m 2 * n₁ 0 - m 0 * n₁ 2, m 0 * n₁ 1 - m 1 * n₁ 0] +
        ![m 1 * n₂ 2 - m 2 * n₂ 1, m 2 * n₂ 0 - m 0 * n₂ 2, m 0 * n₂ 1 - m 1 * n₂ 0]
H4 :
  ∀ (c : R) (m n : Fin 3 → R),
    ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
      c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]
⊢ (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R

Tactic:
apply LinearMap.mk₂ R fun a b : Fin 3 → R =>
      ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]

Premises used: LinearMap.mk₂, HMul.hMul, HSub.hSub, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m₁ m₂ n : Fin 3 → R
H1 :
  ![(m₁ 1 + m₂ 1) * n 2 - (m₁ 2 + m₂ 2) * n 1, (m₁ 2 + m₂ 2) * n 0 - (m₁ 0 + m₂ 0) * n 2,
      (m₁ 0 + m₂ 0) * n 1 - (m₁ 1 + m₂ 1) * n 0] =
    ![m₁ 1 * n 2 - m₁ 2 * n 1 + (m₂ 1 * n 2 - m₂ 2 * n 1), m₁ 2 * n 0 - m₁ 0 * n 2 + (m₂ 2 * n 0 - m₂ 0 * n 2),
      m₁ 0 * n 1 - m₁ 1 * n 0 + (m₂ 0 * n 1 - m₂ 1 * n 0)]
⊢ ![(m₁ + m₂) 1 * n 2 - (m₁ + m₂) 2 * n 1, (m₁ + m₂) 2 * n 0 - (m₁ + m₂) 0 * n 2,
      (m₁ + m₂) 0 * n 1 - (m₁ + m₂) 1 * n 0] =
    ![m₁ 1 * n 2 - m₁ 2 * n 1, m₁ 2 * n 0 - m₁ 0 * n 2, m₁ 0 * n 1 - m₁ 1 * n 0] +
      ![m₂ 1 * n 2 - m₂ 2 * n 1, m₂ 2 * n 0 - m₂ 0 * n 2, m₂ 0 * n 1 - m₂ 1 * n 0]

Tactic:
simp_rw [vec3_add, Pi.add_apply]

Premises used: Matrix.vec3_add, Pi.add_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m₁ m₂ n : Fin 3 → R
H1 : (m₁ 1 + m₂ 1) * n 2 - (m₁ 2 + m₂ 2) * n 1 = m₁ 1 * n 2 - m₁ 2 * n 1 + (m₂ 1 * n 2 - m₂ 2 * n 1)
H1₁ : (m₁ 2 + m₂ 2) * n 0 - (m₁ 0 + m₂ 0) * n 2 = m₁ 2 * n 0 - m₁ 0 * n 2 + (m₂ 2 * n 0 - m₂ 0 * n 2)
H1₂ : (m₁ 0 + m₂ 0) * n 1 - (m₁ 1 + m₂ 1) * n 0 = m₁ 0 * n 1 - m₁ 1 * n 0 + (m₂ 0 * n 1 - m₂ 1 * n 0)
⊢ ![(m₁ 1 + m₂ 1) * n 2 - (m₁ 2 + m₂ 2) * n 1, (m₁ 2 + m₂ 2) * n 0 - (m₁ 0 + m₂ 0) * n 2,
      (m₁ 0 + m₂ 0) * n 1 - (m₁ 1 + m₂ 1) * n 0] =
    ![m₁ 1 * n 2 - m₁ 2 * n 1 + (m₂ 1 * n 2 - m₂ 2 * n 1), m₁ 2 * n 0 - m₁ 0 * n 2 + (m₂ 2 * n 0 - m₂ 0 * n 2),
      m₁ 0 * n 1 - m₁ 1 * n 0 + (m₂ 0 * n 1 - m₂ 1 * n 0)]

Tactic:
apply vec3_eq

Premises used: Matrix.vec3_eq
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m₁ m₂ n : Fin 3 → R
⊢ (m₁ 1 + m₂ 1) * n 2 - (m₁ 2 + m₂ 2) * n 1 = m₁ 1 * n 2 - m₁ 2 * n 1 + (m₂ 1 * n 2 - m₂ 2 * n 1)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m₁ m₂ n : Fin 3 → R
⊢ (m₁ 2 + m₂ 2) * n 0 - (m₁ 0 + m₂ 0) * n 2 = m₁ 2 * n 0 - m₁ 0 * n 2 + (m₂ 2 * n 0 - m₂ 0 * n 2)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m₁ m₂ n : Fin 3 → R
⊢ (m₁ 0 + m₂ 0) * n 1 - (m₁ 1 + m₂ 1) * n 0 = m₁ 0 * n 1 - m₁ 1 * n 0 + (m₂ 0 * n 1 - m₂ 1 * n 0)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
c : R
m n : Fin 3 → R
H2 :
  ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
    ![c • (m 1 * n 2 - m 2 * n 1), c • (m 2 * n 0 - m 0 * n 2), c • (m 0 * n 1 - m 1 * n 0)]
H2₁ :
  ![c • m 1 * n 2 - c • m 2 * n 1, c • m 2 * n 0 - c • m 0 * n 2, c • m 0 * n 1 - c • m 1 * n 0] =
    ![c • (m 1 * n 2 - m 2 * n 1), c • (m 2 * n 0 - m 0 * n 2), c • (m 0 * n 1 - m 1 * n 0)]
H2₂ :
  ![c • m 1 * n 2 - c • m 2 * n 1, c • m 2 * n 0 - c • m 0 * n 2, c • m 0 * n 1 - c • m 1 * n 0] =
    ![c • (m 1 * n 2) - c • (m 2 * n 1), c • (m 2 * n 0) - c • (m 0 * n 2), c • (m 0 * n 1) - c • (m 1 * n 0)]
⊢ ![(c • m) 1 * n 2 - (c • m) 2 * n 1, (c • m) 2 * n 0 - (c • m) 0 * n 2, (c • m) 0 * n 1 - (c • m) 1 * n 0] =
    c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
simp_rw [smul_vec3, Pi.smul_apply, smul_sub, smul_mul_assoc]

Premises used: smul_mul_assoc, Matrix.smul_vec3, smul_sub, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m n₁ n₂ : Fin 3 → R
H3 :
  ![m 1 * (n₁ 2 + n₂ 2) - m 2 * (n₁ 1 + n₂ 1), m 2 * (n₁ 0 + n₂ 0) - m 0 * (n₁ 2 + n₂ 2),
      m 0 * (n₁ 1 + n₂ 1) - m 1 * (n₁ 0 + n₂ 0)] =
    ![m 1 * n₁ 2 - m 2 * n₁ 1 + (m 1 * n₂ 2 - m 2 * n₂ 1), m 2 * n₁ 0 - m 0 * n₁ 2 + (m 2 * n₂ 0 - m 0 * n₂ 2),
      m 0 * n₁ 1 - m 1 * n₁ 0 + (m 0 * n₂ 1 - m 1 * n₂ 0)]
⊢ ![m 1 * (n₁ + n₂) 2 - m 2 * (n₁ + n₂) 1, m 2 * (n₁ + n₂) 0 - m 0 * (n₁ + n₂) 2,
      m 0 * (n₁ + n₂) 1 - m 1 * (n₁ + n₂) 0] =
    ![m 1 * n₁ 2 - m 2 * n₁ 1, m 2 * n₁ 0 - m 0 * n₁ 2, m 0 * n₁ 1 - m 1 * n₁ 0] +
      ![m 1 * n₂ 2 - m 2 * n₂ 1, m 2 * n₂ 0 - m 0 * n₂ 2, m 0 * n₂ 1 - m 1 * n₂ 0]

Tactic:
simp_rw [vec3_add, Pi.add_apply]

Premises used: Matrix.vec3_add, Pi.add_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m n₁ n₂ : Fin 3 → R
H3 : m 1 * (n₁ 2 + n₂ 2) - m 2 * (n₁ 1 + n₂ 1) = m 1 * n₁ 2 - m 2 * n₁ 1 + (m 1 * n₂ 2 - m 2 * n₂ 1)
H3₁ : m 2 * (n₁ 0 + n₂ 0) - m 0 * (n₁ 2 + n₂ 2) = m 2 * n₁ 0 - m 0 * n₁ 2 + (m 2 * n₂ 0 - m 0 * n₂ 2)
H3₂ : m 0 * (n₁ 1 + n₂ 1) - m 1 * (n₁ 0 + n₂ 0) = m 0 * n₁ 1 - m 1 * n₁ 0 + (m 0 * n₂ 1 - m 1 * n₂ 0)
⊢ ![m 1 * (n₁ 2 + n₂ 2) - m 2 * (n₁ 1 + n₂ 1), m 2 * (n₁ 0 + n₂ 0) - m 0 * (n₁ 2 + n₂ 2),
      m 0 * (n₁ 1 + n₂ 1) - m 1 * (n₁ 0 + n₂ 0)] =
    ![m 1 * n₁ 2 - m 2 * n₁ 1 + (m 1 * n₂ 2 - m 2 * n₂ 1), m 2 * n₁ 0 - m 0 * n₁ 2 + (m 2 * n₂ 0 - m 0 * n₂ 2),
      m 0 * n₁ 1 - m 1 * n₁ 0 + (m 0 * n₂ 1 - m 1 * n₂ 0)]

Tactic:
apply vec3_eq

Premises used: Matrix.vec3_eq
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m n₁ n₂ : Fin 3 → R
⊢ m 1 * (n₁ 2 + n₂ 2) - m 2 * (n₁ 1 + n₂ 1) = m 1 * n₁ 2 - m 2 * n₁ 1 + (m 1 * n₂ 2 - m 2 * n₂ 1)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m n₁ n₂ : Fin 3 → R
⊢ m 2 * (n₁ 0 + n₂ 0) - m 0 * (n₁ 2 + n₂ 2) = m 2 * n₁ 0 - m 0 * n₁ 2 + (m 2 * n₂ 0 - m 0 * n₂ 2)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
m n₁ n₂ : Fin 3 → R
⊢ m 0 * (n₁ 1 + n₂ 1) - m 1 * (n₁ 0 + n₂ 0) = m 0 * n₁ 1 - m 1 * n₁ 0 + (m 0 * n₂ 1 - m 1 * n₂ 0)

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
c : R
m n : Fin 3 → R
H4 :
  ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
    ![c • (m 1 * n 2 - m 2 * n 1), c • (m 2 * n 0 - m 0 * n 2), c • (m 0 * n 1 - m 1 * n 0)]
H4₁ :
  ![m 1 * c • n 2 - m 2 * c • n 1, m 2 * c • n 0 - m 0 * c • n 2, m 0 * c • n 1 - m 1 * c • n 0] =
    ![c • (m 1 * n 2 - m 2 * n 1), c • (m 2 * n 0 - m 0 * n 2), c • (m 0 * n 1 - m 1 * n 0)]
H4₂ :
  ![m 1 * c • n 2 - m 2 * c • n 1, m 2 * c • n 0 - m 0 * c • n 2, m 0 * c • n 1 - m 1 * c • n 0] =
    ![c • (m 1 * n 2) - c • (m 2 * n 1), c • (m 2 * n 0) - c • (m 0 * n 2), c • (m 0 * n 1) - c • (m 1 * n 0)]
⊢ ![m 1 * (c • n) 2 - m 2 * (c • n) 1, m 2 * (c • n) 0 - m 0 * (c • n) 2, m 0 * (c • n) 1 - m 1 * (c • n) 0] =
    c • ![m 1 * n 2 - m 2 * n 1, m 2 * n 0 - m 0 * n 2, m 0 * n 1 - m 1 * n 0]

Tactic:
simp_rw [smul_vec3, Pi.smul_apply, smul_sub, mul_smul_comm]

Premises used: Matrix.smul_vec3, smul_sub, mul_smul_comm, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
a b : Fin 3 → R
⊢ (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) a : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
        (a : Fin 3 → R) → Fin 3 → R)
      b =
    ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
⊢ Eq (α := Fin 3 → R)
    (-(((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          w :
      Fin 3 → R)
    ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        v :
      Fin 3 → R)

Tactic:
simp [cross_apply, mul_comm]

Premises used: cross_apply, mul_comm
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
rw :
  Eq (α := Fin 3 → R)
    ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        w :
      Fin 3 → R)
    (-(((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          v :
      Fin 3 → R)
rw₁ rw₂ :
  Eq (α := Fin 3 → R)
    ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        w :
      Fin 3 → R)
    ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        w :
      Fin 3 → R)
⊢ HAdd.hAdd (α := Fin 3 → R) (β := Fin 3 → R)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          w :
        Fin 3 → R)
      ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          v :
        Fin 3 → R) =
    0

Tactic:
rw [add_eq_zero_iff_eq_neg, cross_anticomm]

Premises used: cross_anticomm, add_eq_zero_iff_eq_neg
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
v : Fin 3 → R
⊢ Eq (α := Fin 3 → R)
    ((((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        v :
      Fin 3 → R)
    (0 : Fin 3 → R)

Tactic:
simp [cross_apply, mul_comm]

Premises used: cross_apply, mul_comm
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
rw :
  v 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        v 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      v 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    0
⊢ v ⬝ᵥ
      (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        w =
    0

Tactic:
rw [cross_apply, vec3_dotProduct]

Premises used: Matrix.vec3_dotProduct, cross_apply
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
dsimp : v 0 * (v 1 * w 2 - v 2 * w 1) + v 1 * (v 2 * w 0 - v 0 * w 2) + v 2 * (v 0 * w 1 - v 1 * w 0) = 0
⊢ v 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        v 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      v 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    0

Tactic:
dsimp only [Matrix.cons_val]

Premises used: Matrix.cons_val
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
⊢ v 0 * (v 1 * w 2 - v 2 * w 1) + v 1 * (v 2 * w 0 - v 0 * w 2) + v 2 * (v 0 * w 1 - v 1 * w 0) = 0

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
rw :
  w ⬝ᵥ
      -(((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          v =
    0
rw₁ :
  -(w ⬝ᵥ
        (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
            (a : Fin 3 → R) → Fin 3 → R)
          v) =
    0
rw₂ : Eq.{u_1 + 1} (α := R) (-0) 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ w ⬝ᵥ
      (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        w =
    0

Tactic:
rw [← cross_anticomm, dotProduct_neg, dot_self_cross, neg_zero]

Premises used: dot_self_cross, cross_anticomm, neg_zero, dotProduct_neg
-- Module: Mathlib.LinearAlgebra.CrossProduct
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
simp_rw :
  u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    v 0 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 0 +
        v 1 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 1 +
      v 2 * ![w 1 * u 2 - w 2 * u 1, w 2 * u 0 - w 0 * u 2, w 0 * u 1 - w 1 * u 0] 2
⊢ u ⬝ᵥ
      (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) v : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        w =
    v ⬝ᵥ
      (((crossProduct : (a : Fin 3 → R) → (Fin 3 → R) →ₗ[R] Fin 3 → R) w : (Fin 3 → R) →ₗ[R] Fin 3 → R) :
          (a : Fin 3 → R) → Fin 3 → R)
        u

Tactic:
simp_rw [cross_apply, vec3_dotProduct]

Premises used: Matrix.vec3_dotProduct, cross_apply