awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Countable (goal)
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))
have 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)
Tactic: refine Set.countable_coe_iff.mpr (Set.Countable.mono ?_ (Set.countable_range
      (fun c : (ι →₀ R) => c.sum fun i _ => (c i) • v i)))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Countable (goal)
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
⊢ Countable M
have obtain : ∀ (n : ℕ) (s : Fin n → M) (h : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤), Countable M
Tactic: obtain ⟨n, s, h⟩ := Module.Finite.exists_fin (R := R) (M := M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Countable (goal)
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 M
have rw : Set.Countable.{u_1} (α := M) Set.univ
Tactic: rw [← Set.countable_univ_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Countable (hypothesis)
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)) ⊤
⊢ Set.Countable.{u_1} (α := M) Set.univ
have this : Countable.{u_1 + 1} ↥(Submodule.span R (Set.range s))
Tactic: have : Countable (Submodule.span R (Set.range s)) := inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.Countable (goal)
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))
⊢ Set.Countable.{u_1} (α := M) Set.univ
have rwa : ∀ (this : Countable.{u_1 + 1} ↥⊤), Set.Countable.{u_1} (α := M) Set.univ
Tactic: rwa [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Countable (goal)
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
⊢ Uncountable R
have by_contra! : ∀ (this : Countable R), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R
have 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]
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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]
⊢ (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R
have 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]
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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]
⊢ (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R
have 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]
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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]
⊢ (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R
have 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]
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
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]
have 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)]
Tactic: simp_rw [vec3_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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₁ 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)]
have 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)
Tactic: apply vec3_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)
⊢ ![(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)]
have 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)
Tactic: apply vec3_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)
⊢ ![(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)]
have 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)
Tactic: apply vec3_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
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]
have 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)]
Tactic: simp_rw [smul_vec3, Pi.smul_apply, smul_sub, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)]
⊢ ![(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]
have 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)]
Tactic: simp_rw [smul_vec3, Pi.smul_apply, smul_sub, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)]
⊢ ![(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]
have 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)]
Tactic: simp_rw [smul_vec3, Pi.smul_apply, smul_sub, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
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]
have 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)]
Tactic: simp_rw [vec3_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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 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)]
have 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)
Tactic: apply vec3_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)
⊢ ![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)]
have 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)
Tactic: apply vec3_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)
⊢ ![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)]
have 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)
Tactic: apply vec3_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
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]
have 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)]
Tactic: simp_rw [smul_vec3, Pi.smul_apply, smul_sub, mul_smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)]
⊢ ![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]
have 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)]
Tactic: simp_rw [smul_vec3, Pi.smul_apply, smul_sub, mul_smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)]
⊢ ![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]
have 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)]
Tactic: simp_rw [smul_vec3, Pi.smul_apply, smul_sub, mul_smul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
v 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
have 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)
Tactic: rw [add_eq_zero_iff_eq_neg, cross_anticomm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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)
⊢ 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
have 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)
Tactic: rw [add_eq_zero_iff_eq_neg, cross_anticomm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
⊢ 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
have 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
Tactic: rw [cross_apply, vec3_dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
⊢ 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
have 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
Tactic: dsimp only [Matrix.cons_val]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
v w : Fin 3 → R
⊢ 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
have 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
Tactic: rw [← cross_anticomm, dotProduct_neg, dot_self_cross, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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
⊢ 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
have 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
Tactic: rw [← cross_anticomm, dotProduct_neg, dot_self_cross, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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
⊢ 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
have rw₂ : Eq.{u_1 + 1} (α := R) (-0) 0
Tactic: rw [← cross_anticomm, dotProduct_neg, dot_self_cross, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
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
⊢ 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
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← cross_anticomm, dotProduct_neg, dot_self_cross, neg_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CrossProduct (goal)
Goal:
R : Type u_1
inst : CommRing R
u v w : Fin 3 → R
⊢ 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
have 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
Tactic: simp_rw [cross_apply, vec3_dotProduct]