awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
ha : ¬a ∈ as
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
    (sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)))
have neg : Eq (α := ℕ)
  (sum
    (map (fun (i : α) ↦ count i as)
      (match (motive := Bool → List α) p a with
      | true => a :: filter p as.dedup
      | false => filter p as.dedup)))
  (sum (map (fun (i : α) ↦ count i as) (filter p as.dedup)))
Tactic: simp only [dedup_cons_of_notMem ha, List.filter]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)
have cons : Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup))) (if p a = true then 1 else 0)
Tactic: simp only [beq_iff_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)
have pos : ∀ (hp : p a = true),
  Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)
Tactic: by_cases hp : p a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
pos :
  ∀ (hp : p a = true),
    Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
      (if p a = true then 1 else 0)
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)
have neg : ∀ (hp : ¬p a = true),
  Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)
Tactic: by_cases hp : p a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
hp : p a = true
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)
have pos : HSMul.hSMul (β := ℕ) (count a (filter p (a :: as).dedup)) (if a = a then 1 else 0) = if p a = true then 1 else 0
Tactic: refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
l : List α
⊢ sum (map (fun (x : α) ↦ count x l) (filter p l.dedup)) = countP p l
have nil : sum (map (fun (x : α) ↦ count x []) (filter p (dedup []))) = countP p []
Tactic: induction l with
  | nil => simp
  | cons a as h =>
    simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
    congr 1
    · refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only
    · simp only [beq_iff_eq]
      by_cases hp : p a
      · refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]
      · exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
l : List α
nil : sum (map (fun (x : α) ↦ count x []) (filter p (dedup []))) = countP p []
⊢ sum (map (fun (x : α) ↦ count x l) (filter p l.dedup)) = countP p l
have cons : ∀ (a : α) (as : List α) (h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as),
  sum (map (fun (x : α) ↦ count x (a :: as)) (filter p (a :: as).dedup)) = countP p (a :: as)
Tactic: induction l with
  | nil => simp
  | cons a as h =>
    simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
    congr 1
    · refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only
    · simp only [beq_iff_eq]
      by_cases hp : p a
      · refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]
      · exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
σ : α → Type u_8
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (l₁.sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) l₁)
have nil : (List.sigma (σ := σ) [] l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) [])
Tactic: induction l₁ with
  | nil => rfl
  | cons x l₁ IH => simp only [sigma_cons, length_append, length_map, IH, map, sum_cons]
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
σ : α → Type u_8
l₁ : List α
l₂ : (a : α) → List (σ a)
nil : (List.sigma (σ := σ) [] l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) [])
⊢ (l₁.sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) l₁)
have cons : ∀ (x : α) (l₁ : List α) (IH : (l₁.sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) l₁)),
  ((x :: l₁).sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) (x :: l₁))
Tactic: induction l₁ with
  | nil => rfl
  | cons x l₁ IH => simp only [sigma_cons, length_append, length_map, IH, map, sum_cons]
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun (x1 x2 : ℕ) ↦ x1 ≠ x2) l.ranges.flatten
have rw : Pairwise (fun (x1 x2 : ℕ) ↦ x1 ≠ x2) (range l.sum)
Tactic: rw [ranges_flatten]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
l : List ℕ
n : ℕ
⊢ (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum
have rw : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ range l.sum
Tactic: rw [← mem_range, ← ranges_flatten, mem_flatten]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
l : List ℕ
n : ℕ
rw : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ range l.sum
⊢ (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum
have rw₁ : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ l.ranges.flatten
Tactic: rw [← mem_range, ← ranges_flatten, mem_flatten]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
l : List ℕ
n : ℕ
rw : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ range l.sum
rw₁ : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ l.ranges.flatten
⊢ (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum
have rw₂ : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ ∃ (l_1 : List ℕ), l_1 ∈ l.ranges ∧ n ∈ l_1
Tactic: rw [← mem_range, ← ranges_flatten, mem_flatten]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (hypothesis)
Goal:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) =
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) L i h
have this : take i (map length L) = take i (map length (take (i + 1) L))
Tactic: have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
    simp [map_take, take_take, Nat.min_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
l : List ℤ
h : l.prod = -1
⊢ -1 ∈ l
have obtain : ∀ (x : ℤ) (h₁ : x ∈ l) (h₂ : x ≠ 1), -1 ∈ l
Tactic: obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ l.prod
have let : ∀ (s t : List M) (h : l = s ++ a :: t), a ∣ l.prod
Tactic: let ⟨s, t, h⟩ := append_of_mem ha
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ l.prod
have rw : a ∣ a * (s.prod * t.prod)
Tactic: rw [h, prod_append, prod_cons, mul_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
⊢ l₁.prod ∣ l₂.prod
have obtain : ∀ (l : List M) (hl : l₂ ~ l₁ ++ l), l₁.prod ∣ l₂.prod
Tactic: obtain ⟨l, hl⟩ := h.exists_perm_append
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₂.prod
have rw : l₁.prod ∣ l₁.prod * l.prod
Tactic: rw [hl.prod_eq, prod_append]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw : (a :: (l₁ ++ l₂)).alternatingProd =
  (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw₁ : a / (l₁ ++ l₂).alternatingProd = a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₁ :
  a / (l₁ ++ l₂).alternatingProd =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw₂ : a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
  a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₁ :
  a / (l₁ ++ l₂).alternatingProd =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₂ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw₃ : a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
  a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (l₁.length + 1)
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₁ :
  a / (l₁ ++ l₂).alternatingProd =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₂ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₃ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (l₁.length + 1)
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw₄ : a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
  a / l₁.alternatingProd * l₂.alternatingProd ^ (-1 * HPow.hPow (α := ℤ) (-1) l₁.length)
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₁ :
  a / (l₁ ++ l₂).alternatingProd =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₂ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₃ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (l₁.length + 1)
simp_rw₄ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-1 * HPow.hPow (α := ℤ) (-1) l₁.length)
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw₅ : a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
  a / l₁.alternatingProd * l₂.alternatingProd ^ (-(1 * HPow.hPow (α := ℤ) (-1) l₁.length))
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₁ :
  a / (l₁ ++ l₂).alternatingProd =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₂ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₃ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (l₁.length + 1)
simp_rw₄ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-1 * HPow.hPow (α := ℤ) (-1) l₁.length)
simp_rw₅ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-(1 * HPow.hPow (α := ℤ) (-1) l₁.length))
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw₆ : a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
  a / l₁.alternatingProd * l₂.alternatingProd ^ (-HPow.hPow (α := ℤ) (-1) l₁.length)
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₁ :
  a / (l₁ ++ l₂).alternatingProd =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₂ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₃ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (l₁.length + 1)
simp_rw₄ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-1 * HPow.hPow (α := ℤ) (-1) l₁.length)
simp_rw₅ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-(1 * HPow.hPow (α := ℤ) (-1) l₁.length))
simp_rw₆ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-HPow.hPow (α := ℤ) (-1) l₁.length)
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw₇ : a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
  a / l₁.alternatingProd * (l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length)⁻¹
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l₁ l₂ : List G
simp_rw :
  (a :: (l₁ ++ l₂)).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₁ :
  a / (l₁ ++ l₂).alternatingProd =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₂ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
simp_rw₃ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (l₁.length + 1)
simp_rw₄ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-1 * HPow.hPow (α := ℤ) (-1) l₁.length)
simp_rw₅ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-(1 * HPow.hPow (α := ℤ) (-1) l₁.length))
simp_rw₆ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-HPow.hPow (α := ℤ) (-1) l₁.length)
simp_rw₇ :
  a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
    a / l₁.alternatingProd * (l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length)⁻¹
⊢ (a :: l₁ ++ l₂).alternatingProd =
    (a :: l₁).alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) (a :: l₁).length
have simp_rw₈ : a / (l₁.alternatingProd * l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length) =
  a / l₁.alternatingProd / l₂.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l₁.length
Tactic: simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
⊢ (a :: l).reverse.alternatingProd = (a :: l).alternatingProd ^ HPow.hPow (α := ℤ) (-1) ((a :: l).length + 1)
have simp_rw : (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ * a ^ HPow.hPow (α := ℤ) (-1) l.length =
  (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
Tactic: simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
      alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
⊢ (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ * a ^ HPow.hPow (α := ℤ) (-1) l.length =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
have rw : a ^ HPow.hPow (α := ℤ) (-1) l.length * (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ =
  (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
Tactic: rw [mul_comm, ← div_eq_mul_inv, div_zpow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
rw :
  a ^ HPow.hPow (α := ℤ) (-1) l.length * (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
⊢ (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ * a ^ HPow.hPow (α := ℤ) (-1) l.length =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
have rw₁ : a ^ HPow.hPow (α := ℤ) (-1) l.length / l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length =
  (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
Tactic: rw [mul_comm, ← div_eq_mul_inv, div_zpow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
rw :
  a ^ HPow.hPow (α := ℤ) (-1) l.length * (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
rw₁ :
  a ^ HPow.hPow (α := ℤ) (-1) l.length / l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
⊢ (l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length)⁻¹ * a ^ HPow.hPow (α := ℤ) (-1) l.length =
    (a / l.alternatingProd) ^ HPow.hPow (α := ℤ) (-1) l.length
have rw₂ : a ^ HPow.hPow (α := ℤ) (-1) l.length / l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length =
  a ^ HPow.hPow (α := ℤ) (-1) l.length / l.alternatingProd ^ HPow.hPow (α := ℤ) (-1) l.length
Tactic: rw [mul_comm, ← div_eq_mul_inv, div_zpow]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod
have cons : op (x * xs.prod) = (map op (x :: xs)).reverse.prod
Tactic: rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]