awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
zero₁ : Eq.{u_2 + 1} (α := M) (prod []) 1
⊢ (replicate 0 a).prod = HPow.hPow (β := ℕ) a 0
have zero₂ : Eq.{u_2 + 1} (α := M) 1 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
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ (replicate (n + 1) a).prod = a ^ (n + 1)
have succ : (a :: replicate n a).prod = a ^ (n + 1)
Tactic: rw [replicate_succ, prod_cons, ih, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
succ : (a :: replicate n a).prod = a ^ (n + 1)
⊢ (replicate (n + 1) a).prod = a ^ (n + 1)
have succ₁ : a * (replicate n a).prod = a ^ (n + 1)
Tactic: rw [replicate_succ, prod_cons, ih, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
succ : (a :: replicate n a).prod = a ^ (n + 1)
succ₁ : a * (replicate n a).prod = a ^ (n + 1)
⊢ (replicate (n + 1) a).prod = a ^ (n + 1)
have succ₂ : a * a ^ n = a ^ (n + 1)
Tactic: rw [replicate_succ, prod_cons, ih, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
succ : (a :: replicate n a).prod = a ^ (n + 1)
succ₁ : a * (replicate n a).prod = a ^ (n + 1)
succ₂ : a * a ^ n = a ^ (n + 1)
⊢ (replicate (n + 1) a).prod = a ^ (n + 1)
have succ₃ : a * a ^ n = a * a ^ n
Tactic: rw [replicate_succ, prod_cons, ih, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
a : M
⊢ (replicate n a).prod = a ^ n
have zero : (replicate 0 a).prod = HPow.hPow (β := ℕ) a 0
Tactic: induction n with
  | zero => rw [pow_zero, replicate_zero, prod_nil]
  | succ n ih => rw [replicate_succ, prod_cons, ih, pow_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
a : M
zero : (replicate 0 a).prod = HPow.hPow (β := ℕ) a 0
⊢ (replicate n a).prod = a ^ n
have succ : ∀ (n : ℕ) (ih : (replicate n a).prod = a ^ n), (replicate (n + 1) a).prod = a ^ (n + 1)
Tactic: induction n with
  | zero => rw [pow_zero, replicate_zero, prod_nil]
  | succ n ih => rw [replicate_succ, prod_cons, ih, pow_succ']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ l.prod = m ^ l.length
have rw : l.prod = (replicate l.length m).prod
Tactic: rw [← prod_replicate, ← List.eq_replicate_iff.mpr ⟨rfl, h⟩]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Defs (goal)
Goal:
M : Type u_2
inst : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
rw : l.prod = (replicate l.length m).prod
⊢ l.prod = m ^ l.length
have rw₁ : l.prod = l.prod
Tactic: rw [← prod_replicate, ← List.eq_replicate_iff.mpr ⟨rfl, h⟩]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (h :: t).prod
have simp : IsUnit (h * t.prod)
Tactic: simp only [List.prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_8
inst : CommMonoid M
L : List M
⊢ IsUnit L.prod ↔ ∀ (m : M), m ∈ L → IsUnit m
have refine : ∀ (h : IsUnit L.prod) (m : M), m ∈ L → IsUnit m
Tactic: refine ⟨fun h => ?_, prod_isUnit⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (hypothesis)
Goal:
M : Type u_8
inst : CommMonoid M
m : M
L : List M
ih : ∀ (h : IsUnit L.prod) (m : M), m ∈ L → IsUnit m
h : IsUnit (m :: L).prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1
have h₁ : IsUnit m ∧ IsUnit L.prod
Tactic: rw [prod_cons, IsUnit.mul_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_8
inst : CommMonoid M
L : List M
h : IsUnit L.prod
⊢ ∀ (m : M), m ∈ L → IsUnit m
have nil : ∀ (h : IsUnit.{u_8} (M := M) (prod [])) (m : M), Membership.mem (γ := List M) [] m → IsUnit m
Tactic: induction L with
  | nil => exact fun m' h' => False.elim (not_mem_nil h')
  | cons m L ih =>
    rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_8
inst : CommMonoid M
L : List M
h : IsUnit L.prod
nil : ∀ (h : IsUnit.{u_8} (M := M) (prod [])) (m : M), Membership.mem (γ := List M) [] m → IsUnit m
⊢ ∀ (m : M), m ∈ L → IsUnit m
have cons : ∀ (m : M) (L : List M) (ih : ∀ (h : IsUnit L.prod) (m : M), m ∈ L → IsUnit m) (h : IsUnit (m :: L).prod) (m_1 : M),
  m_1 ∈ m :: L → IsUnit m_1
Tactic: induction L with
  | nil => exact fun m' h' => False.elim (not_mem_nil h')
  | cons m L ih =>
    rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ l₁.prod = l₂.prod
have refine : ∀ (x : M), x ∈ l₁ → ∀ (y : M), y ∈ l₁ → ∀ (z : M), y * (x * z) = x * (y * z)
Tactic: refine h.foldr_eq' ?_ _
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ ∀ (x : M), x ∈ l₁ → ∀ (y : M), y ∈ l₁ → ∀ (z : M), y * (x * z) = x * (y * z)
have H : Symmetric fun (x y : M) ↦ ∀ (z : M), y * (x * z) = x * (y * z)
Tactic: apply Pairwise.forall_of_forall
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
H : Symmetric fun (x y : M) ↦ ∀ (z : M), y * (x * z) = x * (y * z)
⊢ ∀ (x : M), x ∈ l₁ → ∀ (y : M), y ∈ l₁ → ∀ (z : M), y * (x * z) = x * (y * z)
have H₁ : ∀ (x : M), x ∈ l₁ → ∀ (z : M), x * (x * z) = x * (x * z)
Tactic: apply Pairwise.forall_of_forall
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
H : Symmetric fun (x y : M) ↦ ∀ (z : M), y * (x * z) = x * (y * z)
H₁ : ∀ (x : M), x ∈ l₁ → ∀ (z : M), x * (x * z) = x * (x * z)
⊢ ∀ (x : M), x ∈ l₁ → ∀ (y : M), y ∈ l₁ → ∀ (z : M), y * (x * z) = x * (y * z)
have H₂ : Pairwise (fun (x y : M) ↦ ∀ (z : M), y * (x * z) = x * (y * z)) l₁
Tactic: apply Pairwise.forall_of_forall
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
⊢ Pairwise (fun (x y : M) ↦ ∀ (z : M), y * (x * z) = x * (y * z)) l₁
have H₂ : ∀ {a b : M}, Commute a b → ∀ (z : M), b * (a * z) = a * (b * z)
Tactic: apply hc.imp
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h_1 : l₁ ~ l₂
hc : Pairwise Commute l₁
a b : M
h : Commute a b
z : M
⊢ b * (a * z) = a * (b * z)
have H₂ : b * a * z = a * (b * z)
Tactic: rw [← mul_assoc, ← mul_assoc, h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h_1 : l₁ ~ l₂
hc : Pairwise Commute l₁
a b : M
h : Commute a b
z : M
H₂ : b * a * z = a * (b * z)
⊢ b * (a * z) = a * (b * z)
have H₃ : b * a * z = a * b * z
Tactic: rw [← mul_assoc, ← mul_assoc, h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h_1 : l₁ ~ l₂
hc : Pairwise Commute l₁
a b : M
h : Commute a b
z : M
H₂ : b * a * z = a * (b * z)
H₃ : b * a * z = a * b * z
⊢ b * (a * z) = a * (b * z)
have H₄ : b * a * z = b * a * z
Tactic: rw [← mul_assoc, ← mul_assoc, h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (hypothesis)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ ((a :: l).rotate n).prod = 1
have this : n % (a :: l).length ≤ (a :: l).length
Tactic: have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (hypothesis)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1
have hl₁ : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
Tactic: rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
Cleared hypotheses: hl, this
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ ((a :: l).rotate n).prod = 1
have rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
⊢ ((a :: l).rotate n).prod = 1
have rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
⊢ ((a :: l).rotate n).prod = 1
have rw₂ : (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
rw₂ : (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
⊢ ((a :: l).rotate n).prod = 1
have rw₃ : (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
rw₂ : (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
rw₃ : (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
⊢ ((a :: l).rotate n).prod = 1
have rw₄ : 1 * (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
rw₂ : (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
rw₃ : (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₄ : 1 * (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
⊢ ((a :: l).rotate n).prod = 1
have rw₅ : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod *
    (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
  (take (n % (a :: l).length) (a :: l)).prod
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
rw₂ : (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
rw₃ : (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₄ : 1 * (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₅ :
  (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
⊢ ((a :: l).rotate n).prod = 1
have rw₆ : (take (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod *
    (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
  (take (n % (a :: l).length) (a :: l)).prod
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
rw₂ : (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
rw₃ : (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₄ : 1 * (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₅ :
  (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
rw₆ :
  (take (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
⊢ ((a :: l).rotate n).prod = 1
have rw₇ : (take (n % (a :: l).length) (a :: l)).prod *
    ((drop (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod⁻¹) =
  (take (n % (a :: l).length) (a :: l)).prod
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
rw₂ : (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
rw₃ : (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₄ : 1 * (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₅ :
  (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
rw₆ :
  (take (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
rw₇ :
  (take (n % (a :: l).length) (a :: l)).prod *
      ((drop (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod⁻¹) =
    (take (n % (a :: l).length) (a :: l)).prod
⊢ ((a :: l).rotate n).prod = 1
have rw₈ : (take (n % (a :: l).length) (a :: l)).prod * 1 = (take (n % (a :: l).length) (a :: l)).prod
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
rw : ((a :: l).rotate (n % (a :: l).length)).prod = 1
rw₁ : (drop (n % (a :: l).length) (a :: l) ++ take (n % (a :: l).length) (a :: l)).prod = 1
rw₂ : (drop (n % (a :: l).length) (a :: l)).prod * (take (n % (a :: l).length) (a :: l)).prod = 1
rw₃ : (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₄ : 1 * (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
rw₅ :
  (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
rw₆ :
  (take (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod *
      (drop (n % (a :: l).length) (a :: l)).prod⁻¹ =
    (take (n % (a :: l).length) (a :: l)).prod
rw₇ :
  (take (n % (a :: l).length) (a :: l)).prod *
      ((drop (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod⁻¹) =
    (take (n % (a :: l).length) (a :: l)).prod
rw₈ : (take (n % (a :: l).length) (a :: l)).prod * 1 = (take (n % (a :: l).length) (a :: l)).prod
⊢ ((a :: l).rotate n).prod = 1
have rw₉ : (take (n % (a :: l).length) (a :: l)).prod = (take (n % (a :: l).length) (a :: l)).prod
Tactic: rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
⊢ sum (map (fun (x : α) ↦ count x (a :: as)) (filter p (a :: as).dedup)) = countP p (a :: as)
have cons : HAdd.hAdd (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
    (sum (map (fun (i : α) ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup))) =
  countP p as + if p a = true then 1 else 0
Tactic: simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
⊢ HAdd.hAdd (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
      (sum (map (fun (i : α) ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup))) =
    countP p as + if p a = true then 1 else 0
have cons : sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)) = countP p as
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
cons : sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)) = countP p as
⊢ HAdd.hAdd (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
      (sum (map (fun (i : α) ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup))) =
    countP p as + if p a = true then 1 else 0
have cons₁ : Eq (α := ℕ) (sum (map (fun (i : α) ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)))
  (if p a = true then 1 else 0)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
⊢ sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)) = countP p as
have cons : Eq (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
  (sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)))
Tactic: refine _root_.trans ?_ h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
    (sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)))
have pos : ∀ (ha : a ∈ as),
  Eq (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
    (sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)))
Tactic: by_cases ha : a ∈ as
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.List.Lemmas (goal)
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
pos :
  ∀ (ha : a ∈ as),
    Eq (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
      (sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)))
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
    (sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)))
have neg : ∀ (ha : ¬a ∈ as),
  Eq (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
    (sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)))
Tactic: by_cases ha : a ∈ as