R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ ∀ (y : R), y ∈ l → y ∈ s ∨ y = -1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ (∀ (t : List R), t ∈ [l] → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod [l]) = x
simp [h]
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ ∀ (y : R), y ∈ l → y ∈ s ∨ y = -1
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ ∀ (y : R), y ∈ l → y ∈ s ∨ y = -1
clear_aux_decl
no goals
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝ : R
h✝ : x✝ ∈ closure s
x : R
hx : x ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ (y : R), y ∈ l → y ∈ s
h : List.prod l = x
⊢ ∀ (y : R), y ∈ l → y ∈ s ∨ y = -1
tauto
no goals
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x : R
h : x ∈ closure s
⊢ (∀ (t : List R), t ∈ [] → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod []) = 0
simp
no goals
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝² : R
h : x✝² ∈ closure s
x y : R
x✝¹ :
  (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) y
l : List (List R)
hl1 : ∀ (t : List R), t ∈ l → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hl2 : List.sum (List.map List.prod l) = x
m : List (List R)
hm1 : ∀ (t : List R), t ∈ m → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1
hm2 : List.sum (List.map List.prod m) = y
⊢ List.sum (List.map List.prod (l ++ m)) = x + y
simp [hl2, hm2]
no goals
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x : R
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
L : List (List R)
hL : (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x
⊢ List.sum (List.map List.prod (List.map (List.cons (-1)) [])) = -List.sum (List.map List.prod [])
simp
no goals
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
s : Set R
x✝¹ : R
h : x✝¹ ∈ closure s
x : R
x✝ : (fun x => ∃ L, (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x) x
L : List (List R)
hL : (∀ (t : List R), t ∈ L → ∀ (y : R), y ∈ t → y ∈ s ∨ y = -1) ∧ List.sum (List.map List.prod L) = x
⊢ ∀ (head : List R) (tail : List (List R)),
    List.sum (List.map List.prod (List.map (List.cons (-1)) tail)) = -List.sum (List.map List.prod tail) →
      List.sum (List.map List.prod (List.map (List.cons (-1)) (head :: tail))) =
        -List.sum (List.map List.prod (head :: tail))
simp (config := { contextual := true }) [List.map_cons, add_comm]