awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
l : List α
nil :
  prod (map (fun (a : α) ↦ if p a then f a else g a) []) =
    (map f (filter (fun (b : α) ↦ decide (p b)) [])).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) [])).prod
⊢ prod (map (fun (a : α) ↦ if p a then f a else g a) l) =
    (map f (filter (fun (b : α) ↦ decide (p b)) l)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) l)).prod
have cons : ∀ (x : α) (xs : List α)
  (ih :
    prod (map (fun (a : α) ↦ if p a then f a else g a) xs) =
      (map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod),
  prod (map (fun (a : α) ↦ if p a then f a else g a) (x :: xs)) =
    (map f (filter (fun (b : α) ↦ decide (p b)) (x :: xs))).prod *
      (map g (filter (fun (a : α) ↦ decide ¬p a) (x :: xs))).prod
Tactic: induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [map_cons, filter_cons, prod_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : p x
    · simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
        decide_false, Bool.false_eq_true, mul_assoc]
    · simp only [hx, ↓reduceIte, decide_not, decide_false, Bool.false_eq_true, not_false_eq_true,
      decide_true, map_cons, prod_cons, mul_left_comm]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f : α → M
l : List α
⊢ (map f (filter (fun (b : α) ↦ decide (p b)) l)).prod * (map f (filter (fun (x : α) ↦ decide ¬p x) l)).prod =
    (map f l).prod
have rw : prod (map (fun (a : α) ↦ if p a then f a else f a) l) = (map f l).prod
Tactic: rw [← prod_map_ite]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
⊢ L = L'
have refine : ∀ (i : ℕ) (h₁ : i < L.length) (h₂ : i < L'.length), L.get (⟨i, h₁⟩ : Fin L.length) = L'.get (⟨i, h₂⟩ : Fin L'.length)
Tactic: refine ext_get h fun i h₁ h₂ => ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (hypothesis)
Goal:
M : Type u_4
inst : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
⊢ L.get (⟨i, h₁⟩ : Fin L.length) = L'.get (⟨i, h₂⟩ : Fin L'.length)
have this : (take (i + 1) L).prod = (take (i + 1) L').prod
Tactic: have : (L.take (i + 1)).prod = (L'.take (i + 1)).prod := h' _ (Nat.succ_le_of_lt h₁)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (hypothesis)
Goal:
M : Type u_4
inst : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take (i + 1) L).prod = (take (i + 1) L').prod
⊢ L.get (⟨i, h₁⟩ : Fin L.length) = L'.get (⟨i, h₂⟩ : Fin L'.length)
have this₁ : (take i L').prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i h₁ =
  (take i L').prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L' i h₂
Tactic: rw [prod_take_succ L i h₁, prod_take_succ L' i h₂, h' i (Nat.le_of_lt h₁)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : Group G
n : ℕ
f : ℕ → G
⊢ prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range n)) = f 0 / f n
have zero : prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range 0)) = f 0 / f 0
Tactic: induction n with
  | zero => exact (div_self' (f 0)).symm
  | succ n h => simp [range_succ, prod_append, map_append, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : Group G
n : ℕ
f : ℕ → G
zero : prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range 0)) = f 0 / f 0
⊢ prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range n)) = f 0 / f n
have succ : ∀ (n : ℕ) (h : prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range n)) = f 0 / f n),
  prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range (n + 1))) = f 0 / f (n + 1)
Tactic: induction n with
  | zero => exact (div_self' (f 0)).symm
  | succ n h => simp [range_succ, prod_append, map_append, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
⊢ Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)
have h : ∀ (x : ℕ), ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) x = f x / f (x + 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (hypothesis)
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
⊢ prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f n / f 0
have h : Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)
Tactic: have h : ((·⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1) := by ext; apply inv_div
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
h : Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)
⊢ prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f n / f 0
have rw : (prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)))⁻¹ = (f n / f 0)⁻¹
Tactic: rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
h : Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)
rw : (prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)))⁻¹ = (f n / f 0)⁻¹
⊢ prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f n / f 0
have rw₁ : prod (map (fun (x : G) ↦ x⁻¹) (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n))) = (f n / f 0)⁻¹
Tactic: rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
h : Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)
rw : (prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)))⁻¹ = (f n / f 0)⁻¹
rw₁ : prod (map (fun (x : G) ↦ x⁻¹) (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n))) = (f n / f 0)⁻¹
⊢ prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f n / f 0
have rw₂ : prod (map ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = (f n / f 0)⁻¹
Tactic: rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
h : Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)
rw : (prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)))⁻¹ = (f n / f 0)⁻¹
rw₁ : prod (map (fun (x : G) ↦ x⁻¹) (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n))) = (f n / f 0)⁻¹
rw₂ : prod (map ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = (f n / f 0)⁻¹
⊢ prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f n / f 0
have rw₃ : prod (map ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f 0 / f n
Tactic: rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
h : Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)
rw : (prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)))⁻¹ = (f n / f 0)⁻¹
rw₁ : prod (map (fun (x : G) ↦ x⁻¹) (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n))) = (f n / f 0)⁻¹
rw₂ : prod (map ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = (f n / f 0)⁻¹
rw₃ : prod (map ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f 0 / f n
⊢ prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f n / f 0
have rw₄ : prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range n)) = f 0 / f n
Tactic: rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
h : Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)
rw : (prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)))⁻¹ = (f n / f 0)⁻¹
rw₁ : prod (map (fun (x : G) ↦ x⁻¹) (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n))) = (f n / f 0)⁻¹
rw₂ : prod (map ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = (f n / f 0)⁻¹
rw₃ : prod (map ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f 0 / f n
rw₄ : prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range n)) = f 0 / f n
⊢ prod (map (fun (k : ℕ) ↦ f (k + 1) / f k) (range n)) = f n / f 0
have rw₅ : f 0 / f n = f 0 / f n
Tactic: rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
⊢ (L.set n a).prod =
    L.prod *
      if hn : n < L.length then (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a else 1
have refine : ((take n L).prod * if n < L.length then a else 1) * (drop (n + 1) L).prod =
  L.prod * if hn : n < L.length then (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a else 1
Tactic: refine (prod_set L n a).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
⊢ ((take n L).prod * if n < L.length then a else 1) * (drop (n + 1) L).prod =
    L.prod *
      if hn : n < L.length then (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a else 1
have pos : ∀ (hn : n < L.length),
  (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
pos :
  ∀ (hn : n < L.length),
    (take n L).prod * a * (drop (n + 1) L).prod =
      L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
⊢ ((take n L).prod * if n < L.length then a else 1) * (drop (n + 1) L).prod =
    L.prod *
      if hn : n < L.length then (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a else 1
have neg : ∀ (hn : ¬n < L.length), (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
⊢ (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
have pos : a * (take n L).prod * (drop (n + 1) L).prod =
  L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
pos :
  a * (take n L).prod * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
⊢ (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
have pos₁ : a * ((take n L).prod * (drop (n + 1) L).prod) =
  L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
pos :
  a * (take n L).prod * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₁ :
  a * ((take n L).prod * (drop (n + 1) L).prod) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
⊢ (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
have pos₂ : a * ((take n L).prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * (drop n L).prod)) =
  L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
pos :
  a * (take n L).prod * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₁ :
  a * ((take n L).prod * (drop (n + 1) L).prod) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₂ :
  a * ((take n L).prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * (drop n L).prod)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
⊢ (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
have pos₃ : a * ((take n L).prod * ((drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹)) =
  L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
pos :
  a * (take n L).prod * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₁ :
  a * ((take n L).prod * (drop (n + 1) L).prod) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₂ :
  a * ((take n L).prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * (drop n L).prod)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₃ :
  a * ((take n L).prod * ((drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
⊢ (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
have pos₄ : a * ((take n L).prod * (drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹) =
  L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
pos :
  a * (take n L).prod * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₁ :
  a * ((take n L).prod * (drop (n + 1) L).prod) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₂ :
  a * ((take n L).prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * (drop n L).prod)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₃ :
  a * ((take n L).prod * ((drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₄ :
  a * ((take n L).prod * (drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
⊢ (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
have pos₅ : a * (L.prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹) =
  L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
pos :
  a * (take n L).prod * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₁ :
  a * ((take n L).prod * (drop (n + 1) L).prod) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₂ :
  a * ((take n L).prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * (drop n L).prod)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₃ :
  a * ((take n L).prod * ((drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₄ :
  a * ((take n L).prod * (drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₅ :
  a * (L.prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
⊢ (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
have pos₆ : L.prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a =
  L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : n < L.length
pos :
  a * (take n L).prod * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₁ :
  a * ((take n L).prod * (drop (n + 1) L).prod) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₂ :
  a * ((take n L).prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * (drop n L).prod)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₃ :
  a * ((take n L).prod * ((drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹)) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₄ :
  a * ((take n L).prod * (drop n L).prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₅ :
  a * (L.prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹) =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
pos₆ :
  L.prod * (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
⊢ (take n L).prod * a * (drop (n + 1) L).prod =
    L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
have pos₇ : L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a) =
  L.prod * ((getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) L n hn)⁻¹ * a)
Tactic: rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
A : Type u_8
inst_1 : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : prod (map (fun (x : A) ↦ if x = a then f x else g x) xs) = (f a / g a) ^ count a xs * (map g xs).prod
⊢ prod (map (fun (x : A) ↦ if x = a then f x else g x) (x :: xs)) =
    (f a / g a) ^ count a (x :: xs) * (map g (x :: xs)).prod
have cons : (if x = a then f x else g x) * prod (map (fun (x : A) ↦ if x = a then f x else g x) xs) =
  (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Tactic: simp only [map_cons, prod_cons, count_cons] at ih ⊢
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
A : Type u_8
inst_1 : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : prod (map (fun (x : A) ↦ if x = a then f x else g x) xs) = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * prod (map (fun (x : A) ↦ if x = a then f x else g x) xs) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
have cons : (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
  (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
A : Type u_8
inst_1 : DecidableEq A
f g : A → G
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
have pos : ∀ (hx : x = a),
  (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Tactic: by_cases hx : x = a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
A : Type u_8
inst_1 : DecidableEq A
f g : A → G
a x : A
xs : List A
pos :
  ∀ (hx : x = a),
    (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
      (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
have neg : ∀ (hx : ¬x = a),
  (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Tactic: by_cases hx : x = a