awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
refine : ∀ (x : M), x ∈ l₁ → ∀ (y : M), y ∈ l₁ → ∀ (z : M), y * (x * z) = x * (y * z)
⊢ l₁.prod = l₂.prod

Tactic:
refine h.foldr_eq' ?_ _

Premises used: List.Perm.foldr_eq'
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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)
H₂ : Pairwise (fun (x y : M) ↦ ∀ (z : M), y * (x * z) = x * (y * z)) l₁
⊢ ∀ (x : M), x ∈ l₁ → ∀ (y : M), y ∈ l₁ → ∀ (z : M), y * (x * z) = x * (y * z)

Tactic:
apply Pairwise.forall_of_forall

Premises used: List.Pairwise.forall_of_forall
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h_1 : l₁ ~ l₂
hc : Pairwise Commute l₁
x y : M
h : ∀ (z : M), y * (x * z) = x * (y * z)
z : M
⊢ x * (y * z) = y * (x * z)

Tactic:
(h z).symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h_1 : l₁ ~ l₂
hc : Pairwise Commute l₁
x y : M
h : ∀ (z : M), y * (x * z) = x * (y * z)
z : M
⊢ x * (y * z) = y * (x * z)

Tactic:
exact (h z).symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
x : M
h_1 : x ∈ l₁
z : M
⊢ x * (x * z) = x * (x * z)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : Monoid M
l₁ l₂ : List M
h : l₁ ~ l₂
hc : Pairwise Commute l₁
H₂ : ∀ {a b : M}, Commute a b → ∀ (z : M), b * (a * z) = a * (b * z)
⊢ Pairwise (fun (x y : M) ↦ ∀ (z : M), y * (x * z) = x * (y * z)) l₁

Tactic:
apply hc.imp

Premises used: List.Pairwise.imp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
H₄ H₅ : b * a * z = b * a * z
⊢ b * (a * z) = a * (b * z)

Tactic:
rw [← mul_assoc, ← mul_assoc, h]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
G : Type u_7
inst : Group G
h : Eq.{u_7 + 1} (α := G) (prod []) 1
x : ℕ
⊢ Eq.{u_7 + 1} (α := G) (prod (rotate [] x)) 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ 0 < (a :: l).length

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
G : Type u_7
inst : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ 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))
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
⊢ (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

Premises used: List.take_append_drop, List.cons, HMod.hMod, List.length
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
hl₁ : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
⊢ n % (a :: l).length ≤ (a :: l).length

Tactic:
rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl

Premises used: List.take_append_drop, List.cons, HMod.hMod, List.length
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
rw₉ rw₁₀ : (take (n % (a :: l).length) (a :: l)).prod = (take (n % (a :: l).length) (a :: l)).prod
⊢ ((a :: l).rotate n).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]

Premises used: List.prod_append, mul_assoc, mul_eq_one_iff_inv_eq, List.rotate_mod, List.rotate_eq_drop_append_take, Inv.inv, mul_inv_cancel, mul_one, one_mul, List.prod
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
⊢ sum (map (fun (x : α) ↦ count x []) (filter p (dedup []))) = countP p []

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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 :
  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
⊢ sum (map (fun (x : α) ↦ count x (a :: as)) (filter p (a :: as).dedup)) = countP p (a :: as)

Tactic:
simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]

Premises used: List.count_cons, List.countP_cons, List.sum_map_add
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
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)
⊢ 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:
congr 1
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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

Tactic:
_root_.trans ?_ h

Premises used: trans
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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 :
  Eq (α := ℕ) (sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)))
    (sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)))
⊢ sum (map (fun (i : α) ↦ count i as) (filter p (a :: as).dedup)) = countP p as

Tactic:
refine _root_.trans ?_ h

Premises used: trans
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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)))
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)))
⊢ 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
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
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:
simp [dedup_cons_of_mem ha]

Premises used: List.dedup_cons_of_mem
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
ha : ¬a ∈ as
neg :
  Eq (α := ℕ)
    (sum
      (map (fun (i : α) ↦ count i as)
        (match (motive := Bool → List α) p a with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)))
    (sum (map (fun (i : α) ↦ count i 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)))

Tactic:
simp only [dedup_cons_of_notMem ha, List.filter]

Premises used: List.dedup_cons_of_notMem, List.filter
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
ha : ¬a ∈ as
⊢ Eq (α := ℕ)
    (sum
      (map (fun (i : α) ↦ count i as)
        (match (motive := Bool → List α) true with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)))
    (sum (map (fun (i : α) ↦ count i as) (filter p as.dedup)))

Tactic:
simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]

Premises used: Iff.mpr, List.map_cons, List.count_eq_zero, zero_add, List.sum_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
ha : ¬a ∈ as
⊢ Eq (α := ℕ)
    (sum
      (map (fun (i : α) ↦ count i as)
        (match (motive := Bool → List α) false with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)))
    (sum (map (fun (i : α) ↦ count i as) (filter p as.dedup)))

Tactic:
simp only
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
ha : ¬a ∈ as
⊢ Eq (α := ℕ)
    (sum
      (map (fun (i : α) ↦ count i as)
        (match (motive := Bool → List α) p a with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)))
    (sum (map (fun (i : α) ↦ count i as) (filter p as.dedup)))

Tactic:
match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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 :
  Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)
⊢ 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:
simp only [beq_iff_eq]

Premises used: beq_iff_eq
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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 :
  ∀ (hp : p a = true),
    Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
      (if p a = true then 1 else 0)
neg :
  ∀ (hp : ¬p a = true),
    Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
      (if p a = true then 1 else 0)
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)

Tactic:
by_cases hp : p a
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
a : α
as : List α
h_1 : sum (map (fun (x : α) ↦ count x as) (filter p as.dedup)) = countP p as
hp : p a = true
x : α
h : x ≠ a
h_2 : x ∈ filter p (a :: as).dedup
⊢ Eq (α := ℕ) (if a = x then 1 else 0) 0

Tactic:
simp [h.symm]

Premises used: Ne.symm
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
hp : p a = true
pos : HSMul.hSMul (β := ℕ) (count a (filter p (a :: as).dedup)) (if a = a then 1 else 0) = if p a = true then 1 else 0
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)

Tactic:
refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_

Premises used: trans, List.sum_map_eq_nsmul_single
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
hp : p a = true
⊢ HSMul.hSMul (β := ℕ) (count a (filter p (a :: as).dedup)) (if a = a then 1 else 0) = if p a = true then 1 else 0

Tactic:
simp [hp, count_dedup]

Premises used: List.count_dedup
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
hp : ¬p a = true
n : ℕ
hn : Membership.mem (γ := List ℕ) (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)) n
⊢ n = 0

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
hp : ¬p a = true
⊢ Eq (α := ℕ) 0 (if p a = true then 1 else 0)

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
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
hp : ¬p a = true
⊢ Eq (α := ℕ) (sum (map (fun (i : α) ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)))
    (if p a = true then 1 else 0)

Tactic:
exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])

Premises used: List.sum_eq_zero, trans
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
inst : DecidableEq α
p : α → Bool
l : List α
nil : sum (map (fun (x : α) ↦ count x []) (filter p (dedup []))) = countP p []
cons :
  ∀ (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)
⊢ sum (map (fun (x : α) ↦ count x l) (filter p l.dedup)) = countP p l

Tactic:
induction l with
  | nil => simp
  | cons a as h =>
    simp_rw [List.countP_cons, List.count_cons, List.sum_map_add]
    congr 1
    · refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only
    · simp only [beq_iff_eq]
      by_cases hp : p a
      · refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]
      · exact _root_.trans (List.sum_eq_zero fun n hn => by grind) (by simp [hp])

Premises used: List.sum_eq_zero, trans, beq_iff_eq, List.count_cons, List.cons, List.countP_cons, List.filter, List.count_dedup, List.sum_map_add, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
inst : DecidableEq α
l : List α
⊢ sum (map (fun (x : α) ↦ count x l) l.dedup) = l.length

Tactic:
simpa using sum_map_count_dedup_filter_eq_countP (fun _ => True) l

Premises used: True, List.sum_map_count_dedup_filter_eq_countP, Decidable.decide
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
⊢ (List.sigma (σ := σ) [] l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) [])

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : (l₁.sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) l₁)
⊢ ((x :: l₁).sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) (x :: l₁))

Tactic:
simp only [sigma_cons, length_append, length_map, IH, map, sum_cons]

Premises used: List.map, List.length_append, List.sum_cons, List.sigma_cons, List.length_map
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
σ : α → Type u_8
l₁ : List α
l₂ : (a : α) → List (σ a)
nil : (List.sigma (σ := σ) [] l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) [])
cons :
  ∀ (x : α) (l₁ : List α) (IH : (l₁.sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) l₁)),
    ((x :: l₁).sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) (x :: l₁))
⊢ (l₁.sigma (σ := σ) l₂).length = sum (map (fun (a : α) ↦ (l₂ a).length) l₁)

Tactic:
induction l₁ with
  | nil => rfl
  | cons x l₁ IH => simp only [sigma_cons, length_append, length_map, IH, map, sum_cons]

Premises used: List.map, List.length_append, List.cons, List.sum_cons, List.sigma_cons, List.length_map, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
a : ℕ
l : List ℕ
⊢ (a :: l).ranges.flatten = range (a :: l).sum

Tactic:
simp [ranges, ← map_flatten, ranges_flatten, range_add]

Premises used: List.range_add, List.ranges, List.map_flatten
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
l s : List ℕ
hs : s ∈ l.ranges
rw : Pairwise (fun (x1 x2 : ℕ) ↦ x1 ≠ x2) (range l.sum)
⊢ Pairwise (fun (x1 x2 : ℕ) ↦ x1 ≠ x2) l.ranges.flatten

Tactic:
rw [ranges_flatten]

Premises used: List.ranges_flatten
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun (x1 x2 : ℕ) ↦ x1 ≠ x2) (range l.sum)

Tactic:
nodup_range

Premises used: List.Nodup, List.nodup_range
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun (x1 x2 : ℕ) ↦ x1 ≠ x2) (range l.sum)

Tactic:
exact nodup_range

Premises used: List.nodup_range
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
l : List ℕ
n : ℕ
rw : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ range l.sum
rw₁ : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ l.ranges.flatten
rw₂ rw₃ : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ ∃ (l_1 : List ℕ), l_1 ∈ l.ranges ∧ n ∈ l_1
⊢ (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum

Tactic:
rw [← mem_range, ← ranges_flatten, mem_flatten]

Premises used: List.mem_range, List.mem_flatten, List.ranges_flatten
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ take i (map length L) = take i (map length (take (i + 1) L))

Tactic:
simp [map_take, take_take, Nat.min_eq_left]

Premises used: List.take_take, Nat.min_eq_left, List.map_take
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ take i (map length L) = take i (map length (take (i + 1) L))

Tactic:
have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
    simp [map_take, take_take, Nat.min_eq_left]
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
this : take i (map length L) = take i (map length (take (i + 1) L))
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) =
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) L i h

Tactic:
simp only [this, take_sum_flatten, drop_sum_flatten,
    drop_take_succ_eq_cons_getElem, h, flatten_nil, flatten_cons, append_nil]

Premises used: List.append_nil, List.drop_sum_flatten, List.flatten_nil, List.flatten_cons, List.drop_take_succ_eq_cons_getElem, List.take_sum_flatten
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
l : List ℤ
h : l.prod = -1
⊢ Ne (α := ℤ) (-1) 1

Tactic:
decide
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
l : List ℤ
h : l.prod = -1
obtain : ∀ (x : ℤ) (h₁ : x ∈ l) (h₂ : x ≠ 1), -1 ∈ l
⊢ -1 ∈ l

Tactic:
obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))

Premises used: ne_of_eq_of_ne, List.exists_mem_ne_one_of_prod_ne_one
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ HMul.hMul (α := ℤ) (-1) (-1) = 1

Tactic:
decide
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l

Tactic:
exact Or.resolve_left
    (Int.isUnit_iff.mp (prod_isUnit_iff.mp
      (h.symm ▸ ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩ : IsUnit l.prod) x h₁)) h₂ ▸ h₁
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : CommMonoid M
a : M
l : List M
ha : a ∈ l
let : ∀ (s t : List M) (h : l = s ++ a :: t), a ∣ l.prod
⊢ a ∣ l.prod

Tactic:
let ⟨s, t, h⟩ := append_of_mem ha
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
rw : a ∣ a * (s.prod * t.prod)
⊢ a ∣ l.prod

Tactic:
rw [h, prod_append, prod_cons, mul_left_comm]

Premises used: List.prod_append, mul_left_comm, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (s.prod * t.prod)

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (s.prod * t.prod)

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
obtain : ∀ (l : List M) (hl : l₂ ~ l₁ ++ l), l₁.prod ∣ l₂.prod
⊢ l₁.prod ∣ l₂.prod

Tactic:
obtain ⟨l, hl⟩ := h.exists_perm_append

Premises used: List.Sublist.exists_perm_append
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
rw : l₁.prod ∣ l₁.prod * l.prod
⊢ l₁.prod ∣ l₂.prod

Tactic:
rw [hl.prod_eq, prod_append]

Premises used: List.prod_append, List.Perm.prod_eq
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₁.prod * l.prod

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas
Goal:
M : Type u_4
inst : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
l : List M
hl : l₂ ~ l₁ ++ l
⊢ l₁.prod ∣ l₁.prod * l.prod

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right