awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
l : List A
f g : A → G
a : A
⊢ 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
have nil : prod (map (fun (x : A) ↦ if x = a then f x else g x) []) = (f a / g a) ^ count a [] * (map g []).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]
Cleared hypotheses: l
-- 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
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
⊢ 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
have 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
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
L : List ℕ
⊢ L.headI + L.tail.sum = L.sum
have nil : HAdd.hAdd (α := ℕ) (headI []) (sum (tail [])) = sum []
Tactic: cases L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
L : List ℕ
nil : HAdd.hAdd (α := ℕ) (headI []) (sum (tail [])) = sum []
⊢ L.headI + L.tail.sum = L.sum
have cons : ∀ (head : ℕ) (tail : List ℕ), (head :: tail).headI + (head :: tail).tail.sum = (head :: tail).sum
Tactic: cases L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
L : List ℕ
⊢ L.tail.sum = L.sum - L.headI
have rw : L.tail.sum = L.headI + L.tail.sum - L.headI
Tactic: rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
L : List ℕ
rw : L.tail.sum = L.headI + L.tail.sum - L.headI
⊢ L.tail.sum = L.sum - L.headI
have rw₁ : L.tail.sum = L.tail.sum + L.headI - L.headI
Tactic: rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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
⊢ L.tail.sum = L.sum - L.headI
have rw₂ : L.tail.sum = L.tail.sum
Tactic: rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : DivInvMonoid G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a / b * l.alternatingProd
have rw : (a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd
Tactic: rw [div_eq_mul_inv, alternatingProd_cons_cons']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : DivInvMonoid G
a b : G
l : List G
rw : (a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd
⊢ (a :: b :: l).alternatingProd = a / b * l.alternatingProd
have rw₁ : a * b⁻¹ * l.alternatingProd = a * b⁻¹ * l.alternatingProd
Tactic: rw [div_eq_mul_inv, alternatingProd_cons_cons']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
⊢ [a].alternatingProd = a * (alternatingProd [])⁻¹
have rw : [a].alternatingProd = a * 1⁻¹
Tactic: rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
rw : [a].alternatingProd = a * 1⁻¹
⊢ [a].alternatingProd = a * (alternatingProd [])⁻¹
have rw₁ : [a].alternatingProd = a * 1
Tactic: rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
rw : [a].alternatingProd = a * 1⁻¹
rw₁ : [a].alternatingProd = a * 1
⊢ [a].alternatingProd = a * (alternatingProd [])⁻¹
have rw₂ : [a].alternatingProd = a
Tactic: rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
rw : [a].alternatingProd = a * 1⁻¹
rw₁ : [a].alternatingProd = a * 1
rw₂ : [a].alternatingProd = a
⊢ [a].alternatingProd = a * (alternatingProd [])⁻¹
have rw₃ : a = a
Tactic: rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹
have rw : a * b⁻¹ * l.alternatingProd = a * (b :: l).alternatingProd⁻¹
Tactic: rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
a b : G
l : List G
rw : a * b⁻¹ * l.alternatingProd = a * (b :: l).alternatingProd⁻¹
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹
have rw₁ : a * b⁻¹ * l.alternatingProd = a * (b * l.alternatingProd⁻¹)⁻¹
Tactic: rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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⁻¹)⁻¹
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹
have rw₂ : a * b⁻¹ * l.alternatingProd = a * (b⁻¹ * l.alternatingProd⁻¹⁻¹)
Tactic: rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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⁻¹⁻¹)
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹
have rw₃ : a * b⁻¹ * l.alternatingProd = a * (b⁻¹ * l.alternatingProd)
Tactic: rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
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)
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹
have rw₄ : a * (b⁻¹ * l.alternatingProd) = a * (b⁻¹ * l.alternatingProd)
Tactic: rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
⊢ (a :: l).alternatingProd = a / l.alternatingProd
have rw : (a :: l).alternatingProd = a * l.alternatingProd⁻¹
Tactic: rw [div_eq_mul_inv, alternatingProd_cons']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
G : Type u_7
inst : CommGroup G
a : G
l : List G
rw : (a :: l).alternatingProd = a * l.alternatingProd⁻¹
⊢ (a :: l).alternatingProd = a / l.alternatingProd
have rw₁ : a * l.alternatingProd⁻¹ = a * l.alternatingProd⁻¹
Tactic: rw [div_eq_mul_inv, alternatingProd_cons']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
l : List ℕ
n : ℕ
⊢ l.sum % n = sum (map (fun (x : ℕ) ↦ x % n) l) % n
have nil : sum [] % n = sum (map (fun (x : ℕ) ↦ x % n) []) % n
Tactic: induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
l : List ℕ
n : ℕ
nil : sum [] % n = sum (map (fun (x : ℕ) ↦ x % n) []) % n
⊢ l.sum % n = sum (map (fun (x : ℕ) ↦ x % n) l) % n
have cons : ∀ (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: induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
l : List ℕ
n : ℕ
⊢ l.prod % n = prod (map (fun (x : ℕ) ↦ x % n) l) % n
have nil : prod [] % n = prod (map (fun (x : ℕ) ↦ x % n) []) % n
Tactic: induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
l : List ℕ
n : ℕ
nil : prod [] % n = prod (map (fun (x : ℕ) ↦ x % n) []) % n
⊢ l.prod % n = prod (map (fun (x : ℕ) ↦ x % n) l) % n
have cons : ∀ (a : ℕ) (l : List ℕ) (ih : l.prod % n = prod (map (fun (x : ℕ) ↦ x % n) l) % n),
  (a :: l).prod % n = prod (map (fun (x : ℕ) ↦ x % n) (a :: l)) % n
Tactic: induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
l : List ℤ
n : ℤ
⊢ l.sum % n = sum (map (fun (x : ℤ) ↦ x % n) l) % n
have nil : sum [] % n = sum (map (fun (x : ℤ) ↦ x % n) []) % n
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
l : List ℤ
n : ℤ
nil : sum [] % n = sum (map (fun (x : ℤ) ↦ x % n) []) % n
⊢ l.sum % n = sum (map (fun (x : ℤ) ↦ x % n) l) % n
have cons : ∀ (head : ℤ) (tail : List ℤ),
  tail.sum % n = sum (map (fun (x : ℤ) ↦ x % n) tail) % n →
    (head :: tail).sum % n = sum (map (fun (x : ℤ) ↦ x % n) (head :: tail)) % n
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
l : List ℤ
n : ℤ
⊢ l.prod % n = prod (map (fun (x : ℤ) ↦ x % n) l) % n
have nil : prod [] % n = prod (map (fun (x : ℤ) ↦ x % n) []) % n
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
l : List ℤ
n : ℤ
nil : prod [] % n = prod (map (fun (x : ℤ) ↦ x % n) []) % n
⊢ l.prod % n = prod (map (fun (x : ℤ) ↦ x % n) l) % n
have cons : ∀ (head : ℤ) (tail : List ℤ),
  tail.prod % n = prod (map (fun (x : ℤ) ↦ x % n) tail) % n →
    (head :: tail).prod % n = prod (map (fun (x : ℤ) ↦ x % n) (head :: tail)) % n
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
L : List (List α)
i : ℕ
⊢ take (take i (map length L)).sum L.flatten = (take i L).flatten
have nil : ∀ (i : ℕ),
  Eq.{u_2 + 1} (α := List α) (take (take i (map.{u_2, 0} (α := List α) length [])).sum (flatten []))
    (flatten (take i []))
Tactic: induction L generalizing i
Cleared hypotheses: L, i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
L : List (List α)
i : ℕ
nil :
  ∀ (i : ℕ),
    Eq.{u_2 + 1} (α := List α) (take (take i (map.{u_2, 0} (α := List α) length [])).sum (flatten []))
      (flatten (take i []))
⊢ take (take i (map length L)).sum L.flatten = (take i L).flatten
have cons : ∀ (head : List α) (tail : List (List α)),
  (∀ (i : ℕ), take (take i (map length tail)).sum tail.flatten = (take i tail).flatten) →
    ∀ (i : ℕ), take (take i (map length (head :: tail))).sum (head :: tail).flatten = (take i (head :: tail)).flatten
Tactic: induction L generalizing i
Cleared hypotheses: L, i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), take (take i (map length tail)).sum tail.flatten = (take i tail).flatten
i : ℕ
⊢ take (take i (map length (head :: tail))).sum (head :: tail).flatten = (take i (head :: tail)).flatten
have cons : take (take 0 (map length (head :: tail))).sum (head :: tail).flatten = (take 0 (head :: tail)).flatten
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), take (take i (map length tail)).sum tail.flatten = (take i tail).flatten
i : ℕ
cons : take (take 0 (map length (head :: tail))).sum (head :: tail).flatten = (take 0 (head :: tail)).flatten
⊢ take (take i (map length (head :: tail))).sum (head :: tail).flatten = (take i (head :: tail)).flatten
have cons₁ : ∀ (n : ℕ),
  take (take (n + 1) (map length (head :: tail))).sum (head :: tail).flatten = (take (n + 1) (head :: tail)).flatten
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
L : List (List α)
i : ℕ
⊢ drop (take i (map length L)).sum L.flatten = (drop i L).flatten
have nil : ∀ (i : ℕ),
  Eq.{u_2 + 1} (α := List α) (drop (take i (map.{u_2, 0} (α := List α) length [])).sum (flatten []))
    (flatten (drop i []))
Tactic: induction L generalizing i
Cleared hypotheses: L, i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
L : List (List α)
i : ℕ
nil :
  ∀ (i : ℕ),
    Eq.{u_2 + 1} (α := List α) (drop (take i (map.{u_2, 0} (α := List α) length [])).sum (flatten []))
      (flatten (drop i []))
⊢ drop (take i (map length L)).sum L.flatten = (drop i L).flatten
have cons : ∀ (head : List α) (tail : List (List α)),
  (∀ (i : ℕ), drop (take i (map length tail)).sum tail.flatten = (drop i tail).flatten) →
    ∀ (i : ℕ), drop (take i (map length (head :: tail))).sum (head :: tail).flatten = (drop i (head :: tail)).flatten
Tactic: induction L generalizing i
Cleared hypotheses: L, i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), drop (take i (map length tail)).sum tail.flatten = (drop i tail).flatten
i : ℕ
⊢ drop (take i (map length (head :: tail))).sum (head :: tail).flatten = (drop i (head :: tail)).flatten
have cons : drop (take 0 (map length (head :: tail))).sum (head :: tail).flatten = (drop 0 (head :: tail)).flatten
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
α : Type u_2
head : List α
tail : List (List α)
tail_ih : ∀ (i : ℕ), drop (take i (map length tail)).sum tail.flatten = (drop i tail).flatten
i : ℕ
cons : drop (take 0 (map length (head :: tail))).sum (head :: tail).flatten = (drop 0 (head :: tail)).flatten
⊢ drop (take i (map length (head :: tail))).sum (head :: tail).flatten = (drop i (head :: tail)).flatten
have cons₁ : ∀ (n : ℕ),
  drop (take (n + 1) (map length (head :: tail))).sum (head :: tail).flatten = (drop (n + 1) (head :: tail)).flatten
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
j : ℕ
L : List ℕ
IH : ∀ (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i), L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ (j :: L).length ≤ (j :: L).sum
have cons : 1 + L.length ≤ j + L.sum
Tactic: rw [sum_cons, length, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
⊢ L.length ≤ L.sum
have nil : ∀ (h : ∀ (i : ℕ), Membership.mem (γ := List ℕ) [] i → 1 ≤ i), length (α := ℕ) [] ≤ sum []
Tactic: induction L with
  | nil => simp
  | cons j L IH =>
    rw [sum_cons, length, add_comm]
    exact Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Basic (goal)
Goal:
L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
nil : ∀ (h : ∀ (i : ℕ), Membership.mem (γ := List ℕ) [] i → 1 ≤ i), length (α := ℕ) [] ≤ sum []
⊢ L.length ≤ L.sum
have cons : ∀ (j : ℕ) (L : List ℕ) (IH : ∀ (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i), L.length ≤ L.sum) (h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i),
  (j :: L).length ≤ (j :: L).sum
Tactic: induction L with
  | nil => simp
  | cons j L IH =>
    rw [sum_cons, length, add_comm]
    exact Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : ∀ (base : ∀ (x : M), x ∈ l → p x), p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a :: l).prod
have cons : p (a * l.prod)
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (hypothesis)
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
a : M
l : List M
ih : ∀ (base : ∀ (x : M), x ∈ l → p x), p l.prod
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a * l.prod)
have base₁ : p a ∧ ∀ (a : M), a ∈ l → p a
Tactic: simp only [mem_cons, forall_eq_or_imp] at base
Cleared hypotheses: base
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), x ∈ l → p x
⊢ p l.prod
have nil : ∀ (base : ∀ (x : M), Membership.mem (γ := List M) [] x → p x), p (prod [])
Tactic: induction l with
  | nil => simpa
  | cons a l ih =>
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih base.2)
Cleared hypotheses: base
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Mul M
inst_1 : One M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
unit : p 1
base : ∀ (x : M), x ∈ l → p x
nil : ∀ (base : ∀ (x : M), Membership.mem (γ := List M) [] x → p x), p (prod [])
⊢ p l.prod
have cons : ∀ (a : M) (l : List M) (ih : ∀ (base : ∀ (x : M), x ∈ l → p x), p l.prod) (base : ∀ (x : M), x ∈ a :: l → p x),
  p (a :: l).prod
Tactic: induction l with
  | nil => simpa
  | cons a l ih =>
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih base.2)
Cleared hypotheses: base
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
l : List ι
⊢ Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) l)) 1
have nil : Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) [])) 1
Tactic: induction l with simp [*]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : MulOneClass M
l : List ι
nil : Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) [])) 1
⊢ Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) l)) 1
have cons : ∀ (head : ι) (tail : List ι),
  Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) tail)) 1 →
    Eq.{u_2 + 1} (α := M) (prod (map (fun (x : ι) ↦ 1) (head :: tail))) 1
Tactic: induction l with simp [*]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a :: l).prod
have pos : ∀ (hl_empty : l = []), p (a :: l).prod
Tactic: by_cases hl_empty : l = []
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
pos : ∀ (hl_empty : l = []), p (a :: l).prod
⊢ p (a :: l).prod
have neg : ∀ (hl_empty : ¬l = []), p (a :: l).prod
Tactic: by_cases hl_empty : l = []
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p (a :: l).prod
have neg : p (a * l.prod)
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (hypothesis)
Goal:
M : Type u_2
inst : MulOneClass M
l_1 : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p (a * l.prod)
have base₁ : p a ∧ ∀ (a : M), a ∈ l → p a
Tactic: simp only [mem_cons, forall_eq_or_imp] at base
Cleared hypotheses: base
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : MulOneClass M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
hl : l ≠ []
base : ∀ (x : M), x ∈ l → p x
⊢ p l.prod
have nil : ∀ (hl : Ne.{u_2 + 1} (α := List M) [] []) (base : ∀ (x : M), Membership.mem (γ := List M) [] x → p x), p (prod [])
Tactic: induction l with
  | nil => simp at hl
  | cons a l ih =>
    by_cases hl_empty : l = []
    · simp [*]
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih hl_empty base.2)
Cleared hypotheses: hl, base
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : MulOneClass M
l : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
hl : l ≠ []
base : ∀ (x : M), x ∈ l → p x
nil : ∀ (hl : Ne.{u_2 + 1} (α := List M) [] []) (base : ∀ (x : M), Membership.mem (γ := List M) [] x → p x), p (prod [])
⊢ p l.prod
have cons : ∀ (a : M) (l : List M) (ih : ∀ (hl : l ≠ []) (base : ∀ (x : M), x ∈ l → p x), p l.prod) (hl : a :: l ≠ [])
  (base : ∀ (x : M), x ∈ a :: l → p x), p (a :: l).prod
Tactic: induction l with
  | nil => simp at hl
  | cons a l ih =>
    by_cases hl_empty : l = []
    · simp [*]
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih hl_empty base.2)
Cleared hypotheses: hl, base
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
⊢ (replicate 0 a).prod = HPow.hPow (β := ℕ) a 0
have zero : (replicate 0 a).prod = 1
Tactic: rw [pow_zero, replicate_zero, prod_nil]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
zero : (replicate 0 a).prod = 1
⊢ (replicate 0 a).prod = HPow.hPow (β := ℕ) a 0
have zero₁ : Eq.{u_2 + 1} (α := M) (prod []) 1
Tactic: rw [pow_zero, replicate_zero, prod_nil]