awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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)
⊢ (ι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)
have 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)
Tactic: rw [← AlternatingMap.map_perm, permOfDisjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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)
⊢ 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)
have 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)))
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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)
⊢ 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)))
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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)
⊢ 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
have 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)
Tactic: change _ = v (e (e.symm _))
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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)
⊢ 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)
have pos : ∀ (hi : (↑i : ℕ) < 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))
      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: by_cases! hi : i < m
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [← Fin.castAdd_castLT n i hi, Fin.append_left, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_castAdd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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 : ℕ)
⊢ 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)
have 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 sorry 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 sorry i) hi)))) :
      I)
Tactic: rw [← Fin.natAdd_subNat_cast hi, Fin.append_right, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_natAdd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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 : (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)
have 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)))
Tactic: rw [ιMulti_apply, ιMulti_apply, map_list_prod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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
⊢ (map f).toLinearMap.compAlternatingMap (ιMulti R n) = AlternatingMap.compLinearMap (ιMulti R n) f
have 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)
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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
inst_5 : Module.{u1, u2} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : Module.{u1, u4} Rᵐᵒᵖ N
inst_8 : IsCentralScalar R N
f : M →ₗ[R] N
⊢ Eq (α := ExteriorAlgebra R M →ₐ[R] TrivSqZeroExt R N) (AlgHom.comp toTrivSqZeroExt (map f))
    (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt)
have h : Eq (α := M →ₗ[R] TrivSqZeroExt R N) (AlgHom.toLinearMap (AlgHom.comp toTrivSqZeroExt (map f)) ∘ₗ ι R)
  (AlgHom.toLinearMap (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt) ∘ₗ ι R)
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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
inst_5 : Module.{u1, u2} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : Module.{u1, u4} Rᵐᵒᵖ N
inst_8 : IsCentralScalar R N
f : M →ₗ[R] N
⊢ Eq (α := M →ₗ[R] TrivSqZeroExt R N) (AlgHom.toLinearMap (AlgHom.comp toTrivSqZeroExt (map f)) ∘ₗ ι R)
    (AlgHom.toLinearMap (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt) ∘ₗ ι R)
have h : ∀ (x : M),
  Eq (α := TrivSqZeroExt R N)
    ((AlgHom.toLinearMap (AlgHom.comp toTrivSqZeroExt (map f)) ∘ₗ ι R : (a : M) → TrivSqZeroExt R N) x :
      TrivSqZeroExt R N)
    ((AlgHom.toLinearMap (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt) ∘ₗ ι R : (a : M) → TrivSqZeroExt R N) x :
      TrivSqZeroExt R N)
Tactic: apply LinearMap.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
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
this : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
have this₁ : IsCentralScalar R M
Tactic: haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (hypothesis)
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
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
this : Module.{u1, u4} Rᵐᵒᵖ N := Module.compHom N (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
have this₁ : IsCentralScalar R N
Tactic: haveI : IsCentralScalar R N := ⟨fun r m => rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
this_3 : Module.{u1, u4} Rᵐᵒᵖ N := Module.compHom N (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R N
| (TrivSqZeroExt.sndHom R N ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt) ∘ₗ (map f).toLinearMap
have rw : (f ∘ₗ TrivSqZeroExt.sndHom R M) ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt
Tactic: rw [LinearMap.comp_assoc, ← AlgHom.comp_toLinearMap, toTrivSqZeroExt_comp_map,
                AlgHom.comp_toLinearMap, ← LinearMap.comp_assoc, TrivSqZeroExt.sndHom_comp_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
this_3 : Module.{u1, u4} Rᵐᵒᵖ N := Module.compHom N (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R N
⊢ (TrivSqZeroExt.sndHom R N ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt) ∘ₗ (map f).toLinearMap =
    f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt
have conv_lhs : (f ∘ₗ TrivSqZeroExt.sndHom R M) ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt =
  f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt
Tactic: conv_lhs => rw [LinearMap.comp_assoc, ← AlgHom.comp_toLinearMap, toTrivSqZeroExt_comp_map,
                AlgHom.comp_toLinearMap, ← LinearMap.comp_assoc, TrivSqZeroExt.sndHom_comp_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.Basic (goal)
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
g : N →ₗ[R] M
⊢ LeftInverse (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
      (⇑(map g) : (a : ExteriorAlgebra R N) → ExteriorAlgebra R M)
      (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) ↔
    LeftInverse.{u2 + 1, u4 + 1} (α := M) (β := N) (⇑g : (a : N) → M) (⇑f : (a : M) → N)
have refine : ∀
  (h :
    LeftInverse (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
      (⇑(map g) : (a : ExteriorAlgebra R N) → ExteriorAlgebra R M)
      (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N))
  (x : M), (g : (a : N) → M) ((f : (a : M) → N) x : N) = x
Tactic: refine ⟨fun h x => ?_, fun h => CliffordAlgebra.leftInverse_map_of_leftInverse _ _ h⟩