chore: forward-port leanprover-community/mathlib#18341 and leanprover…

…-community/mathlib#18950 (#3807)

This also brings the proof of `partialProd_right_inv` in line with mathlib3.

Mathlib/Algebra/BigOperators/Fin.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Anne Baanen
 
 ! This file was ported from Lean 3 source module algebra.big_operators.fin
-! leanprover-community/mathlib commit cdb01be3c499930fd29be05dce960f4d8d201c54
+! leanprover-community/mathlib commit cc5dd6244981976cc9da7afc4eee5682b037a013
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -255,49 +255,57 @@ theorem partialProd_left_inv {G : Type _} [Group G] (f : Fin (n + 1) → G) :
 #align fin.partial_prod_left_inv Fin.partialProd_left_inv
 #align fin.partial_sum_left_neg Fin.partialSum_left_neg
 
--- Porting note:
--- 1) Changed `i` in statement to `(Fin.castLT i (Nat.lt_succ_of_lt i.2))` because of
---    coercion issues. Might need to be fixed later.
--- 2) The current proof is really bad! It should be redone once `assoc_rw` is
---    implemented and `rw` knows that `i.succ = i + 1`.
--- 3) The original Mathport output was:
---   cases' i with i hn
---   induction' i with i hi generalizing hn
---   · simp [← Fin.succ_mk, partialProd_succ]
---   · specialize hi (lt_trans (Nat.lt_succ_self i) hn)
---     simp only [mul_inv_rev, Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk, smul_eq_mul,
---       Pi.smul_apply] at hi ⊢
---     rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
---     simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
---     assoc_rw [hi, inv_mul_cancel_left]
 @[to_additive]
-theorem partialProd_right_inv {G : Type _} [Group G] (g : G) (f : Fin n → G) (i : Fin n) :
-    ((g • partialProd f) (Fin.castLT i (Nat.lt_succ_of_lt i.2)))⁻¹ *
-    (g • partialProd f) i.succ = f i := by
-  rcases i with ⟨i, hn⟩
+theorem partialProd_right_inv {G : Type _} [Group G] (f : Fin n → G) (i : Fin n) :
+    (partialProd f (Fin.castSucc i))⁻¹ * partialProd f i.succ = f i := by
+  cases' i with i hn
   induction i with
-  | zero =>
-    simp
-    change partialProd f (succ ⟨0, hn⟩) = f ⟨0, hn⟩
-    rw [partialProd_succ]
-    simp
+  | zero => simp [-Fin.succ_mk, partialProd_succ]
   | succ i hi =>
     specialize hi (lt_trans (Nat.lt_succ_self i) hn)
-    simp at hi ⊢
-    change (partialProd f (succ ⟨i, Nat.lt_of_succ_lt hn⟩))⁻¹ * g⁻¹ * (g *
-      partialProd f (succ ⟨i + 1, hn⟩)) = f ⟨Nat.succ i, hn⟩
-    rw [partialProd_succ, partialProd_succ, Fin.castSucc_mk, Fin.castSucc_mk, mul_inv_rev]
-    simp_rw [← mul_assoc] at hi ⊢
-    suffices h : (f ⟨i, Nat.lt_of_succ_lt hn⟩)⁻¹ *
-        ((partialProd f ⟨i, Nat.lt_succ_of_lt (Nat.lt_of_succ_lt hn)⟩)⁻¹ * g⁻¹ *
-        (g * partialProd f ⟨i + 1, Nat.succ_lt_succ (Nat.lt_of_succ_lt hn)⟩)) *
-        f ⟨Nat.succ i, hn⟩ = f ⟨Nat.succ i, hn⟩
-    · simp_rw[←mul_assoc] at h
-      assumption
-    · rw [mul_left_eq_self, inv_mul_eq_one, ←hi, ← mul_assoc]
+    simp only [Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk] at hi⊢
+    rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
+    rw [Nat.succ_eq_add_one] at hn
+    simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
+    -- Porting note: was
+    -- assoc_rw [hi, inv_mul_cancel_left]
+    rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, mul_left_inv]
 #align fin.partial_prod_right_inv Fin.partialProd_right_inv
 #align fin.partial_sum_right_neg Fin.partialSum_right_neg
 
+/-- Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
+Then if `k < j`, this says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ`.
+If `k = j`, it says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ₊₁ = gₖgₖ₊₁`.
+If `k > j`, it says `(g₀g₁...gₖ)⁻¹ * g₀g₁...gₖ₊₁ = gₖ₊₁.`
+Useful for defining group cohomology. -/
+@[to_additive
+      "Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
+      Then if `k < j`, this says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ) = gₖ`.
+      If `k = j`, it says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ + gₖ₊₁`.
+      If `k > j`, it says `-(g₀ + g₁ + ... + gₖ) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ₊₁.`
+      Useful for defining group cohomology."]
+theorem inv_partialProd_mul_eq_contractNth {G : Type _} [Group G] (g : Fin (n + 1) → G)
+    (j : Fin (n + 1)) (k : Fin n) :
+    (partialProd g (j.succ.succAbove (Fin.castSucc k)))⁻¹ * partialProd g (j.succAbove k).succ =
+      j.contractNth (· * ·) g k := by
+  rcases lt_trichotomy (k : ℕ) j with (h | h | h)
+  · rwa [succAbove_below, succAbove_below, partialProd_right_inv, contractNth_apply_of_lt]
+    · assumption
+    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
+      exact le_of_lt h
+  · rwa [succAbove_below, succAbove_above, partialProd_succ, castSucc_fin_succ, ← mul_assoc,
+      partialProd_right_inv, contractNth_apply_of_eq]
+    · simp [le_iff_val_le_val, ← h]
+    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
+      exact le_of_eq h
+  · rwa [succAbove_above, succAbove_above, partialProd_succ, partialProd_succ,
+      castSucc_fin_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
+    · exact le_iff_val_le_val.2 (le_of_lt h)
+    · rw [le_iff_val_le_val, val_succ]
+      exact Nat.succ_le_of_lt h
+#align fin.inv_partial_prod_mul_eq_contract_nth Fin.inv_partialProd_mul_eq_contractNth
+#align fin.neg_partial_sum_add_eq_contract_nth Fin.neg_partialSum_add_eq_contractNth
+
 end PartialProd
 
 end Fin

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Yury Kudryashov, Sébastien Gouëzel, Chris Hughes
 
 ! This file was ported from Lean 3 source module data.fin.tuple.basic
-! leanprover-community/mathlib commit d97a0c9f7a7efe6d76d652c5a6b7c9c634b70e0a
+! leanprover-community/mathlib commit ef997baa41b5c428be3fb50089a7139bf4ee886b
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -949,6 +949,44 @@ theorem mem_find_of_unique {p : Fin n → Prop} [DecidablePred p] (h : ∀ i j,
 
 end Find
 
+section ContractNth
+
+variable {α : Type _}
+
+/-- Sends `(g₀, ..., gₙ)` to `(g₀, ..., op gⱼ gⱼ₊₁, ..., gₙ)`. -/
+def contractNth (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) : α :=
+  if (k : ℕ) < j then g (Fin.castSucc k)
+  else if (k : ℕ) = j then op (g (Fin.castSucc k)) (g k.succ) else g k.succ
+#align fin.contract_nth Fin.contractNth
+
+theorem contractNth_apply_of_lt (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
+    (h : (k : ℕ) < j) : contractNth j op g k = g (Fin.castSucc k) :=
+  if_pos h
+#align fin.contract_nth_apply_of_lt Fin.contractNth_apply_of_lt
+
+theorem contractNth_apply_of_eq (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
+    (h : (k : ℕ) = j) : contractNth j op g k = op (g (Fin.castSucc k)) (g k.succ) := by
+  have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
+  rw [contractNth, if_neg this, if_pos h]
+#align fin.contract_nth_apply_of_eq Fin.contractNth_apply_of_eq
+
+theorem contractNth_apply_of_gt (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
+    (h : (j : ℕ) < k) : contractNth j op g k = g k.succ := by
+  rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]
+#align fin.contract_nth_apply_of_gt Fin.contractNth_apply_of_gt
+
+theorem contractNth_apply_of_ne (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
+    (hjk : (j : ℕ) ≠ k) : contractNth j op g k = g (j.succAbove k) := by
+  rcases lt_trichotomy (k : ℕ) j with (h | h | h)
+  · rwa [j.succAbove_below, contractNth_apply_of_lt]
+    · rwa [Fin.lt_iff_val_lt_val]
+  · exact False.elim (hjk h.symm)
+  · rwa [j.succAbove_above, contractNth_apply_of_gt]
+    · exact Fin.le_iff_val_le_val.2 (le_of_lt h)
+#align fin.contract_nth_apply_of_ne Fin.contractNth_apply_of_ne
+
+end ContractNth
+
 /-- To show two sigma pairs of tuples agree, it to show the second elements are related via
 `Fin.cast`. -/
 theorem sigma_eq_of_eq_comp_cast {α : Type _} :