awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
simp :
  (ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
      (Fin.append
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
            (a : Fin m) → I))
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
            (a : Fin n) → I))) =
    HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M)
      ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (m + n))) → ℤˣ) (permOfDisjoint h) : ℤˣ)
      ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I)
                    (disjUnion h) :
                  Fin (m + n) ↪o I) :
              (a : Fin (m + n)) → I)) :
        ExteriorAlgebra R M)
⊢ HMul.hMul (α := ExteriorAlgebra R M) (ιMulti_family R m v s) (ιMulti_family R n v t) =
    HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M)
      ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (m + n))) → ℤˣ) (permOfDisjoint h) : ℤˣ)
      (ιMulti_family R (m + n) v (disjUnion h))

Tactic:
simp only [ιMulti_family, ιMulti_mul_ιMulti]

Premises used: ExteriorAlgebra.ιMulti_mul_ιMulti, ExteriorAlgebra.ιMulti_family
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
rw :
  Eq (α := ExteriorAlgebra R M)
    ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
        (Fin.append
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
              (a : Fin m) → I))
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
              (a : Fin n) → I))) :
      ExteriorAlgebra R M)
    ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
        (Function.comp (β := Fin (m + n))
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I)
                    (disjUnion h) :
                  Fin (m + n) ↪o I) :
              (a : Fin (m + n)) → I))
          (⇑(Equiv.trans (Equiv.symm finSumFinEquiv)
                ((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                      Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)).trans
                  ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h).trans
                    (↑(OrderIso.symm (orderIsoOfFin (disjUnion h))) : ↥(↑(disjUnion h) : Finset I) ≃ Fin (m + n))))) :
            (a : Fin (m + n)) → Fin (m + n))) :
      ExteriorAlgebra R M)
⊢ (ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
      (Fin.append
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
            (a : Fin m) → I))
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
            (a : Fin n) → I))) =
    HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M)
      ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (m + n))) → ℤˣ) (permOfDisjoint h) : ℤˣ)
      ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I)
                    (disjUnion h) :
                  Fin (m + n) ↪o I) :
              (a : Fin (m + n)) → I)) :
        ExteriorAlgebra R M)

Tactic:
rw [← AlternatingMap.map_perm, permOfDisjoint]

Premises used: AlternatingMap.map_perm, Set.powersetCard.permOfDisjoint
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
h₁ :
  Eq (α := Fin (m + n) → M)
    (Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)))
    (Function.comp (β := Fin (m + n))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I) (disjUnion h) :
              Fin (m + n) ↪o I) :
          (a : Fin (m + n)) → I))
      (⇑(Equiv.trans (Equiv.symm finSumFinEquiv)
            ((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                  Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)).trans
              ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h).trans
                (↑(OrderIso.symm (orderIsoOfFin (disjUnion h))) : ↥(↑(disjUnion h) : Finset I) ≃ Fin (m + n))))) :
        (a : Fin (m + n)) → Fin (m + n)))
⊢ Eq (α := ExteriorAlgebra R M)
    ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
        (Fin.append
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
              (a : Fin m) → I))
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
              (a : Fin n) → I))) :
      ExteriorAlgebra R M)
    ((ιMulti R (m + n) : (a : Fin (m + n) → M) → ExteriorAlgebra R M)
        (Function.comp (β := Fin (m + n))
          (v ∘
            (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I)
                    (disjUnion h) :
                  Fin (m + n) ↪o I) :
              (a : Fin (m + n)) → I))
          (⇑(Equiv.trans (Equiv.symm finSumFinEquiv)
                ((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                      Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)).trans
                  ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h).trans
                    (↑(OrderIso.symm (orderIsoOfFin (disjUnion h))) : ↥(↑(disjUnion h) : Finset I) ≃ Fin (m + n))))) :
            (a : Fin (m + n)) → Fin (m + n))) :
      ExteriorAlgebra R M)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
h₁ :
  ∀ (i : Fin (m + n)),
    Fin.append
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
            (a : Fin m) → I))
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
            (a : Fin n) → I))
        i =
      Function.comp (β := Fin (m + n))
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I)
                  (disjUnion h) :
                Fin (m + n) ↪o I) :
            (a : Fin (m + n)) → I))
        (⇑(Equiv.trans (Equiv.symm finSumFinEquiv)
              ((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                    Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)).trans
                ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h).trans
                  (↑(OrderIso.symm (orderIsoOfFin (disjUnion h))) : ↥(↑(disjUnion h) : Finset I) ≃ Fin (m + n))))) :
          (a : Fin (m + n)) → Fin (m + n))
        i
⊢ Eq (α := Fin (m + n) → M)
    (Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I)))
    (Function.comp (β := Fin (m + n))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I) (disjUnion h) :
              Fin (m + n) ↪o I) :
          (a : Fin (m + n)) → I))
      (⇑(Equiv.trans (Equiv.symm finSumFinEquiv)
            ((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                  Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)).trans
              ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h).trans
                (↑(OrderIso.symm (orderIsoOfFin (disjUnion h))) : ↥(↑(disjUnion h) : Finset I) ≃ Fin (m + n))))) :
        (a : Fin (m + n)) → Fin (m + n)))

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
i : Fin (m + n)
e : Fin (m + n) ≃o ↥(↑(disjUnion h) : Finset I) := orderIsoOfFin (disjUnion h)
h₁ :
  Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))
      i =
    v
      (↑((e : (a : Fin (m + n)) → ↥(↑(disjUnion h) : Finset I))
            ((e.symm : (a : ↥(↑(disjUnion h) : Finset I)) → Fin (m + n))
                ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h :
                    (a : ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) → ↥(↑(disjUnion h) : Finset I))
                  (((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                        Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) :
                      (a : Fin m ⊕ Fin n) → ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I))
                    ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) i : Fin m ⊕ Fin n))) :
              Fin (m + n))) :
        I)
⊢ Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))
      i =
    Function.comp (β := Fin (m + n))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I (m + n)) : Type u_1)) → Fin (m + n) ↪o I) (disjUnion h) :
              Fin (m + n) ↪o I) :
          (a : Fin (m + n)) → I))
      (⇑(Equiv.trans (Equiv.symm finSumFinEquiv)
            ((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                  Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)).trans
              ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h).trans
                (↑(OrderIso.symm (orderIsoOfFin (disjUnion h))) : ↥(↑(disjUnion h) : Finset I) ≃ Fin (m + n))))) :
        (a : Fin (m + n)) → Fin (m + n))
      i

Tactic:
change _ = v (e (e.symm _))

Premises used: OrderIso.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
i : Fin (m + n)
e : Fin (m + n) ≃o ↥(↑(disjUnion h) : Finset I) := orderIsoOfFin (disjUnion h)
hi : (↑i : ℕ) < m
pos :
  (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (i.castLT hi) =
    v
      (↑((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h :
              (a : ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) → ↥(↑(disjUnion h) : Finset I))
            (((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                  Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) :
                (a : Fin m ⊕ Fin n) → ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I))
              (Sum.inl (i.castLT hi)))) :
        I)
⊢ Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))
      i =
    v
      (↑((e : (a : Fin (m + n)) → ↥(↑(disjUnion h) : Finset I))
            ((e.symm : (a : ↥(↑(disjUnion h) : Finset I)) → Fin (m + n))
                ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h :
                    (a : ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) → ↥(↑(disjUnion h) : Finset I))
                  (((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                        Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) :
                      (a : Fin m ⊕ Fin n) → ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I))
                    ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) i : Fin m ⊕ Fin n))) :
              Fin (m + n))) :
        I)

Tactic:
rw [← Fin.castAdd_castLT n i hi, Fin.append_left, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_castAdd]

Premises used: OrderIso.apply_symm_apply, Fin.castAdd_castLT, finSumFinEquiv_symm_apply_castAdd, Fin.append_left
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
i : Fin (m + n)
e : Fin (m + n) ≃o ↥(↑(disjUnion h) : Finset I) := orderIsoOfFin (disjUnion h)
hi : (↑i : ℕ) < m
⊢ (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (i.castLT hi) =
    v
      (↑((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h :
              (a : ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) → ↥(↑(disjUnion h) : Finset I))
            (((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                  Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) :
                (a : Fin m ⊕ Fin n) → ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I))
              (Sum.inl (i.castLT hi)))) :
        I)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
i : Fin (m + n)
e : Fin (m + n) ≃o ↥(↑(disjUnion h) : Finset I) := orderIsoOfFin (disjUnion h)
hi : m ≤ (↑i : ℕ)
neg :
  (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))
      (Fin.subNat m (Fin.cast ⋯ i) hi) =
    v
      (↑((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h :
              (a : ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) → ↥(↑(disjUnion h) : Finset I))
            (((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                  Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) :
                (a : Fin m ⊕ Fin n) → ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I))
              (Sum.inr (Fin.subNat m (Fin.cast ⋯ i) hi)))) :
        I)
⊢ Fin.append
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I m) : Type u_1)) → Fin m ↪o I) s : Fin m ↪o I) :
          (a : Fin m) → I))
      (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))
      i =
    v
      (↑((e : (a : Fin (m + n)) → ↥(↑(disjUnion h) : Finset I))
            ((e.symm : (a : ↥(↑(disjUnion h) : Finset I)) → Fin (m + n))
                ((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h :
                    (a : ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) → ↥(↑(disjUnion h) : Finset I))
                  (((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                        Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) :
                      (a : Fin m ⊕ Fin n) → ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I))
                    ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) i : Fin m ⊕ Fin n))) :
              Fin (m + n))) :
        I)

Tactic:
rw [← Fin.natAdd_subNat_cast hi, Fin.append_right, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_natAdd]

Premises used: OrderIso.apply_symm_apply, Fin.append_right, finSumFinEquiv_symm_apply_natAdd, Fin.natAdd_subNat_cast
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m n : ℕ
I : Type u_1
inst_3 : LinearOrder I
v : I → M
s : (↑(powersetCard I m) : Type u_1)
t : (↑(powersetCard I n) : Type u_1)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
i : Fin (m + n)
e : Fin (m + n) ≃o ↥(↑(disjUnion h) : Finset I) := orderIsoOfFin (disjUnion h)
hi : m ≤ (↑i : ℕ)
⊢ (v ∘
        (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_1)) → Fin n ↪o I) t : Fin n ↪o I) :
          (a : Fin n) → I))
      (Fin.subNat m (Fin.cast ⋯ i) hi) =
    v
      (↑((Equiv.Finset.disjUnionEquiv (↑s : Finset I) (↑t : Finset I) h :
              (a : ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) → ↥(↑(disjUnion h) : Finset I))
            (((↑(OrderIso.sumCongr (orderIsoOfFin s) (orderIsoOfFin t)) :
                  Fin m ⊕ Fin n ≃ ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I)) :
                (a : Fin m ⊕ Fin n) → ↥(↑s : Finset I) ⊕ ↥(↑t : Finset I))
              (Sum.inr (Fin.subNat m (Fin.cast ⋯ i) hi)))) :
        I)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
⊢ Nontrivial (ExteriorAlgebra R M)

Tactic:
(algebraMap_leftInverse M).injective.nontrivial

Premises used: Function.LeftInverse.injective, Function.Injective.nontrivial, ExteriorAlgebra.algebraMap_leftInverse
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ (map f).toLinearMap ∘ₗ ι R = ι R ∘ₗ f

Tactic:
CliffordAlgebra.map_comp_ι _

Premises used: ExteriorAlgebra.map, CliffordAlgebra.map_comp_ι
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
m : M
⊢ Eq (α := ExteriorAlgebra R N)
    ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) ((ι R : (a : M) → ExteriorAlgebra R M) m) :
      ExteriorAlgebra R N)
    ((ι R : (a : N) → ExteriorAlgebra R N) ((f : (a : M) → N) m) : ExteriorAlgebra R N)

Tactic:
CliffordAlgebra.map_apply_ι _ m

Premises used: CliffordAlgebra.map_apply_ι
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
rw :
  Eq (α := ExteriorAlgebra R N)
    (List.prod
      (List.map (α := ExteriorAlgebra R M) (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
        (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (m i))))
    (List.prod
      (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : N) → ExteriorAlgebra R N) (((⇑f : (a : M) → N) ∘ m) i)))
⊢ Eq (α := ExteriorAlgebra R N)
    ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
        ((ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) m) :
      ExteriorAlgebra R N)
    ((ιMulti R n : (a : Fin n → N) → ExteriorAlgebra R N) ((⇑f : (a : M) → N) ∘ m) : ExteriorAlgebra R N)

Tactic:
rw [ιMulti_apply, ιMulti_apply, map_list_prod]

Premises used: map_list_prod, ExteriorAlgebra.ιMulti_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ Eq (α := ExteriorAlgebra R N)
    (List.prod
      (List.map (α := ExteriorAlgebra R M) (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
        (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : M) → ExteriorAlgebra R M) (m i))))
    (List.prod
      (List.ofFn (n := n) fun (i : Fin n) ↦ (ι R : (a : N) → ExteriorAlgebra R N) (((⇑f : (a : M) → N) ∘ m) i)))

Tactic:
simp only [List.map_ofFn, Function.comp_def, map_apply_ι]

Premises used: List.map_ofFn, ExteriorAlgebra.map_apply_ι, Function.comp_def
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] N
H :
  ∀ (m : Fin n → M),
    Eq (α := ExteriorAlgebra R N)
      (((map f).toLinearMap.compAlternatingMap (ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R N) m :
        ExteriorAlgebra R N)
      ((AlternatingMap.compLinearMap (ιMulti R n) f : (a : Fin n → M) → ExteriorAlgebra R N) m : ExteriorAlgebra R N)
⊢ (map f).toLinearMap.compAlternatingMap (ιMulti R n) = AlternatingMap.compLinearMap (ιMulti R n) f

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ Eq (α := ExteriorAlgebra R N)
    (((map f).toLinearMap.compAlternatingMap (ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R N) m :
      ExteriorAlgebra R N)
    ((AlternatingMap.compLinearMap (ιMulti R n) f : (a : Fin n → M) → ExteriorAlgebra R N) m : ExteriorAlgebra R N)

Tactic:
map_apply_ιMulti _ _

Premises used: ExteriorAlgebra.map_apply_ιMulti, List.prod
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ Eq (α := ExteriorAlgebra R N)
    (((map f).toLinearMap.compAlternatingMap (ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R N) m :
      ExteriorAlgebra R N)
    ((AlternatingMap.compLinearMap (ιMulti R n) f : (a : Fin n → M) → ExteriorAlgebra R N) m : ExteriorAlgebra R N)

Tactic:
exact map_apply_ιMulti _ _

Premises used: ExteriorAlgebra.map_apply_ιMulti
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := ExteriorAlgebra R M →ₐ[R] ExteriorAlgebra R M) (map LinearMap.id) (AlgHom.id R (ExteriorAlgebra R M))

Tactic:
CliffordAlgebra.map_id 0

Premises used: CliffordAlgebra.map_id, ExteriorAlgebra.map, QuadraticMap.Isometry.id, OfNat.ofNat