-- 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)
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)
⊢ 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 : ∀ (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)
Tactic: by_cases! hi : i < m