awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
i : M
l : List M
hil : ∀ (hl : ∀ (x : M), x ∈ l → x = 1), l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
⊢ (i :: l).prod = 1
have cons : i * l.prod = 1
Tactic: rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
i : M
l : List M
hil : ∀ (hl : ∀ (x : M), x ∈ l → x = 1), l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
cons : i * l.prod = 1
⊢ (i :: l).prod = 1
have cons₁ : i * 1 = 1
Tactic: rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
i : M
l : List M
hil : ∀ (hl : ∀ (x : M), x ∈ l → x = 1), l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
cons : i * l.prod = 1
cons₁ : i * 1 = 1
⊢ (i :: l).prod = 1
have cons₂ : HMul.hMul (α := M) 1 1 = 1
Tactic: rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
i : M
l : List M
hil : ∀ (hl : ∀ (x : M), x ∈ l → x = 1), l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
cons : i * l.prod = 1
cons₁ : i * 1 = 1
cons₂ : HMul.hMul (α := M) 1 1 = 1
⊢ (i :: l).prod = 1
have cons₃ : Eq.{u_4 + 1} (α := M) 1 1
Tactic: rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
hl : ∀ (x : M), x ∈ l → x = 1
⊢ l.prod = 1
have nil : ∀ (hl : ∀ (x : M), Membership.mem (γ := List M) [] x → x = 1), Eq.{u_4 + 1} (α := M) (prod []) 1
Tactic: induction l with
  | nil => rfl
  | cons i l hil =>
    rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
hl : ∀ (x : M), x ∈ l → x = 1
nil : ∀ (hl : ∀ (x : M), Membership.mem (γ := List M) [] x → x = 1), Eq.{u_4 + 1} (α := M) (prod []) 1
⊢ l.prod = 1
have cons : ∀ (i : M) (l : List M) (hil : ∀ (hl : ∀ (x : M), x ∈ l → x = 1), l.prod = 1) (hl : ∀ (x : M), x ∈ i :: l → x = 1),
  (i :: l).prod = 1
Tactic: induction l with
  | nil => rfl
  | cons i l hil =>
    rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons : ∀ (ha : a ∈ a :: l) (comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x),
  a * ((a :: l).erase a).prod = (a :: l).prod
Tactic: obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
Cleared hypotheses: b, ha, comm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
cons :
  ∀ (ha : a ∈ a :: l) (comm : ∀ (x : M), x ∈ a :: l → ∀ (y : M), y ∈ a :: l → x * y = y * x),
    a * ((a :: l).erase a).prod = (a :: l).prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons₁ : ∀ (ne : a ≠ b) (h : a ∈ l), a * ((b :: l).erase a).prod = (b :: l).prod
Tactic: obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons : a *
    prod
      (match (motive := Bool → List M) b == a with
      | true => l
      | false => b :: l.erase a) =
  (b :: l).prod
Tactic: rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
cons :
  a *
      prod
        (match (motive := Bool → List M) b == a with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons₁ : a *
    prod
      (match (motive := Bool → List M) false with
      | true => l
      | false => b :: l.erase a) =
  (b :: l).prod
Tactic: rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
cons :
  a *
      prod
        (match (motive := Bool → List M) b == a with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₁ :
  a *
      prod
        (match (motive := Bool → List M) false with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons₂ : a * (b * (l.erase a).prod) = (b :: l).prod
Tactic: rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
cons :
  a *
      prod
        (match (motive := Bool → List M) b == a with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₁ :
  a *
      prod
        (match (motive := Bool → List M) false with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₂ : a * (b * (l.erase a).prod) = (b :: l).prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons₃ : a * (b * (l.erase a).prod) = b * l.prod
Tactic: rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
cons :
  a *
      prod
        (match (motive := Bool → List M) b == a with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₁ :
  a *
      prod
        (match (motive := Bool → List M) false with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₂ : a * (b * (l.erase a).prod) = (b :: l).prod
cons₃ : a * (b * (l.erase a).prod) = b * l.prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons₄ : a * b * (l.erase a).prod = b * l.prod
Tactic: rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
cons :
  a *
      prod
        (match (motive := Bool → List M) b == a with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₁ :
  a *
      prod
        (match (motive := Bool → List M) false with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₂ : a * (b * (l.erase a).prod) = (b :: l).prod
cons₃ : a * (b * (l.erase a).prod) = b * l.prod
cons₄ : a * b * (l.erase a).prod = b * l.prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons₅ : b * a * (l.erase a).prod = b * l.prod
Tactic: rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
cons :
  a *
      prod
        (match (motive := Bool → List M) b == a with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₁ :
  a *
      prod
        (match (motive := Bool → List M) false with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₂ : a * (b * (l.erase a).prod) = (b :: l).prod
cons₃ : a * (b * (l.erase a).prod) = b * l.prod
cons₄ : a * b * (l.erase a).prod = b * l.prod
cons₅ : b * a * (l.erase a).prod = b * l.prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons₆ : b * (a * (l.erase a).prod) = b * l.prod
Tactic: rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l_1 : List M
a : M
inst_1 : DecidableEq M
b : M
l : List M
ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
cons :
  a *
      prod
        (match (motive := Bool → List M) b == a with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₁ :
  a *
      prod
        (match (motive := Bool → List M) false with
        | true => l
        | false => b :: l.erase a) =
    (b :: l).prod
cons₂ : a * (b * (l.erase a).prod) = (b :: l).prod
cons₃ : a * (b * (l.erase a).prod) = b * l.prod
cons₄ : a * b * (l.erase a).prod = b * l.prod
cons₅ : b * a * (l.erase a).prod = b * l.prod
cons₆ : b * (a * (l.erase a).prod) = b * l.prod
⊢ a * ((b :: l).erase a).prod = (b :: l).prod
have cons₇ : b * l.prod = b * l.prod
Tactic: rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
a : M
inst_1 : DecidableEq M
ha : a ∈ l
comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x
⊢ a * (l.erase a).prod = l.prod
have nil : ∀ (ha : Membership.mem (γ := List M) [] a)
  (comm : ∀ (x : M), Membership.mem (γ := List M) [] x → ∀ (y : M), Membership.mem (γ := List M) [] y → x * y = y * x),
  a * (List.erase [] a).prod = prod []
Tactic: induction l with
  | nil => simp only [not_mem_nil] at ha
  | cons b l ih =>
    obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
    · simp only [erase_cons_head, prod_cons]
    rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
Cleared hypotheses: ha, comm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
a : M
inst_1 : DecidableEq M
ha : a ∈ l
comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x
nil :
  ∀ (ha : Membership.mem (γ := List M) [] a)
    (comm :
      ∀ (x : M), Membership.mem (γ := List M) [] x → ∀ (y : M), Membership.mem (γ := List M) [] y → x * y = y * x),
    a * (List.erase [] a).prod = prod []
⊢ a * (l.erase a).prod = l.prod
have cons : ∀ (b : M) (l : List M)
  (ih : ∀ (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x), a * (l.erase a).prod = l.prod)
  (ha : a ∈ b :: l) (comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x),
  a * ((b :: l).erase a).prod = (b :: l).prod
Tactic: induction l with
  | nil => simp only [not_mem_nil] at ha
  | cons b l ih =>
    obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
    · simp only [erase_cons_head, prod_cons]
    rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]
Cleared hypotheses: ha, comm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → Membership.mem (γ := List α) [] a' → f a' = 1
⊢ (map f []).prod = f a ^ count a []
have nil : prod [] = f a ^ count a []
Tactic: rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → Membership.mem (γ := List α) [] a' → f a' = 1
nil : prod [] = f a ^ count a []
⊢ (map f []).prod = f a ^ count a []
have nil₁ : 1 = f a ^ count a []
Tactic: rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → Membership.mem (γ := List α) [] a' → f a' = 1
nil : prod [] = f a ^ count a []
nil₁ : 1 = f a ^ count a []
⊢ (map f []).prod = f a ^ count a []
have nil₂ : 1 = HPow.hPow (β := ℕ) (f a) 0
Tactic: rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a : α
hf : ∀ (a' : α), a' ≠ a → Membership.mem (γ := List α) [] a' → f a' = 1
nil : prod [] = f a ^ count a []
nil₁ : 1 = f a ^ count a []
nil₂ : 1 = HPow.hPow (β := ℕ) (f a) 0
⊢ (map f []).prod = f a ^ count a []
have nil₃ : Eq.{u_4 + 1} (α := M) 1 1
Tactic: rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (hypothesis)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
h : ∀ (a : α) (hf : ∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1), (map f as).prod = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)
have h₁ : (map f as).prod = f a ^ count a as
Tactic: specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)
have cons : f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)
Tactic: rw [List.map_cons, List.prod_cons, count_cons, h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ (count a as + if (a' == a) = true then 1 else 0)
have cons : f a' * f a ^ count a as = f a ^ (count a as + if a' = a then 1 else 0)
Tactic: simp only [beq_iff_eq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
⊢ f a' * f a ^ count a as = f a ^ (count a as + if a' = a then 1 else 0)
have pos : ∀ (ha' : a' = a), f a' * f a ^ count a as = f a ^ (count a as + 1)
Tactic: split_ifs with ha'
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
pos : ∀ (ha' : a' = a), f a' * f a ^ count a as = f a ^ (count a as + 1)
⊢ f a' * f a ^ count a as = f a ^ (count a as + if a' = a then 1 else 0)
have neg : ∀ (ha' : ¬a' = a), f a' * f a ^ count a as = f a ^ (count a as + 0)
Tactic: split_ifs with ha'
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)
have pos : f a * f a ^ count a as = f a ^ (count a as + 1)
Tactic: rw [ha', _root_.pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : a' = a
pos : f a * f a ^ count a as = f a ^ (count a as + 1)
⊢ f a' * f a ^ count a as = f a ^ (count a as + 1)
have pos₁ : f a * f a ^ count a as = f a * f a ^ count a as
Tactic: rw [ha', _root_.pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)
have neg : 1 * f a ^ count a as = f a ^ (count a as + 0)
Tactic: rw [hf a' ha' mem_cons_self, one_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : ¬a' = a
neg : 1 * f a ^ count a as = f a ^ (count a as + 0)
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)
have neg₁ : f a ^ count a as = f a ^ (count a as + 0)
Tactic: rw [hf a' ha' mem_cons_self, one_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
f : α → M
a' : α
as : List α
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
h : (map f as).prod = f a ^ count a as
ha' : ¬a' = a
neg : 1 * f a ^ count a as = f a ^ (count a as + 0)
neg₁ : f a ^ count a as = f a ^ (count a as + 0)
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)
have neg₂ : f a ^ count a as = f a ^ count a as
Tactic: rw [hf a' ha' mem_cons_self, one_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
l : List α
a : α
f : α → M
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
⊢ (map f l).prod = f a ^ count a l
have nil : ∀ (a : α) (hf : ∀ (a' : α), a' ≠ a → Membership.mem (γ := List α) [] a' → f a' = 1), (map f []).prod = f a ^ count a []
Tactic: induction l generalizing a with
  | nil => rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
  | cons a' as h =>
    specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
    rw [List.map_cons, List.prod_cons, count_cons, h]
    simp only [beq_iff_eq]
    split_ifs with ha'
    · rw [ha', _root_.pow_succ']
    · rw [hf a' ha' mem_cons_self, one_mul, add_zero]
Cleared hypotheses: l, a, hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
M : Type u_4
inst : Monoid M
inst_1 : DecidableEq α
l : List α
a : α
f : α → M
hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1
nil :
  ∀ (a : α) (hf : ∀ (a' : α), a' ≠ a → Membership.mem (γ := List α) [] a' → f a' = 1),
    (map f []).prod = f a ^ count a []
⊢ (map f l).prod = f a ^ count a l
have cons : ∀ (a' : α) (as : List α)
  (h : ∀ (a : α) (hf : ∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1), (map f as).prod = f a ^ count a as) (a : α)
  (hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1), (map f (a' :: as)).prod = f a ^ count a (a' :: as)
Tactic: induction l generalizing a with
  | nil => rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
  | cons a' as h =>
    specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
    rw [List.map_cons, List.prod_cons, count_cons, h]
    simp only [beq_iff_eq]
    split_ifs with ha'
    · rw [ha', _root_.pow_succ']
    · rw [hf a' ha' mem_cons_self, one_mul, add_zero]
Cleared hypotheses: l, a, hf
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
inst_1 : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1
⊢ l.prod = (map id l).prod
have rw : l.prod = l.prod
Tactic: rw [map_id]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
M : Type u_4
inst : Monoid M
l : List M
a : M
i : ℕ
hlen : i ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute a a'
⊢ (l.insertIdx i a).prod = a * l.prod
have induction : ∀ {l : List M} (hlen : 0 ≤ l.length) (hcomm : ∀ (a' : M), a' ∈ take 0 l → Commute a a'),
  (l.insertIdx 0 a).prod = a * l.prod
Tactic: induction i generalizing l
Cleared hypotheses: l, i, hlen, hcomm