awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f g : α → M
x : α
xs : List α
hx : ¬p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun (b : α) ↦ decide (p b)) xs)).prod * (map g (filter (fun (a : α) ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun (b : α) ↦ decide (p b)) xs
          else filter (fun (b : α) ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun (a : α) ↦ decide ¬p a) xs
          else filter (fun (a : α) ↦ decide ¬p a) xs)).prod

Tactic:
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]

Premises used: List.map_cons, Bool.false_eq_true, decide_false, decide_not, mul_left_comm, decide_true, reduceIte, not_false_eq_true, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
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
⊢ 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

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]

Premises used: List.map_cons, mul_assoc, Bool.false_eq_true, not_true_eq_false, decide_false, decide_not, mul_left_comm, decide_true, List.cons, reduceIte, List.filter_cons, not_false_eq_true, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f : α → M
l : List α
rw : prod (map (fun (a : α) ↦ if p a then f a else f a) l) = (map f l).prod
⊢ (map f (filter (fun (b : α) ↦ decide (p b)) l)).prod * (map f (filter (fun (x : α) ↦ decide ¬p x) l)).prod =
    (map f l).prod

Tactic:
rw [← prod_map_ite]

Premises used: List.prod_map_ite
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
α : Type u_2
M : Type u_4
inst : CommMonoid M
p : α → Prop
inst_1 : DecidablePred p
f : α → M
l : List α
⊢ prod (map (fun (a : α) ↦ if p a then f a else f a) l) = (map f l).prod

Tactic:
simp only [ite_self]

Premises used: ite_self
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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'

Tactic:
ext_get h fun i h₁ h₂ => ?_

Premises used: List.ext_get
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
refine :
  ∀ (i : ℕ) (h₁ : i < L.length) (h₂ : i < L'.length), L.get (⟨i, h₁⟩ : Fin L.length) = L'.get (⟨i, h₂⟩ : Fin L'.length)
⊢ L = L'

Tactic:
refine ext_get h fun i h₁ h₂ => ?_

Premises used: List.ext_get
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
⊢ (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₁)
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
⊢ (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

Premises used: List.prod_take_succ, Nat.le_of_lt
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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 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₂
⊢ getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L i h₁ =
    getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) L' i h₂

Tactic:
mul_left_cancel this

Premises used: mul_left_cancel
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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 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₂
⊢ L.get (⟨i, h₁⟩ : Fin L.length) = L'.get (⟨i, h₂⟩ : Fin L'.length)

Tactic:
convert! mul_left_cancel this

Premises used: mul_left_cancel
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : Group G
⊢ Eq.{u_7 + 1} (α := G) (prod [])⁻¹ (prod (reverse (map (fun (x : G) ↦ x⁻¹) [])))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : Group G
x : G
xs : List G
⊢ (x :: xs).prod⁻¹ = prod (reverse (map (fun (x : G) ↦ x⁻¹) (x :: xs)))

Tactic:
simp [prod_append, prod_inv_reverse xs]

Premises used: List.prod_append
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : Group G
⊢ ∀ (L : List G), L.reverse.prod = (prod (map (fun (x : G) ↦ x⁻¹) L))⁻¹

Tactic:
simp [prod_inv_reverse]

Premises used: List.prod_inv_reverse
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : Group G
head : G
tail : List G
h : 0 < (head :: tail).length
⊢ (drop (HAdd.hAdd (α := ℕ) 0 1) (head :: tail)).prod =
    (getElem (valid := fun (as : List G) (i : ℕ) ↦ i < as.length) (head :: tail) 0 h)⁻¹ * (drop 0 (head :: tail)).prod

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : Group G
f : ℕ → G
⊢ prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range 0)) = f 0 / f 0

Tactic:
(div_self' (f 0)).symm

Premises used: div_self', OfNat.ofNat, Eq.symm, List.foldr, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : Group G
f : ℕ → G
⊢ prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range 0)) = f 0 / f 0

Tactic:
exact (div_self' (f 0)).symm

Premises used: div_self', OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : Group G
f : ℕ → G
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:
simp [range_succ, prod_append, map_append, h]

Premises used: List.prod_append, List.map_append, List.range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
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)
⊢ prod (map (fun (k : ℕ) ↦ f k / f (k + 1)) (range n)) = f 0 / f n

Tactic:
induction n with
  | zero => exact (div_self' (f 0)).symm
  | succ n h => simp [range_succ, prod_append, map_append, h]

Premises used: List.prod_append, div_self', List.map_append, OfNat.ofNat, Eq.symm, List.range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
K : Type u_8
inst : DivisionCommMonoid K
⊢ Eq.{u_8 + 1} (α := K) (prod [])⁻¹ (prod (map (fun (x : K) ↦ x⁻¹) []))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
K : Type u_8
inst : DivisionCommMonoid K
x : K
xs : List K
⊢ (x :: xs).prod⁻¹ = prod (map (fun (x : K) ↦ x⁻¹) (x :: xs))

Tactic:
simp [mul_comm, prod_inv xs]

Premises used: mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
h : ∀ (x : ℕ), ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) x = f x / f (x + 1)
⊢ Eq.{u_7 + 1} (α := ℕ → G) ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) fun (k : ℕ) ↦ f k / f (k + 1)

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
n : ℕ
f : ℕ → G
x : ℕ
⊢ ((fun (x : G) ↦ x⁻¹) ∘ fun (k : ℕ) ↦ f (k + 1) / f k) x = f x / f (x + 1)

Tactic:
apply inv_div

Premises used: inv_div
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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)

Tactic:
have h : ((·⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1) := by ext; apply inv_div
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
rw₅ rw₆ : f 0 / f n = f 0 / f n
⊢ 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']

Premises used: List.map_map, inv_inj, List.prod_range_div', inv_div, List.prod_inv
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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

Tactic:
(prod_set L n a).trans ?_

Premises used: List.prod_set, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
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
⊢ (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

Tactic:
refine (prod_set L n a).trans ?_

Premises used: List.prod_set, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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)
neg : ∀ (hn : ¬n < L.length), (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1
⊢ ((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:
split_ifs with hn
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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)
pos₇ 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)

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]

Premises used: List.prod_take_mul_prod_drop, mul_assoc, List.drop, mul_comm, List.prod_drop_succ, List.take, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
L : List G
n : ℕ
a : G
hn : ¬n < L.length
⊢ (take n L).prod * 1 * (drop (n + 1) L).prod = L.prod * 1

Tactic:
simp (disch := grind) [take_of_length_le, drop_eq_nil_of_le]

Premises used: List.take_of_length_le, List.drop_eq_nil_of_le
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
A : Type u_8
inst_1 : DecidableEq A
f g : A → G
a : A
⊢ prod (map (fun (x : A) ↦ if x = a then f x else g x) []) = (f a / g a) ^ count a [] * (map g []).prod

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
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)
⊢ 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

Tactic:
simp only [map_cons, prod_cons, count_cons] at ih ⊢

Premises used: List.map_cons, List.count_cons, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
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)
⊢ (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:
rw [ih]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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)
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)
⊢ (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
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
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:
simp only [hx, ite_true, pow_add, pow_one, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm,
      mul_inv_cancel_left, beq_self_eq_true]

Premises used: mul_assoc, pow_add, ite_true, mul_left_comm, div_eq_mul_inv, pow_one, mul_comm, beq_self_eq_true, mul_inv_cancel_left
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
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
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:
simp only [hx, ite_false, add_zero, mul_assoc, mul_comm (g x) _, beq_iff_eq]

Premises used: ite_false, mul_assoc, beq_iff_eq, mul_comm, add_zero
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
A : Type u_8
inst_1 : DecidableEq A
l : List A
f g : A → G
a : A
nil : prod (map (fun (x : A) ↦ if x = a then f x else g x) []) = (f a / g a) ^ count a [] * (map g []).prod
cons :
  ∀ (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
⊢ prod (map (fun (x : A) ↦ if x = a then f x else g x) l) = (f a / g a) ^ count a l * (map g l).prod

Tactic:
induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [map_cons, prod_cons, count_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : x = a
    · simp only [hx, ite_true, pow_add, pow_one, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm,
      mul_inv_cancel_left, beq_self_eq_true]
    · simp only [hx, ite_false, add_zero, mul_assoc, mul_comm (g x) _, beq_iff_eq]

Premises used: List.map_cons, ite_false, mul_assoc, beq_iff_eq, pow_add, List.count_cons, ite_true, mul_left_comm, div_eq_mul_inv, List.cons, pow_one, mul_comm, add_zero, beq_self_eq_true, mul_inv_cancel_left, List.prod_cons, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
m n : ℕ
⊢ (replicate m n).sum = m * n

Tactic:
sum_replicate m n

Premises used: List.sum_replicate
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
L : List ℕ
nil : HAdd.hAdd (α := ℕ) (headI []) (sum (tail [])) = sum []
cons : ∀ (head : ℕ) (tail : List ℕ), (head :: tail).headI + (head :: tail).tail.sum = (head :: tail).sum
⊢ L.headI + L.tail.sum = L.sum

Tactic:
cases L
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
⊢ HAdd.hAdd (α := ℕ) (headI []) (sum (tail [])) = sum []

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
head : ℕ
tail : List ℕ
⊢ (head :: tail).headI + (head :: tail).tail.sum = (head :: tail).sum

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
L : List ℕ
⊢ L.headI ≤ L.sum

Tactic:
Nat.le.intro (headI_add_tail_sum L)

Premises used: Nat.le.intro, List.headI_add_tail_sum
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
L : List ℕ
rw : L.tail.sum = L.headI + L.tail.sum - L.headI
rw₁ : L.tail.sum = L.tail.sum + L.headI - L.headI
rw₂ rw₃ : L.tail.sum = L.tail.sum
⊢ L.tail.sum = L.sum - L.headI

Tactic:
rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right, add_comm, List.headI_add_tail_sum
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : One G
inst_1 : Mul G
inst_2 : Inv G
⊢ Eq.{u_7 + 1} (α := G) (alternatingProd []) 1

Tactic:
rfl

Premises used: List.alternatingProd, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : One G
inst_1 : Mul G
inst_2 : Inv G
a : G
⊢ [a].alternatingProd = a

Tactic:
rfl

Premises used: List.alternatingProd, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : One G
inst_1 : Mul G
inst_2 : Inv G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd

Tactic:
rfl

Premises used: List.alternatingProd, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : DivInvMonoid G
a b : G
l : List G
rw : (a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd
rw₁ rw₂ : a * b⁻¹ * l.alternatingProd = a * b⁻¹ * l.alternatingProd
⊢ (a :: b :: l).alternatingProd = a / b * l.alternatingProd

Tactic:
rw [div_eq_mul_inv, alternatingProd_cons_cons']

Premises used: div_eq_mul_inv, List.alternatingProd_cons_cons'
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
a : G
rw : [a].alternatingProd = a * 1⁻¹
rw₁ : [a].alternatingProd = a * 1
rw₂ : [a].alternatingProd = a
rw₃ rw₄ : a = a
⊢ [a].alternatingProd = a * (alternatingProd [])⁻¹

Tactic:
rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]

Premises used: inv_one, List.alternatingProd_nil, mul_one, List.alternatingProd_singleton
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
a b : G
l : List G
rw : a * b⁻¹ * l.alternatingProd = a * (b :: l).alternatingProd⁻¹
rw₁ : a * b⁻¹ * l.alternatingProd = a * (b * l.alternatingProd⁻¹)⁻¹
rw₂ : a * b⁻¹ * l.alternatingProd = a * (b⁻¹ * l.alternatingProd⁻¹⁻¹)
rw₃ : a * b⁻¹ * l.alternatingProd = a * (b⁻¹ * l.alternatingProd)
rw₄ rw₅ : a * (b⁻¹ * l.alternatingProd) = a * (b⁻¹ * l.alternatingProd)
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹

Tactic:
rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]

Premises used: mul_inv, mul_assoc, List.alternatingProd_cons_cons', inv_inv
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
rw : (a :: l).alternatingProd = a * l.alternatingProd⁻¹
rw₁ rw₂ : a * l.alternatingProd⁻¹ = a * l.alternatingProd⁻¹
⊢ (a :: l).alternatingProd = a / l.alternatingProd

Tactic:
rw [div_eq_mul_inv, alternatingProd_cons']

Premises used: div_eq_mul_inv, List.alternatingProd_cons'
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
n : ℕ
⊢ sum [] % n = sum (map (fun (x : ℕ) ↦ x % n) []) % n

Tactic:
simp only [map_nil]

Premises used: List.map_nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Basic
Goal:
n a : ℕ
l : List ℕ
ih : l.sum % n = sum (map (fun (x : ℕ) ↦ x % n) l) % n
⊢ (a :: l).sum % n = sum (map (fun (x : ℕ) ↦ x % n) (a :: l)) % n

Tactic:
simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

Premises used: List.map_cons, Nat.add_mod_mod, Nat.mod_add_mod, List.sum_cons