R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
a : R
h : a ∈ closure s
b : R
ih✝ : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = b
L1 : List (List R)
h1 : ∀ (l : List R), l ∈ L1 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
x✝ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L1))
hd : List R
tl : List (List R)
ih : List.sum (List.map (fun x => -List.prod x) tl) = -List.sum (List.map List.prod tl)
⊢ List.sum (List.map (fun x => -List.prod x) (hd :: tl)) = -List.sum (List.map List.prod (hd :: tl))
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
a : R
h : a ∈ closure s
b : R
ih : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = b
L1 : List (List R)
h1 : ∀ (l : List R), l ∈ L1 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
x✝ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L1))
⊢ List.sum (List.map (fun x => -List.prod x) L1) = -List.sum (List.map List.prod L1)
refine' List.recOn L1 neg_zero.symm fun hd tl ih ↦ _
no goals
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
a : R
h : a ∈ closure s
b : R
ih✝ : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = b
L1 : List (List R)
h1 : ∀ (l : List R), l ∈ L1 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
x✝ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L1))
hd : List R
tl : List (List R)
ih : List.sum (List.map (fun x => -List.prod x) tl) = -List.sum (List.map List.prod tl)
⊢ List.sum (List.map (fun x => -List.prod x) (hd :: tl)) = -List.sum (List.map List.prod (hd :: tl))
rw [List.map_cons, List.sum_cons, ih, List.map_cons, List.sum_cons, neg_add]
no goals
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
a : R
h : a ∈ closure s
r1 r2 : R
ih1 : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = r1
ih2 : ∃ L, (∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) ∧ List.sum (List.map List.prod L) = r2
L1 : List (List R)
h1 : ∀ (l : List R), l ∈ L1 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
L2 : List (List R)
h2 : ∀ (l : List R), l ∈ L2 → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
x✝¹ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L1))
x✝ : AddGroup.InClosure (Monoid.Closure s) (List.sum (List.map List.prod L2))
⊢ List.sum (List.map List.prod (L1 ++ L2)) = List.sum (List.map List.prod L1) + List.sum (List.map List.prod L2)
rw [List.map_append, List.sum_append]