awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin (n + 1) → G
x_1 : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ
have rw : f 0 * (partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ)) =
  f x.succ
Tactic: rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin (n + 1) → G
x_1 : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
rw :
  f 0 * (partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ)) =
    f x.succ
⊢ f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ
have rw₁ : f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ) = f x.succ
Tactic: rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin (n + 1) → G
x_1 : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
rw :
  f 0 * (partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ)) =
    f x.succ
rw₁ :
  f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ) =
    f x.succ
⊢ f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ
have rw₂ : f x.castSucc * ((f x.castSucc)⁻¹ * f x.succ) = f x.succ
Tactic: rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin (n + 1) → G
x_1 : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
rw :
  f 0 * (partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ)) =
    f x.succ
rw₁ :
  f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ) =
    f x.succ
rw₂ : f x.castSucc * ((f x.castSucc)⁻¹ * f x.succ) = f x.succ
⊢ f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ
have rw₃ : f x.succ = f x.succ
Tactic: rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin n → G
i : Fin n
⊢ (partialProd f i.castSucc)⁻¹ * partialProd f i.succ = f i
have rw : (partialProd f i.castSucc)⁻¹ * (partialProd f i.castSucc * f i) = f i
Tactic: rw [partialProd_succ, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin n → G
i : Fin n
rw : (partialProd f i.castSucc)⁻¹ * (partialProd f i.castSucc * f i) = f i
⊢ (partialProd f i.castSucc)⁻¹ * partialProd f i.succ = f i
have rw₁ : f i = f i
Tactic: rw [partialProd_succ, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a : Fin (n + 1)
⊢ partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) = partialProd g ∘ a.succ.succAbove
have h : ∀ (i : Fin (n + 1)), partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i = (partialProd g ∘ a.succ.succAbove) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i : Fin (n + 1)
⊢ partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i = (partialProd g ∘ a.succ.succAbove) i
have h : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) 0 = (partialProd g ∘ a.succ.succAbove) 0
Tactic: refine inductionOn i ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i : Fin (n + 1)
h : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) 0 = (partialProd g ∘ a.succ.succAbove) 0
⊢ partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i = (partialProd g ∘ a.succ.succAbove) i
have h₁ : ∀ (i : Fin n),
  partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = (partialProd g ∘ a.succ.succAbove) i.castSucc →
    partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.succ = (partialProd g ∘ a.succ.succAbove) i.succ
Tactic: refine inductionOn i ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi :
  partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = (partialProd g ∘ a.succ.succAbove) i.castSucc
⊢ partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.succ = (partialProd g ∘ a.succ.succAbove) i.succ
have h : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.succ = partialProd g (a.succAbove i).succ
Tactic: simp only [Function.comp_apply, succ_succAbove_succ] at *
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.succ = partialProd g (a.succAbove i).succ
have h : partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
  partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
Tactic: rw [partialProd_succ, partialProd_succ, hi]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h : ∀ (h : (↑i : ℕ) < (↑a : ℕ)),
  partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
Tactic: rcases lt_trichotomy (i : ℕ) a with (h | h | h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h :
  ∀ (h : (↑i : ℕ) < (↑a : ℕ)),
    partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
      partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h₁ : ∀ (h : (↑i : ℕ) = (↑a : ℕ)),
  partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
Tactic: rcases lt_trichotomy (i : ℕ) a with (h | h | h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h :
  ∀ (h : (↑i : ℕ) < (↑a : ℕ)),
    partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
      partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
h₁ :
  ∀ (h : (↑i : ℕ) = (↑a : ℕ)),
    partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
      partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h₂ : ∀ (h : (↑a : ℕ) < (↑i : ℕ)),
  partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
Tactic: rcases lt_trichotomy (i : ℕ) a with (h | h | h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑i : ℕ) < (↑a : ℕ)
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h₁ : i.castSucc < a
Tactic: rw [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h,
        succAbove_of_castSucc_lt]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑i : ℕ) < (↑a : ℕ)
h₁ : i.castSucc < a
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h₂ : i.castSucc.castSucc < a.succ
Tactic: rw [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h,
        succAbove_of_castSucc_lt]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑i : ℕ) < (↑a : ℕ)
⊢ i.castSucc.castSucc < a.succ
have h₁ : (↑i : ℕ) < (↑a : ℕ) + 1
Tactic: simp only [lt_def, val_castSucc, val_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑i : ℕ) = (↑a : ℕ)
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h₁ : a ≤ i.castSucc
Tactic: rw [succAbove_of_castSucc_lt, contractNth_apply_of_eq _ _ _ _ h,
        succAbove_of_le_castSucc, castSucc_succ, partialProd_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑i : ℕ) = (↑a : ℕ)
h₁ : a ≤ i.castSucc
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h₂ : i.castSucc.castSucc < a.succ
Tactic: rw [succAbove_of_castSucc_lt, contractNth_apply_of_eq _ _ _ _ h,
        succAbove_of_le_castSucc, castSucc_succ, partialProd_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑i : ℕ) = (↑a : ℕ)
⊢ a ≤ i.castSucc
have h₁ : (↑a : ℕ) ≤ (↑i : ℕ)
Tactic: simp only [castSucc_lt_succ_iff, le_def, val_castSucc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑i : ℕ) = (↑a : ℕ)
⊢ i.castSucc.castSucc < a.succ
have h₁ : (↑i : ℕ) ≤ (↑a : ℕ)
Tactic: simp only [castSucc_lt_succ_iff, le_def, val_castSucc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑a : ℕ) < (↑i : ℕ)
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h₁ : a ≤ i.castSucc
Tactic: rw [succAbove_of_le_castSucc, succAbove_of_le_castSucc, contractNth_apply_of_gt _ _ _ _ h,
        castSucc_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑a : ℕ) < (↑i : ℕ)
h₁ : a ≤ i.castSucc
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)
have h₂ : a.succ ≤ i.castSucc.castSucc
Tactic: rw [succAbove_of_le_castSucc, succAbove_of_le_castSucc, contractNth_apply_of_gt _ _ _ _ h,
        castSucc_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑a : ℕ) < (↑i : ℕ)
⊢ a ≤ i.castSucc
have h₁ : (↑a : ℕ) ≤ (↑i : ℕ)
Tactic: simp only [le_def, val_succ, val_castSucc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : (↑a : ℕ) < (↑i : ℕ)
⊢ a.succ ≤ i.castSucc.castSucc
have h₁ : (↑a : ℕ) + 1 ≤ (↑i : ℕ)
Tactic: simp only [le_def, val_succ, val_castSucc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inl : ∀ (h : (↑k : ℕ) < (↑j : ℕ)),
  (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
Tactic: rcases lt_trichotomy (k : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
inl :
  ∀ (h : (↑k : ℕ) < (↑j : ℕ)),
    (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
      j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inr : ∀ (h : (↑k : ℕ) = (↑j : ℕ)),
  (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
Tactic: rcases lt_trichotomy (k : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
inl :
  ∀ (h : (↑k : ℕ) < (↑j : ℕ)),
    (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
      j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
inr :
  ∀ (h : (↑k : ℕ) = (↑j : ℕ)),
    (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
      j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inr₁ : ∀ (h : (↑j : ℕ) < (↑k : ℕ)),
  (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
Tactic: rcases lt_trichotomy (k : ℕ) j with (h | h | h)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑k : ℕ) < (↑j : ℕ)
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inl : k.castSucc < j
Tactic: rwa [succAbove_of_castSucc_lt, succAbove_of_castSucc_lt, partialProd_right_inv,
    contractNth_apply_of_lt]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑k : ℕ) < (↑j : ℕ)
inl : k.castSucc < j
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inl₁ : k.castSucc.castSucc < j.succ
Tactic: rwa [succAbove_of_castSucc_lt, succAbove_of_castSucc_lt, partialProd_right_inv,
    contractNth_apply_of_lt]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑k : ℕ) < (↑j : ℕ)
⊢ k.castSucc.castSucc < j.succ
have inl : (↑k.castSucc : ℕ) ≤ (↑j : ℕ)
Tactic: rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑k : ℕ) = (↑j : ℕ)
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inr : j ≤ k.castSucc
Tactic: rwa [succAbove_of_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ,
    castSucc_succ, ← mul_assoc,
      partialProd_right_inv, contractNth_apply_of_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑k : ℕ) = (↑j : ℕ)
inr : j ≤ k.castSucc
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inr₁ : k.castSucc.castSucc < j.succ
Tactic: rwa [succAbove_of_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ,
    castSucc_succ, ← mul_assoc,
      partialProd_right_inv, contractNth_apply_of_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑k : ℕ) = (↑j : ℕ)
⊢ k.castSucc.castSucc < j.succ
have inr : (↑k.castSucc : ℕ) ≤ (↑j : ℕ)
Tactic: rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑k : ℕ)
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inr : j ≤ k.castSucc
Tactic: rwa [succAbove_of_le_castSucc, succAbove_of_le_castSucc, partialProd_succ, partialProd_succ,
      castSucc_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑k : ℕ)
inr : j ≤ k.castSucc
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k
have inr₁ : j.succ ≤ k.castSucc.castSucc
Tactic: rwa [succAbove_of_le_castSucc, succAbove_of_le_castSucc, partialProd_succ, partialProd_succ,
      castSucc_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑k : ℕ)
⊢ j.succ ≤ k.castSucc.castSucc
have inr : (↑j : ℕ) + 1 ≤ (↑k.castSucc.castSucc : ℕ)
Tactic: rw [le_iff_val_le_val, val_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
⊢ Fintype.card (Fin n → Fin m) = Fintype.card (Fin (m ^ n))
have simp_rw : Fintype.card (Fin m) ^ Fintype.card (Fin n) = Fintype.card (Fin (m ^ n))
Tactic: simp_rw [Fintype.card_fun, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
ih : ∀ (f : Fin n → Fin m), ∑ i : Fin n, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ n
f : Fin (n + 1) → Fin m
⊢ ∑ i : Fin (n + 1), (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ (n + 1)
have succ : ∀ (ih : ∀ (f : Fin n → Fin 0), ∑ i : Fin n, (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 n)
  (f : Fin (n + 1) → Fin 0),
  ∑ i : Fin (n + 1), (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 (n + 1)
Tactic: cases m
Cleared hypotheses: m, ih, f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
ih : ∀ (f : Fin n → Fin m), ∑ i : Fin n, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ n
f : Fin (n + 1) → Fin m
succ :
  ∀ (ih : ∀ (f : Fin n → Fin 0), ∑ i : Fin n, (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 n)
    (f : Fin (n + 1) → Fin 0),
    ∑ i : Fin (n + 1), (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 (n + 1)
⊢ ∑ i : Fin (n + 1), (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ (n + 1)
have succ₁ : ∀ (n_1 : ℕ) (ih : ∀ (f : Fin n → Fin (n_1 + 1)), ∑ i : Fin n, (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ n)
  (f : Fin (n + 1) → Fin (n_1 + 1)), ∑ i : Fin (n + 1), (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ (n + 1)
Tactic: cases m
Cleared hypotheses: m, ih, f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n n_1 : ℕ
ih : ∀ (f : Fin n → Fin (n_1 + 1)), ∑ i : Fin n, (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ n
f : Fin (n + 1) → Fin (n_1 + 1)
⊢ ∑ i : Fin (n + 1), (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ (n + 1)
have succ : ∑ x : Fin n, (↑(f x.castSucc) : ℕ) * (n_1 + 1) ^ (↑x : ℕ) + (↑(f (Fin.last n)) : ℕ) * (n_1 + 1) ^ n <
  (n_1 + 1) ^ (n + 1)
Tactic: simp_rw [Fin.sum_univ_castSucc, Fin.val_castSucc, Fin.val_last]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n n_1 : ℕ
ih : ∀ (f : Fin n → Fin (n_1 + 1)), ∑ i : Fin n, (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ n
f : Fin (n + 1) → Fin (n_1 + 1)
⊢ ∑ x : Fin n, (↑(f x.castSucc) : ℕ) * (n_1 + 1) ^ (↑x : ℕ) + (↑(f (Fin.last n)) : ℕ) * (n_1 + 1) ^ n <
    (n_1 + 1) ^ (n + 1)
have succ : (n_1 + 1) ^ n + n_1 * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
Tactic: refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _
          (Fin.is_le _)).trans_eq ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n n_1 : ℕ
ih : ∀ (f : Fin n → Fin (n_1 + 1)), ∑ i : Fin n, (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ n
f : Fin (n + 1) → Fin (n_1 + 1)
⊢ (n_1 + 1) ^ n + n_1 * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
have succ : (1 + n_1) * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
Tactic: rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n n_1 : ℕ
ih : ∀ (f : Fin n → Fin (n_1 + 1)), ∑ i : Fin n, (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ n
f : Fin (n + 1) → Fin (n_1 + 1)
succ : (1 + n_1) * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
⊢ (n_1 + 1) ^ n + n_1 * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
have succ₁ : (n_1 + 1) * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
Tactic: rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']