[GOAL]
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 List.prod (List.map (List.cons (-1)) L1)) = -List.sum (List.map List.prod L1)
[PROOFSTEP]
simp only [List.map_map, (· ∘ ·), List.prod_cons, neg_one_mul]
[GOAL]
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)
[PROOFSTEP]
refine' List.recOn L1 neg_zero.symm fun hd tl ih ↦ _
[GOAL]
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))
[PROOFSTEP]
rw [List.map_cons, List.sum_cons, ih, List.map_cons, List.sum_cons, neg_add]
[GOAL]
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)
[PROOFSTEP]
rw [List.map_append, List.sum_append]
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
⊢ C x
[PROOFSTEP]
have h0 : C 0 := add_neg_self (1 : R) ▸ ha h1 hneg1
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
⊢ C x
[PROOFSTEP]
rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩
[GOAL]
case intro.intro
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hx : List.sum (List.map List.prod L) ∈ closure s
⊢ C (List.sum (List.map List.prod L))
[PROOFSTEP]
clear hx
[GOAL]
case intro.intro
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
⊢ C (List.sum (List.map List.prod L))
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.nil
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
HL : ∀ (l : List R), l ∈ [] → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
⊢ C (List.sum (List.map List.prod []))
[PROOFSTEP]
exact h0
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : ∀ (l : List R), l ∈ hd :: tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
rw [List.forall_mem_cons] at HL 
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (x_1 : R), x_1 ∈ x → x_1 ∈ s ∨ x_1 = -1
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
suffices C (List.prod hd) by
  rw [List.map_cons, List.sum_cons]
  exact ha this (ih HL.2)
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (x_1 : R), x_1 ∈ x → x_1 ∈ s ∨ x_1 = -1
this : C (List.prod hd)
⊢ C (List.sum (List.map List.prod (hd :: tl)))
[PROOFSTEP]
rw [List.map_cons, List.sum_cons]
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (x_1 : R), x_1 ∈ x → x_1 ∈ s ∨ x_1 = -1
this : C (List.prod hd)
⊢ C (List.prod hd + List.sum (List.map List.prod tl))
[PROOFSTEP]
exact ha this (ih HL.2)
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : (∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1) ∧ ∀ (x : List R), x ∈ tl → ∀ (x_1 : R), x_1 ∈ x → x_1 ∈ s ∨ x_1 = -1
⊢ C (List.prod hd)
[PROOFSTEP]
replace HL := HL.1
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
tl : List (List R)
ih : (∀ (l : List R), l ∈ tl → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1) → C (List.sum (List.map List.prod tl))
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
⊢ C (List.prod hd)
[PROOFSTEP]
clear ih tl
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
⊢ C (List.prod hd)
[PROOFSTEP]
suffices ∃ L, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
  by
  rcases this with ⟨L, HL', HP | HP⟩ <;> rw [HP] <;> clear HP HL
  · induction' L with hd tl ih
    · exact h1
    rw [List.forall_mem_cons] at HL' 
    rw [List.prod_cons]
    exact hs _ HL'.1 _ (ih HL'.2)
  · induction' L with hd tl ih
    · exact hneg1
    rw [List.prod_cons, neg_mul_eq_mul_neg]
    rw [List.forall_mem_cons] at HL' 
    exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
this : ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
⊢ C (List.prod hd)
[PROOFSTEP]
rcases this with ⟨L, HL', HP | HP⟩
[GOAL]
case intro.intro.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rw [HP]
[GOAL]
case intro.intro.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (List.prod hd)
[PROOFSTEP]
rw [HP]
[GOAL]
case intro.intro.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = List.prod L
⊢ C (List.prod L)
[PROOFSTEP]
clear HP HL
[GOAL]
case intro.intro.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod hd = -List.prod L
⊢ C (-List.prod L)
[PROOFSTEP]
clear HP HL
[GOAL]
case intro.intro.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
⊢ C (List.prod L)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.inl.nil
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
HL' : ∀ (x : R), x ∈ [] → x ∈ s
⊢ C (List.prod [])
[PROOFSTEP]
exact h1
[GOAL]
case intro.intro.inl.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (List.prod (hd :: tl))
[PROOFSTEP]
rw [List.forall_mem_cons] at HL' 
[GOAL]
case intro.intro.inl.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (List.prod (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons]
[GOAL]
case intro.intro.inl.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (hd * List.prod tl)
[PROOFSTEP]
exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
case intro.intro.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
⊢ C (-List.prod L)
[PROOFSTEP]
induction' L with hd tl ih
[GOAL]
case intro.intro.inr.nil
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
HL' : ∀ (x : R), x ∈ [] → x ∈ s
⊢ C (-List.prod [])
[PROOFSTEP]
exact hneg1
[GOAL]
case intro.intro.inr.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (-List.prod (hd :: tl))
[PROOFSTEP]
rw [List.prod_cons, neg_mul_eq_mul_neg]
[GOAL]
case intro.intro.inr.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : ∀ (x : R), x ∈ hd :: tl → x ∈ s
⊢ C (hd * -List.prod tl)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL' 
[GOAL]
case intro.intro.inr.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ L : List R
HL'✝ : ∀ (x : R), x ∈ L → x ∈ s
hd : R
tl : List R
ih : (∀ (x : R), x ∈ tl → x ∈ s) → C (-List.prod tl)
HL' : hd ∈ s ∧ ∀ (x : R), x ∈ tl → x ∈ s
⊢ C (hd * -List.prod tl)
[PROOFSTEP]
exact hs _ HL'.1 _ (ih HL'.2)
[GOAL]
case intro.intro.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
[PROOFSTEP]
induction' hd with hd tl ih
[GOAL]
case intro.intro.cons.nil
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd : List R
HL✝ : ∀ (x : R), x ∈ hd → x ∈ s ∨ x = -1
HL : ∀ (x : R), x ∈ [] → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod [] = List.prod L ∨ List.prod [] = -List.prod L)
[PROOFSTEP]
exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
[GOAL]
case intro.intro.cons.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : ∀ (x : R), x ∈ hd :: tl → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
rw [List.forall_mem_cons] at HL 
[GOAL]
case intro.intro.cons.cons
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
rcases ih HL.2 with ⟨L, HL', HP | HP⟩
[GOAL]
case intro.intro.cons.cons.intro.intro.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
cases' HL.1 with hhd hhd
[GOAL]
case intro.intro.cons.cons.intro.intro.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
cases' HL.1 with hhd hhd
[GOAL]
case intro.intro.cons.cons.intro.intro.inl.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd ∈ s
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨hd :: L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, Or.inl <| by rw [List.prod_cons, List.prod_cons, HP]⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd ∈ s
⊢ List.prod (hd :: tl) = List.prod (hd :: L)
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, HP]
[GOAL]
case intro.intro.cons.cons.intro.intro.inl.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = List.prod L
hhd : hd = -1
⊢ List.prod (hd :: tl) = -List.prod L
[PROOFSTEP]
rw [List.prod_cons, hhd, neg_one_mul, HP]
[GOAL]
case intro.intro.cons.cons.intro.intro.inr.inl
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd ∈ s
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact
  ⟨hd :: L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, Or.inr <| by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd ∈ s
⊢ List.prod (hd :: tl) = -List.prod (hd :: L)
[PROOFSTEP]
rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]
[GOAL]
case intro.intro.cons.cons.intro.intro.inr.inr
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd = -1
⊢ ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod (hd :: tl) = List.prod L ∨ List.prod (hd :: tl) = -List.prod L)
[PROOFSTEP]
exact ⟨L, HL', Or.inl <| by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
cR : Type u
inst✝ : CommRing cR
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ (z : R), z ∈ s → ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L✝ : List (List R)
HL✝¹ : ∀ (l : List R), l ∈ L✝ → ∀ (x : R), x ∈ l → x ∈ s ∨ x = -1
hd✝ : List R
HL✝ : ∀ (x : R), x ∈ hd✝ → x ∈ s ∨ x = -1
hd : R
tl : List R
ih :
  (∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1) →
    ∃ L, (∀ (x : R), x ∈ L → x ∈ s) ∧ (List.prod tl = List.prod L ∨ List.prod tl = -List.prod L)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ (x : R), x ∈ tl → x ∈ s ∨ x = -1
L : List R
HL' : ∀ (x : R), x ∈ L → x ∈ s
HP : List.prod tl = -List.prod L
hhd : hd = -1
⊢ List.prod (hd :: tl) = List.prod L
[PROOFSTEP]
rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]
[GOAL]
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
⊢ ↑f '' closure s = closure (↑f '' s)
[PROOFSTEP]
refine'
  le_antisymm _ (closure_subset (RingHom.isSubring_image _ closure.isSubring) <| Set.image_subset _ subset_closure)
[GOAL]
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
⊢ ↑f '' closure s ≤ closure (↑f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ↑f x ∈ closure (↑f '' s)
[PROOFSTEP]
apply AddGroup.InClosure.recOn (motive := fun {x} _ ↦ f x ∈ closure (f '' s)) hx _
[GOAL]
case intro.intro.zero
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ↑f 0 ∈ closure (↑f '' s)
[PROOFSTEP]
intros
[GOAL]
case intro.intro.neg
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ∀ {a : R}, AddGroup.InClosure (Monoid.Closure s) a → ↑f a ∈ closure (↑f '' s) → ↑f (-a) ∈ closure (↑f '' s)
[PROOFSTEP]
intros
[GOAL]
case intro.intro.add
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ∀ {a b : R},
    AddGroup.InClosure (Monoid.Closure s) a →
      AddGroup.InClosure (Monoid.Closure s) b →
        ↑f a ∈ closure (↑f '' s) → ↑f b ∈ closure (↑f '' s) → ↑f (a + b) ∈ closure (↑f '' s)
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ∀ {a : R} (a_1 : a ∈ Monoid.Closure s),
    (fun {x} x_1 => ↑f x ∈ closure (↑f '' s)) (_ : AddGroup.InClosure (Monoid.Closure s) a)
[PROOFSTEP]
intros
[GOAL]
case intro.intro.zero
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ ↑f 0 ∈ closure (↑f '' s)
[PROOFSTEP]
rw [f.map_zero]
[GOAL]
case intro.intro.zero
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ 0 ∈ closure (↑f '' s)
[PROOFSTEP]
apply closure.isSubring.zero_mem
[GOAL]
case intro.intro.neg
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : AddGroup.InClosure (Monoid.Closure s) a✝¹
a_ih✝ : ↑f a✝¹ ∈ closure (↑f '' s)
⊢ ↑f (-a✝¹) ∈ closure (↑f '' s)
[PROOFSTEP]
rw [f.map_neg]
[GOAL]
case intro.intro.neg
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : AddGroup.InClosure (Monoid.Closure s) a✝¹
a_ih✝ : ↑f a✝¹ ∈ closure (↑f '' s)
⊢ -↑f a✝¹ ∈ closure (↑f '' s)
[PROOFSTEP]
apply closure.isSubring.neg_mem
[GOAL]
case intro.intro.neg
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : AddGroup.InClosure (Monoid.Closure s) a✝¹
a_ih✝ : ↑f a✝¹ ∈ closure (↑f '' s)
⊢ ↑f a✝¹ ∈ closure (↑f '' s)
[PROOFSTEP]
assumption
[GOAL]
case intro.intro.add
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝² b✝ : R
a✝¹ : AddGroup.InClosure (Monoid.Closure s) a✝²
a✝ : AddGroup.InClosure (Monoid.Closure s) b✝
a_ih✝¹ : ↑f a✝² ∈ closure (↑f '' s)
a_ih✝ : ↑f b✝ ∈ closure (↑f '' s)
⊢ ↑f (a✝² + b✝) ∈ closure (↑f '' s)
[PROOFSTEP]
rw [f.map_add]
[GOAL]
case intro.intro.add
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝² b✝ : R
a✝¹ : AddGroup.InClosure (Monoid.Closure s) a✝²
a✝ : AddGroup.InClosure (Monoid.Closure s) b✝
a_ih✝¹ : ↑f a✝² ∈ closure (↑f '' s)
a_ih✝ : ↑f b✝ ∈ closure (↑f '' s)
⊢ ↑f a✝² + ↑f b✝ ∈ closure (↑f '' s)
[PROOFSTEP]
apply closure.isSubring.add_mem
[GOAL]
case intro.intro.add.a
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝² b✝ : R
a✝¹ : AddGroup.InClosure (Monoid.Closure s) a✝²
a✝ : AddGroup.InClosure (Monoid.Closure s) b✝
a_ih✝¹ : ↑f a✝² ∈ closure (↑f '' s)
a_ih✝ : ↑f b✝ ∈ closure (↑f '' s)
⊢ ↑f a✝² ∈ closure (↑f '' s)
case intro.intro.add.a
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝² b✝ : R
a✝¹ : AddGroup.InClosure (Monoid.Closure s) a✝²
a✝ : AddGroup.InClosure (Monoid.Closure s) b✝
a_ih✝¹ : ↑f a✝² ∈ closure (↑f '' s)
a_ih✝ : ↑f b✝ ∈ closure (↑f '' s)
⊢ ↑f b✝ ∈ closure (↑f '' s)
[PROOFSTEP]
assumption'
[GOAL]
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : a✝¹ ∈ Monoid.Closure s
⊢ ↑f a✝¹ ∈ closure (↑f '' s)
[PROOFSTEP]
apply AddGroup.mem_closure
[GOAL]
case a
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : a✝¹ ∈ Monoid.Closure s
⊢ ↑f a✝¹ ∈ Monoid.Closure (↑f '' s)
[PROOFSTEP]
rw [← Monoid.image_closure f.to_isMonoidHom]
[GOAL]
case a
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : a✝¹ ∈ Monoid.Closure s
⊢ ↑f a✝¹ ∈ ↑f '' Monoid.Closure s
[PROOFSTEP]
apply Set.mem_image_of_mem
[GOAL]
case a.h
R : Type u
inst✝² : Ring R
cR : Type u
inst✝¹ : CommRing cR
s✝ : Set R
S : Type u_1
inst✝ : Ring S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
a✝¹ : R
a✝ : a✝¹ ∈ Monoid.Closure s
⊢ a✝¹ ∈ Monoid.Closure s
[PROOFSTEP]
assumption
