-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem InClosure.recOn {C : R → Prop} {x : R} (hx : x ∈ closure s) (h1 : C 1)
    (hneg1 : C (-1)) (hs : ∀ z ∈ s, ∀ n, C n → C (z * n)) (ha : ∀ {x y}, C x → C y → C (x + y)) :
    C x

Proof state:
case intro.intro.cons.intro.intro.inl
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ 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 R
HL' : ∀ x ∈ L, x ∈ s
⊢ C L.prod

Tactic:
induction' L with hd tl ih

Result:
case intro.intro.cons.intro.intro.inl.nil
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL' : ∀ x ∈ [], x ∈ s
⊢ C [].prod

case intro.intro.cons.intro.intro.inl.cons
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ x ∈ tl, x ∈ s) → C tl.prod
HL' : ∀ x ∈ hd :: tl, x ∈ s
⊢ C (hd :: tl).prod

Proof state:
case cons.intro.intro.inl.inr
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
hhd : hd = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩

Result:
no goals

Proof state:
case intro.intro.nil
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL : ∀ t ∈ [], ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.map List.prod []).sum

Tactic:
exact h0

Result:
no goals

Proof state:
case intro.intro
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ 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 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.map List.prod L).sum

Tactic:
induction' L with hd tl ih

Result:
case intro.intro.nil
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
HL : ∀ t ∈ [], ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.map List.prod []).sum

case intro.intro.cons
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ s ∨ y = -1
⊢ C (List.map List.prod (hd :: tl)).sum

Proof state:
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd = -1
⊢ (hd :: tl).prod = L.prod

Tactic:
rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (List.map List.prod (hd :: tl)).sum

Tactic:
rw [List.map_cons, List.sum_cons]

Result:
R : Type u
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
tl : List (List R)
ih : (∀ t ∈ tl, ∀ y ∈ t, y ∈ s ∨ y = -1) → C (List.map List.prod tl).sum
HL : (∀ y ∈ hd, y ∈ s ∨ y = -1) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ s ∨ y = -1
this : C hd.prod
⊢ C (hd.prod + (List.map List.prod tl).sum)