awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
R : Type u_3
inst : Ring R
n : ℕ
IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)
succ : (if Even n then 0 else 1) + HPow.hPow (α := R) (-1) n = if Even n then 1 else 0
⊢ Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin (n + 1), HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even (n + 1) then 0 else 1)

Tactic:
simp only [Fin.sum_univ_castSucc, Fin.val_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]

Premises used: Nat.even_add_one, Fin.sum_univ_castSucc, ite_not, Fin.val_last, Fin.val_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
R : Type u_3
inst : Ring R
n : ℕ
IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)
pos : ∀ (h : Even n), 0 + HPow.hPow (α := R) (-1) n = 1
neg : ∀ (h : ¬Even n), 1 + HPow.hPow (α := R) (-1) n = 0
⊢ (if Even n then 0 else 1) + HPow.hPow (α := R) (-1) n = if Even n then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
R : Type u_3
inst : Ring R
n : ℕ
IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)
h : Even n
⊢ 0 + HPow.hPow (α := R) (-1) n = 1

Tactic:
simp [*]
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
R : Type u_3
inst : Ring R
n : ℕ
IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)
h : ¬Even n
⊢ 1 + HPow.hPow (α := R) (-1) n = 0

Tactic:
simp [(Nat.not_even_iff_odd.mp h).neg_pow]

Premises used: Odd.neg_pow, Nat.not_even_iff_odd, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
R : Type u_3
inst : Ring R
m : ℕ
zero : Eq.{u_3 + 1} (α := R) (∑ n : Fin 0, HPow.hPow (α := R) (-1) (↑n : ℕ)) (if Even (α := ℕ) 0 then 0 else 1)
succ :
  ∀ (n : ℕ) (IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)),
    Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin (n + 1), HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even (n + 1) then 0 else 1)
⊢ Eq.{u_3 + 1} (α := R) (∑ n : Fin m, HPow.hPow (α := R) (-1) (↑n : ℕ)) (if Even m then 0 else 1)

Tactic:
induction m with
  | zero => simp
  | succ n IH =>
    simp only [Fin.sum_univ_castSucc, Fin.val_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]
    split_ifs with h
    · simp [*]
    · simp [(Nat.not_even_iff_odd.mp h).neg_pow]

Premises used: Nat.even_add_one, Fin.sum_univ_castSucc, Fin.succ, ite_not, Fin.val_last, Fin.val_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
f : Fin n → M
⊢ partialProd f 0 = 1

Tactic:
simp [partialProd]

Premises used: Fin.partialProd
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
f : Fin n → M
j : Fin n
⊢ partialProd f j.succ = partialProd f j.castSucc * f j

Tactic:
simp [partialProd, List.take_add_one]

Premises used: Fin.partialProd, List.take_add_one
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
f : Fin (n + 1) → M
j : Fin (n + 1)
simp :
  f 0 * List.prod (List.take (↑j : ℕ) (List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ)) =
    f 0 * (List.take (↑j : ℕ) (List.ofFn (tail (α := fun (i : Fin (n + 1)) ↦ M) f))).prod
⊢ partialProd f j.succ = f 0 * partialProd (tail (α := fun (i : Fin (n + 1)) ↦ M) f) j

Tactic:
simp [partialProd]

Premises used: Fin.partialProd
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
f : Fin (n + 1) → M
j : Fin (n + 1)
⊢ f 0 * List.prod (List.take (↑j : ℕ) (List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ)) =
    f 0 * (List.take (↑j : ℕ) (List.ofFn (tail (α := fun (i : Fin (n + 1)) ↦ M) f))).prod

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
⊢ partialProd (init (α := fun (i : Fin (n + 1)) ↦ M) f) 0 = partialProd f (castSucc 0)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
f : Fin (n + 1) → M
i_1 : Fin (n + 1)
i : Fin n
hi : partialProd (init (α := fun (i : Fin (n + 1)) ↦ M) f) i.castSucc = partialProd f i.castSucc.castSucc
⊢ partialProd (init (α := fun (i : Fin (n + 1)) ↦ M) f) i.succ = partialProd f i.succ.castSucc

Tactic:
simp_all [init, partialProd_succ]

Premises used: Fin.init, Fin.partialProd_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin (n + 1) → G
x : Fin (n + 1)
⊢ HSMul.hSMul (β := (i : Fin (n + 1)) → G) (f 0) (partialProd fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) 0 = f 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin (n + 1) → G
x_1 : Fin (n + 1)
x : Fin n
hx :
  HSMul.hSMul (β := (i : Fin (n + 1)) → G) (f 0) (partialProd fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ)
      x.castSucc =
    f x.castSucc
simp : f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ
⊢ HSMul.hSMul (β := (i : Fin (n + 1)) → G) (f 0) (partialProd fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ =
    f x.succ

Tactic:
simp only [Pi.smul_apply, smul_eq_mul] at hx ⊢

Premises used: smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Algebra.BigOperators.Fin
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
rw₃ rw₄ : f x.succ = f x.succ
⊢ f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ

Tactic:
rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]

Premises used: mul_assoc, Fin.partialProd_succ, mul_inv_cancel_left
-- Module: Mathlib.Algebra.BigOperators.Fin
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
rw₁ rw₂ : f i = f i
⊢ (partialProd f i.castSucc)⁻¹ * partialProd f i.succ = f i

Tactic:
rw [partialProd_succ, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, Fin.partialProd_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
G : Type u_3
inst : Monoid G
n : ℕ
g : Fin (n + 1) → G
a : Fin (n + 1)
h :
  ∀ (i : Fin (n + 1)),
    partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i = (partialProd g ∘ a.succ.succAbove) i
⊢ partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) = partialProd g ∘ a.succ.succAbove

Tactic:
ext i
-- Module: Mathlib.Algebra.BigOperators.Fin
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

Tactic:
inductionOn i ?_ ?_

Premises used: Fin.inductionOn
-- Module: Mathlib.Algebra.BigOperators.Fin
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
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
⊢ partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i = (partialProd g ∘ a.succ.succAbove) i

Tactic:
refine inductionOn i ?_ ?_
-- Module: Mathlib.Algebra.BigOperators.Fin
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) 0 = (partialProd g ∘ a.succ.succAbove) 0

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.succ = partialProd g (a.succAbove i).succ
⊢ partialProd (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.succ = (partialProd g ∘ a.succ.succAbove) i.succ

Tactic:
simp only [Function.comp_apply, succ_succAbove_succ] at *

Premises used: Fin.succ_succAbove_succ, Function.comp_apply
-- Module: Mathlib.Algebra.BigOperators.Fin
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 :
  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 (a.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) i.succ = partialProd g (a.succAbove i).succ

Tactic:
rw [partialProd_succ, partialProd_succ, hi]

Premises used: Fin.partialProd_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
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)
⊢ 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)

Premises used: Fin.val, lt_trichotomy
-- Module: Mathlib.Algebra.BigOperators.Fin
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
h₂ : i.castSucc.castSucc < a.succ
⊢ 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 [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h,
        succAbove_of_castSucc_lt]

Premises used: Fin.succAbove_of_castSucc_lt, Fin.contractNth_apply_of_lt
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) < (↑a : ℕ)
⊢ i.castSucc < a

Tactic:
simp only [lt_def, val_castSucc, val_succ]

Premises used: Fin.val_succ, Fin.lt_def, Fin.val_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) < (↑a : ℕ) + 1
⊢ i.castSucc.castSucc < a.succ

Tactic:
simp only [lt_def, val_castSucc, val_succ]

Premises used: Fin.val_succ, Fin.lt_def, Fin.val_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) < (↑a : ℕ)

Tactic:
lia
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) < (↑a : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Algebra.BigOperators.Fin
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
h₂ : i.castSucc.castSucc < a.succ
⊢ 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 [succAbove_of_castSucc_lt, contractNth_apply_of_eq _ _ _ _ h,
        succAbove_of_le_castSucc, castSucc_succ, partialProd_succ, mul_assoc]

Premises used: Fin.succAbove_of_le_castSucc, mul_assoc, Fin.castSucc_succ, Fin.partialProd_succ, Fin.succAbove_of_castSucc_lt, Fin.contractNth_apply_of_eq
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ)
⊢ a ≤ i.castSucc

Tactic:
simp only [castSucc_lt_succ_iff, le_def, val_castSucc]

Premises used: Fin.le_def, Fin.val_castSucc, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) ≤ (↑a : ℕ)
⊢ i.castSucc.castSucc < a.succ

Tactic:
simp only [castSucc_lt_succ_iff, le_def, val_castSucc]

Premises used: Fin.le_def, Fin.val_castSucc, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ)

Tactic:
lia
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) ≤ (↑a : ℕ)

Tactic:
lia
-- Module: Mathlib.Algebra.BigOperators.Fin
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
h₂ : a.succ ≤ i.castSucc.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)

Tactic:
rw [succAbove_of_le_castSucc, succAbove_of_le_castSucc, contractNth_apply_of_gt _ _ _ _ h,
        castSucc_succ]

Premises used: Fin.succAbove_of_le_castSucc, Fin.contractNth_apply_of_gt, Fin.castSucc_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ)
⊢ a ≤ i.castSucc

Tactic:
simp only [le_def, val_succ, val_castSucc]

Premises used: Fin.le_def, Fin.val_succ, Fin.val_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) + 1 ≤ (↑i : ℕ)
⊢ a.succ ≤ i.castSucc.castSucc

Tactic:
simp only [le_def, val_succ, val_castSucc]

Premises used: Fin.le_def, Fin.val_succ, Fin.val_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ)

Tactic:
lia
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) + 1 ≤ (↑i : ℕ)

Tactic:
lia
-- Module: Mathlib.Algebra.BigOperators.Fin
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
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
⊢ (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)

Premises used: Fin.val, lt_trichotomy
-- Module: Mathlib.Algebra.BigOperators.Fin
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
inl₁ : k.castSucc.castSucc < j.succ
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k

Tactic:
rwa [succAbove_of_castSucc_lt, succAbove_of_castSucc_lt, partialProd_right_inv,
    contractNth_apply_of_lt]

Premises used: Fin.succAbove_of_castSucc_lt, Fin.partialProd_right_inv, Fin.contractNth_apply_of_lt
-- Module: Mathlib.Algebra.BigOperators.Fin
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 < j

Tactic:
assumption
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ)
⊢ k.castSucc.castSucc < j.succ

Tactic:
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]

Premises used: Fin.succ_le_succ_iff, Fin.castSucc_lt_iff_succ_le, Fin.le_iff_val_le_val
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) ≤ (↑j : ℕ)

Tactic:
le_of_lt h

Premises used: le_of_lt
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) ≤ (↑j : ℕ)

Tactic:
exact le_of_lt h

Premises used: le_of_lt
-- Module: Mathlib.Algebra.BigOperators.Fin
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
inr₁ : k.castSucc.castSucc < j.succ
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k

Tactic:
rwa [succAbove_of_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ,
    castSucc_succ, ← mul_assoc,
      partialProd_right_inv, contractNth_apply_of_eq]

Premises used: Fin.succAbove_of_le_castSucc, mul_assoc, Fin.castSucc_succ, Fin.partialProd_succ, Fin.succAbove_of_castSucc_lt, Fin.partialProd_right_inv, Fin.contractNth_apply_of_eq
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : ℕ
G : Type u_3
inst : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : (↑k : ℕ) = (↑j : ℕ)
⊢ j ≤ k.castSucc

Tactic:
simp [le_iff_val_le_val, ← h]

Premises used: Fin.le_iff_val_le_val
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : (↑k.castSucc : ℕ) ≤ (↑j : ℕ)
⊢ k.castSucc.castSucc < j.succ

Tactic:
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]

Premises used: Fin.succ_le_succ_iff, Fin.castSucc_lt_iff_succ_le, Fin.le_iff_val_le_val
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) ≤ (↑j : ℕ)

Tactic:
le_of_eq h

Premises used: le_of_eq
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) ≤ (↑j : ℕ)

Tactic:
exact le_of_eq h

Premises used: le_of_eq
-- Module: Mathlib.Algebra.BigOperators.Fin
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
inr₁ : j.succ ≤ k.castSucc.castSucc
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g k

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]

Premises used: Fin.succAbove_of_le_castSucc, inv_mul_cancel_left, Fin.contractNth_apply_of_gt, Fin.castSucc_succ, Fin.partialProd_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
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 ≤ k.castSucc

Tactic:
le_iff_val_le_val.2 (le_of_lt h)

Premises used: Iff.mpr, le_of_lt, Fin.le_iff_val_le_val
-- Module: Mathlib.Algebra.BigOperators.Fin
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 ≤ k.castSucc

Tactic:
exact le_iff_val_le_val.2 (le_of_lt h)

Premises used: Iff.mpr, le_of_lt, Fin.le_iff_val_le_val
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) + 1 ≤ (↑k.castSucc.castSucc : ℕ)
⊢ j.succ ≤ k.castSucc.castSucc

Tactic:
rw [le_iff_val_le_val, val_succ]

Premises used: Fin.val_succ, Fin.le_iff_val_le_val
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) + 1 ≤ (↑k.castSucc.castSucc : ℕ)

Tactic:
Nat.succ_le_of_lt h

Premises used: Nat.succ_le_of_lt
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) + 1 ≤ (↑k.castSucc.castSucc : ℕ)

Tactic:
exact Nat.succ_le_of_lt h

Premises used: Nat.succ_le_of_lt
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
simp_rw : Fintype.card (Fin m) ^ Fintype.card (Fin n) = Fintype.card (Fin (m ^ n))
⊢ Fintype.card (Fin n → Fin m) = Fintype.card (Fin (m ^ n))

Tactic:
simp_rw [Fintype.card_fun, Fintype.card_fin]

Premises used: Fintype.card_fin, Fintype.card_fun
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
f : Fin 0 → Fin m
⊢ ∑ i : Fin 0, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < HPow.hPow (β := ℕ) m 0

Tactic:
simp