awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
r : R
rw :
  (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
          ExteriorAlgebra R M →ₗ[R] N) :
        (a : ExteriorAlgebra R M) → N)
      (HSMul.hSMul (β := ExteriorAlgebra R M) r 1) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
rw₁ :
  HSMul.hSMul (β := N) r
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          1 :
        N) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
rw₂ rw₃ :
  HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)
⊢ (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
          ExteriorAlgebra R M →ₗ[R] N) :
        (a : ExteriorAlgebra R M) → N)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) =
    HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]

Premises used: ExteriorAlgebra.liftAlternating_one, Algebra.algebraMap_eq_smul_one, map_smul
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
rw :
  Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f n : (a : Fin n → M) → N) v : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) v : ExteriorAlgebra R M) :
      N)
    ((f n : (a : Fin n → M) → N) v : N)

Tactic:
rw [ιMulti_apply]

Premises used: ExteriorAlgebra.ιMulti_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin 0 → M
zero :
  Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        (List.prod []) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
zero₁ :
  Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        1 :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)
zero₂ : Eq.{u_3 + 1} (α := N) ((f 0 : (a : Fin 0 → M) → N) 0 : N) ((f 0 : (a : Fin 0 → M) → N) v : N)
zero₃ zero₄ : Eq.{u_3 + 1} (α := N) ((f 0 : (a : Fin 0 → M) → N) v : N) ((f 0 : (a : Fin 0 → M) → N) v : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f 0 : (a : Fin 0 → M) → N) v : N)

Tactic:
rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]

Premises used: ExteriorAlgebra.liftAlternating_one, List.ofFn_zero, List.prod_nil, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    Eq.{u_3 + 1} (α := N)
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f n : (a : Fin n → M) → N) v : N)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
succ :
  Eq.{u_3 + 1} (α := N) ((f n.succ : (a : Fin n.succ → M) → N) (Matrix.vecCons (v 0) fun (i : Fin n) ↦ v i.succ) : N)
    ((f (n + 1) : (a : Fin (n + 1) → M) → N) v : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        (List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f (n + 1) : (a : Fin (n + 1) → M) → N) v : N)

Tactic:
rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
      AlternatingMap.curryLeft_apply_apply]

Premises used: ExteriorAlgebra.liftAlternating_ι_mul, AlternatingMap.curryLeft_apply_apply, List.prod_cons, List.ofFn_succ
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    Eq.{u_3 + 1} (α := N)
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f n : (a : Fin n → M) → N) v : N)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
succ : (Matrix.vecCons (v 0) fun (i : Fin n) ↦ v i.succ) = v
⊢ Eq.{u_3 + 1} (α := N) ((f n.succ : (a : Fin n.succ → M) → N) (Matrix.vecCons (v 0) fun (i : Fin n) ↦ v i.succ) : N)
    ((f (n + 1) : (a : Fin (n + 1) → M) → N) v : N)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    Eq.{u_3 + 1} (α := N)
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f n : (a : Fin n → M) → N) v : N)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (Matrix.vecCons (v 0) fun (i : Fin n) ↦ v i.succ) = v

Tactic:
Matrix.cons_head_tail _

Premises used: Matrix.vecHead, Matrix.cons_head_tail, Matrix.vecTail
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    Eq.{u_3 + 1} (α := N)
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f n : (a : Fin n → M) → N) v : N)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (Matrix.vecCons (v 0) fun (i : Fin n) ↦ v i.succ) = v

Tactic:
exact Matrix.cons_head_tail _

Premises used: Matrix.cons_head_tail
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
zero :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin 0 → M),
    Eq.{u_3 + 1} (α := N)
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          (List.prod (List.ofFn (n := 0) fun (i : Fin 0) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f 0 : (a : Fin 0 → M) → N) v : N)
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
        Eq.{u_3 + 1} (α := N)
          ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                  ExteriorAlgebra R M →ₗ[R] N) :
                (a : ExteriorAlgebra R M) → N)
              (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
            N)
          ((f n : (a : Fin n → M) → N) v : N))
    (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin (n + 1) → M),
    Eq.{u_3 + 1} (α := N)
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          (List.prod (List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
        N)
      ((f (n + 1) : (a : Fin (n + 1) → M) → N) v : N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            ExteriorAlgebra R M →ₗ[R] N) :
          (a : ExteriorAlgebra R M) → N)
        (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (v i))) :
      N)
    ((f n : (a : Fin n → M) → N) v : N)

Tactic:
induction n generalizing f with
  | zero => rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
  | succ n ih =>
    rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
      AlternatingMap.curryLeft_apply_apply]
    congr
    exact Matrix.cons_head_tail _

Premises used: ExteriorAlgebra.liftAlternating_ι_mul, AlternatingMap.curryLeft_apply_apply, ExteriorAlgebra.liftAlternating_one, List.ofFn_zero, Matrix.cons_head_tail, List.prod_nil, List.prod_cons, List.ofFn_succ
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ LinearMap.compAlternatingMap ((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f)
      (ιMulti R n) =
    f n

Tactic:
AlternatingMap.ext <| liftAlternating_apply_ιMulti f

Premises used: ExteriorAlgebra.liftAlternating_apply_ιMulti, AlternatingMap.ext
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
h :
  ∀ (v : ExteriorAlgebra R M),
    Eq.{u_4 + 1} (α := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          v :
        N')
      ((g ∘ₗ (liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
            (a : ExteriorAlgebra R M) → N')
          v :
        N')
⊢ Eq (α := ExteriorAlgebra R M →ₗ[R] N')
    ((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
      g.compAlternatingMap (f i))
    (g ∘ₗ (liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f)

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : ExteriorAlgebra R M
h :
  Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        v :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            v :
          N) :
      N')
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        v :
      N')
    ((g ∘ₗ (liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
          (a : ExteriorAlgebra R M) → N')
        v :
      N')

Tactic:
rw [LinearMap.comp_apply]

Premises used: LinearMap.comp_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
r : R
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
h :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    (g : (a : N) → N')
      ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
              ExteriorAlgebra R M →ₗ[R] N) :
            (a : ExteriorAlgebra R M) → N)
          ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
            CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
        N)
h₁ :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    (g : (a : N) → N') (HSMul.hSMul (β := N) r ((f 0 : (a : Fin 0 → M) → N) 0 : N))
h₂ :
  HSMul.hSMul (β := N') r ((g.compAlternatingMap (f 0) : (a : Fin 0 → M) → N') 0 : N') =
    HSMul.hSMul (β := N') r ((g : (a : N) → N') ((f 0 : (a : Fin 0 → M) → N) 0 : N) : N')
h₃ h₄ :
  HSMul.hSMul (β := N') r ((g : (a : N) → N') ((f 0 : (a : Fin 0 → M) → N) 0 : N) : N') =
    HSMul.hSMul (β := N') r ((g : (a : N) → N') ((f 0 : (a : Fin 0 → M) → N) 0 : N) : N')
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
          CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            ((algebraMap R (CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) : (a : R) → CliffordAlgebra 0) r :
              CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) :
          N) :
      N')

Tactic:
rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul,
      LinearMap.compAlternatingMap_apply]

Premises used: LinearMap.compAlternatingMap_apply, ExteriorAlgebra.liftAlternating_algebraMap, map_smul
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
x : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0
m : M
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    Eq.{u_4 + 1} (α := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          x :
        N')
      ((g : (a : N) → N')
          ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                  ExteriorAlgebra R M →ₗ[R] N) :
                (a : ExteriorAlgebra R M) → N)
              x :
            N) :
        N')
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
h :
  Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            (AlternatingMap.curryLeft (g.compAlternatingMap (f i.succ)) : (a : M) → M [⋀^Fin i]→ₗ[R] N') m :
          (a : ExteriorAlgebra R M) → N')
        x :
      N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m) :
          (a : ExteriorAlgebra R M) → N')
        x :
      N')
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap (f i) :
          (a : ExteriorAlgebra R M) → N')
        (HMul.hMul (α := CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
          ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0) x) :
      N')
    ((g : (a : N) → N')
        ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                ExteriorAlgebra R M →ₗ[R] N) :
              (a : ExteriorAlgebra R M) → N)
            (HMul.hMul (α := CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
              ((CliffordAlgebra.ι 0 : (a : M) → CliffordAlgebra 0) m : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0)
              x) :
          N) :
      N')

Tactic:
rw [liftAlternating_ι_mul, liftAlternating_ι_mul, ← hx]

Premises used: ExteriorAlgebra.liftAlternating_ι_mul
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
g : N →ₗ[R] N'
x : CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0
m : M
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    Eq.{u_4 + 1} (α := N')
      (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
              g.compAlternatingMap (f i) :
            (a : ExteriorAlgebra R M) → N')
          x :
        N')
      ((g : (a : N) → N')
          ((((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] N) f :
                  ExteriorAlgebra R M →ₗ[R] N) :
                (a : ExteriorAlgebra R M) → N)
              x :
            N) :
        N')
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ Eq.{u_4 + 1} (α := N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            (AlternatingMap.curryLeft (g.compAlternatingMap (f i.succ)) : (a : M) → M [⋀^Fin i]→ₗ[R] N') m :
          (a : ExteriorAlgebra R M) → N')
        x :
      N')
    (((liftAlternating : (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N') → ExteriorAlgebra R M →ₗ[R] N') fun (i : ℕ) ↦
            g.compAlternatingMap ((AlternatingMap.curryLeft (f i.succ) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m) :
          (a : ExteriorAlgebra R M) → N')
        x :
      N')

Tactic:
simp_rw [AlternatingMap.curryLeft_compAlternatingMap]

Premises used: AlternatingMap.curryLeft_compAlternatingMap
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup N'
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N'
F : ExteriorAlgebra R M →ₗ[R] N
rw : F ∘ₗ LinearMap.id = F
rw₁ rw₂ : F = F
⊢ F ∘ₗ
      (liftAlternating :
          (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] ExteriorAlgebra R M) → ExteriorAlgebra R M →ₗ[R] ExteriorAlgebra R M)
        (ιMulti R) =
    F

Tactic:
rw [liftAlternating_ιMulti, LinearMap.comp_id]

Premises used: ExteriorAlgebra.liftAlternating_ιMulti, LinearMap.comp_id
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
f g : ExteriorAlgebra R M →ₗ[R] N
h : ∀ (i : ℕ), f.compAlternatingMap (ιMulti R i) = g.compAlternatingMap (ιMulti R i)
⊢ f = g

Tactic:
liftAlternatingEquiv.symm.injective <| funext h

Premises used: LinearEquiv.symm, funext, LinearEquiv.injective, ExteriorAlgebra.liftAlternatingEquiv
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
a : Fin n → M
⊢ Eq (α := ExteriorAlgebra R M)
    ((↑((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) a) : ExteriorAlgebra R M) : ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) a : ExteriorAlgebra R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
⊢ Eq (α := (s : (↑(powersetCard I n) : Type u_4)) → ExteriorAlgebra R M) (ExteriorAlgebra.ιMulti_family R n v)
    (Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
        Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M) x) ∘
      ιMulti_family R n v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I n) : Type u_4)
⊢ Eq (α := ExteriorAlgebra R M) (↑(ιMulti_family R n v s) : ExteriorAlgebra R M) (ExteriorAlgebra.ιMulti_family R n v s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R (range (ι := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)))
    (⋀[R]^n M)

Tactic:
ExteriorAlgebra.ιMulti_span_fixedDegree R n

Premises used: ExteriorAlgebra.ιMulti_span_fixedDegree
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
a :
  LE.le (α := Submodule R (ExteriorAlgebra R M))
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))
    (⋀[R]^n M)
a₁ :
  LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))
    (⋀[R]^n M)

Tactic:
apply le_antisymm

Premises used: le_antisymm