feat: Add DropPair ProdP commutation lemma for one orientation

Physlib/Relativity/Tensors/Contraction/Products.lean

@@ -89,6 +89,34 @@ lemma Pure.prodP_dropPair {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
       (by rw [Fin.succSuccAbove_comm_natAdd i j])]
     simp [LinearEquiv.cast_apply]
 
+set_option backward.isDefEq.respectTransparency false in
+/-- Dropping a pair of indices in the left factor of a product of pure tensors agrees,
+  up to the canonical reindexing, with dropping the corresponding pair after taking
+  the product. -/
+lemma Pure.dropPair_prodP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
+    {c1 : Fin n1 → C}
+    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
+    (p : Pure S c) (p1 : Pure S c1) :
+    (dropPair i j hij.1 p).prodP p1 = permP _ (IsReindexing.append_succSuccAbove_castAdd i j)
+    (dropPair (Fin.castAdd n1 i) (Fin.castAdd n1 j)
+    (by simp_all [Fin.ext_iff]) (p.prodP p1)) := by
+  ext x
+  obtain ⟨x, rfl⟩ := finSumFinEquiv.surjective x
+  rw [prodP_apply_finSumFinEquiv]
+  simp only [Function.comp_apply, finSumFinEquiv_apply_left, finSumFinEquiv_apply_right, dropPair,
+    permP, Nat.add_eq, id_eq]
+  match x with
+  | Sum.inl m =>
+    simp only [finSumFinEquiv_apply_left]
+    rw [← congr_right (p.prodP p1) _ (Fin.castAdd n1 (i.succSuccAbove j m))
+      (by rw [Fin.succSuccAbove_comm_castAdd i j])]
+    simp [LinearEquiv.cast_apply]
+  | Sum.inr m =>
+    simp only [finSumFinEquiv_apply_right]
+    rw [← congr_right (p.prodP p1) _ (Fin.natAdd (n + 1 + 1) m)
+      (by rw [Fin.succSuccAbove_castAdd_apply_natAdd i j])]
+    simp [LinearEquiv.cast_apply]
+
 set_option backward.isDefEq.respectTransparency false in
 lemma Pure.prodP_contrP_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
     {c1 : Fin n1 → C}

Physlib/Relativity/Tensors/Contraction/Pure.lean

@@ -118,8 +118,6 @@ lemma dropPair_update_succSuccAbove {n : ℕ} [inst : DecidableEq (Fin (n + 1 +1
     · simp [h]
     · simp [h]
 
-TODO "Prove lemmas relating to the commutation rules of `dropPair` and `prodP`."
-
 @[simp]
 lemma dropPair_permP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
     {c1 : Fin (n1 + 1 + 1) → C} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j)

Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean

@@ -250,6 +250,20 @@ lemma succSuccAbove_comm_natAdd {n n1 : ℕ}
   simp only [succSuccAbove, val_natAdd, add_lt_add_iff_left, add_le_add_iff_left, Fin.ext_iff]
   grind
 
+lemma succSuccAbove_comm_castAdd {n n1 : ℕ}
+    (i j : Fin (n + 1 + 1)) (m : Fin n) :
+    succSuccAbove (n := n + n1) (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.castAdd n1 m)
+    = Fin.castAdd n1 (succSuccAbove i j m) := by
+  simp only [Fin.ext_iff, succSuccAbove_val, castAdd]
+  grind (splits := 20)
+
+lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ}
+    (i j : Fin (n + 1 + 1)) (m : Fin n1) :
+    succSuccAbove (n := n + n1) (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.natAdd n m)
+    = Fin.natAdd (n + 1 + 1) m := by
+  simp only [Fin.ext_iff, succSuccAbove_val, natAdd, castAdd]
+  grind (splits := 20)
+
 /-!
 
 ## predPredAbove

Physlib/Relativity/Tensors/Reindexing.lean

@@ -283,6 +283,18 @@ lemma append_succSuccAbove_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
   apply And.intro (Function.bijective_id)
   simp [forall_fin_add, succSuccAbove_comm_natAdd i j, succSuccAbove_natAdd_apply_castAdd i j]
 
+/-- Removing two entries from the left component of `Fin.append c c1` commutes with the
+  append: removing the `i`-th and `j`-th entries of `c` and then appending `c1` matches
+  removing the corresponding entries of `Fin.append c c1`, via the identity permutation.
+  This is used for the commutation of taking a *product* of tensors
+  with *contraction* of indices. -/
+lemma append_succSuccAbove_castAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
+    {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) :
+    IsReindexing (Fin.append c c1 ∘ (Fin.castAdd n1 i).succSuccAbove (Fin.castAdd n1 j))
+      (Fin.append (c ∘ i.succSuccAbove j) c1) id := by
+  apply And.intro (Function.bijective_id)
+  simp [forall_fin_add, succSuccAbove_comm_castAdd i j, succSuccAbove_castAdd_apply_natAdd i j]
+
 /-- Given a reindexing of `c` by `c1` via `σ` for which the index `i` is sent to `0`,
   removing the `i`-th entry of `c1` and the first entry of `c` yields a reindexing of
   `c ∘ Fin.succ` by `c1 ∘ i.succAbove` via the map sending `j` to the predecessor of