[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h : ∀ (b : R), b ∈ l → Commute a b
⊢ Commute a (sum l)
[PROOFSTEP]
induction' l with x xs ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h✝ : ∀ (b : R), b ∈ l → Commute a b
h : ∀ (b : R), b ∈ [] → Commute a b
⊢ Commute a (sum [])
[PROOFSTEP]
exact Commute.zero_right _
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h✝ : ∀ (b : R), b ∈ l → Commute a b
x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a (sum xs)
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (sum (x :: xs))
[PROOFSTEP]
rw [List.sum_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : NonUnitalNonAssocSemiring R
a : R
l : List R
h✝ : ∀ (b : R), b ∈ l → Commute a b
x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a (sum xs)
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + sum xs)
[PROOFSTEP]
exact (h _ <| mem_cons_self _ _).add_right (ih fun j hj => h _ <| mem_cons_of_mem _ hj)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ prod l = 1
[PROOFSTEP]
rw [List.eq_replicate.2 ⟨_, h⟩, prod_replicate, one_pow]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ ℕ
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ length l = ?m.7726
[PROOFSTEP]
exact (length l)
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
l : List M
h : ∀ (x : M), x ∈ l → x = 1
⊢ length l = length l
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℤ
h : prod l = -1
⊢ -1 ∈ l
[PROOFSTEP]
obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℤ
h : prod l = -1
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
l : List ℤ
h : prod l = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l
[PROOFSTEP]
exact
  Or.resolve_left (Int.isUnit_iff.mp (prod_isUnit_iff.mp (h.symm ▸ IsUnit.neg isUnit_one : IsUnit l.prod) x h₁)) h₂ ▸ h₁
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
⊢ length L ≤ sum L
[PROOFSTEP]
induction' L with j L IH h
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L → 1 ≤ i
h : ∀ (i : ℕ), i ∈ [] → 1 ≤ i
⊢ length [] ≤ sum []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L✝ : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L✝ → 1 ≤ i
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → length L ≤ sum L
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ length (j :: L) ≤ sum (j :: L)
[PROOFSTEP]
rw [sum_cons, length, add_comm]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
L✝ : List ℕ
h✝ : ∀ (i : ℕ), i ∈ L✝ → 1 ≤ i
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → length L ≤ sum L
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ 1 + length L ≤ j + sum L
[PROOFSTEP]
exact add_le_add (h _ (mem_cons_self _ _)) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ prod l
[PROOFSTEP]
let ⟨s, t, h⟩ := mem_split ha
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ prod l
[PROOFSTEP]
rw [h, prod_append, prod_cons, mul_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ a * (prod s * prod t)
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Semiring R
a : R
l : List R
h : ∀ (x : R), x ∈ l → a ∣ x
⊢ a ∣ sum l
[PROOFSTEP]
induction' l with x l ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Semiring R
a : R
l : List R
h✝ : ∀ (x : R), x ∈ l → a ∣ x
h : ∀ (x : R), x ∈ [] → a ∣ x
⊢ a ∣ sum []
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Semiring R
a : R
l✝ : List R
h✝ : ∀ (x : R), x ∈ l✝ → a ∣ x
x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ sum l
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ sum (x :: l)
[PROOFSTEP]
rw [List.sum_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Semiring R
a : R
l✝ : List R
h✝ : ∀ (x : R), x ∈ l✝ → a ∣ x
x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ sum l
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ x + sum l
[PROOFSTEP]
exact dvd_add (h _ (mem_cons_self _ _)) (ih fun x hx => h x (mem_cons_of_mem _ hx))
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
l₂ : List α
⊢ alternatingProd ([] ++ l₂) = alternatingProd [] * alternatingProd l₂ ^ (-1) ^ length []
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a : α
l₁ l₂ : List α
⊢ alternatingProd (a :: l₁ ++ l₂) = alternatingProd (a :: l₁) * alternatingProd l₂ ^ (-1) ^ length (a :: l₁)
[PROOFSTEP]
simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ, neg_mul, one_mul, zpow_neg, ←
  div_eq_mul_inv, div_div]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
⊢ alternatingProd (reverse []) = alternatingProd [] ^ (-1) ^ (length [] + 1)
[PROOFSTEP]
simp only [alternatingProd_nil, one_zpow, reverse_nil]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a : α
l : List α
⊢ alternatingProd (reverse (a :: l)) = alternatingProd (a :: l) ^ (-1) ^ (length (a :: l) + 1)
[PROOFSTEP]
simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse, alternatingProd_singleton, alternatingProd_cons,
  length_reverse, length, pow_succ, neg_mul, one_mul, zpow_neg, inv_inv]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : CommGroup α
a : α
l : List α
⊢ (alternatingProd l ^ (-1) ^ length l)⁻¹ * a ^ (-1) ^ length l = (a / alternatingProd l) ^ (-1) ^ length l
[PROOFSTEP]
rw [mul_comm, ← div_eq_mul_inv, div_zpow]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
⊢ ∀ (l : List M), op (prod l) = prod (reverse (map op l))
[PROOFSTEP]
intro l
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List M
⊢ op (prod l) = prod (reverse (map op l))
[PROOFSTEP]
induction l with
| nil => rfl
| cons x xs ih => rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List M
⊢ op (prod l) = prod (reverse (map op l))
[PROOFSTEP]
induction l with
| nil => rfl
| cons x xs ih => rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
⊢ op (prod []) = prod (reverse (map op []))
[PROOFSTEP]

| nil => rfl
[GOAL]
case nil
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
⊢ op (prod []) = prod (reverse (map op []))
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
x : M
xs : List M
ih : op (prod xs) = prod (reverse (map op xs))
⊢ op (prod (x :: xs)) = prod (reverse (map op (x :: xs)))
[PROOFSTEP]

| cons x xs ih => rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
x : M
xs : List M
ih : op (prod xs) = prod (reverse (map op xs))
⊢ op (prod (x :: xs)) = prod (reverse (map op (x :: xs)))
[PROOFSTEP]
rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ unop (prod l) = prod (reverse (map unop l))
[PROOFSTEP]
rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse, op_comp_unop, map_id]
[GOAL]
ι : Type u_1
α : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M₀ : Type u_6
G : Type u_7
R : Type u_8
inst✝² : Monoid M
inst✝¹ : Monoid N
F : Type u_9
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ unop (↑f (prod l)) = prod (reverse (map (unop ∘ ↑f) l))
[PROOFSTEP]
rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]
