case inl
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ (partialProd g (↑(succAbove (succ j)) (↑castSucc k)))⁻¹ * partialProd g (succ (↑(succAbove j) k)) =
    contractNth j (fun x x_1 => x * x_1) g k

case inr.inl
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ (partialProd g (↑(succAbove (succ j)) (↑castSucc k)))⁻¹ * partialProd g (succ (↑(succAbove j) k)) =
    contractNth j (fun x x_1 => x * x_1) g k

case inr.inr
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ (partialProd g (↑(succAbove (succ j)) (↑castSucc k)))⁻¹ * partialProd g (succ (↑(succAbove j) k)) =
    contractNth j (fun x x_1 => x * x_1) g k
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
⊢ (partialProd g (↑(succAbove (succ j)) (↑castSucc k)))⁻¹ * partialProd g (succ (↑(succAbove j) k)) =
    contractNth j (fun x x_1 => x * x_1) g k
rcases lt_trichotomy (k : ℕ) j with (h | h | h)
case inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑castSucc k < j

case inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑castSucc (↑castSucc k) < succ j
case inl
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ (partialProd g (↑(succAbove (succ j)) (↑castSucc k)))⁻¹ * partialProd g (succ (↑(succAbove j) k)) =
    contractNth j (fun x x_1 => x * x_1) g k
rwa [succAbove_below, succAbove_below, partialProd_right_inv, contractNth_apply_of_lt]
no goals
case inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑castSucc k < j
assumption
case inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑(↑castSucc k) ≤ ↑j
case inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑castSucc (↑castSucc k) < succ j
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
no goals
case inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ ↑(↑castSucc k) ≤ ↑j
exact le_of_lt h
case inr.inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ ↑castSucc k

case inr.inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ ↑castSucc (↑castSucc k) < succ j
case inr.inl
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ (partialProd g (↑(succAbove (succ j)) (↑castSucc k)))⁻¹ * partialProd g (succ (↑(succAbove j) k)) =
    contractNth j (fun x x_1 => x * x_1) g k
rwa [succAbove_below, succAbove_above, partialProd_succ, castSucc_fin_succ, ← mul_assoc,
  partialProd_right_inv, contractNth_apply_of_eq]
no goals
case inr.inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ ↑castSucc k
simp [le_iff_val_le_val, ← h]
case inr.inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ ↑(↑castSucc k) ≤ ↑j
case inr.inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ ↑castSucc (↑castSucc k) < succ j
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
no goals
case inr.inl.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ ↑(↑castSucc k) ≤ ↑j
exact le_of_eq h
case inr.inr.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j ≤ ↑castSucc k

case inr.inr.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ succ j ≤ ↑castSucc (↑castSucc k)
case inr.inr
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ (partialProd g (↑(succAbove (succ j)) (↑castSucc k)))⁻¹ * partialProd g (succ (↑(succAbove j) k)) =
    contractNth j (fun x x_1 => x * x_1) g k
rwa [succAbove_above, succAbove_above, partialProd_succ, partialProd_succ,
  castSucc_fin_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
no goals
case inr.inr.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ j ≤ ↑castSucc k
exact le_iff_val_le_val.2 (le_of_lt h)
case inr.inr.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ ↑j + 1 ≤ ↑(↑castSucc (↑castSucc k))
case inr.inr.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ succ j ≤ ↑castSucc (↑castSucc k)
rw [le_iff_val_le_val, val_succ]
no goals
case inr.inr.h
α : Type ?u.123864
β : Type ?u.123867
inst✝¹ : Monoid α
n : ℕ
G : Type u_1
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑j < ↑k
⊢ ↑j + 1 ≤ ↑(↑castSucc (↑castSucc k))
exact Nat.succ_le_of_lt h