-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem mem_closure_iff_exists_list {R} [Semiring R] {s : Set R} {x} :
    x ∈ closure s ↔ ∃ L : List (List R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (L.map List.prod).sum = x

Proof state:
case mp.mem.mul.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x y : R
hx✝ : x ∈ Submonoid.closure s
hy✝ : y ∈ Submonoid.closure s
ht : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = y
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
u : List R
hu1 : ∀ y ∈ u, y ∈ s
hu2 : u.prod = y
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y

Tactic:
exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s ↔ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s → ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s

Proof state:
case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s

Tactic:
rintro ⟨L, HL1, HL2⟩

Result:
case mpr.intro.intro
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
⊢ x ∈ closure s

Proof state:
case mp.mem
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Tactic:
induction hx using Submonoid.closure_induction with
| mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
| one => exact ⟨[], List.forall_mem_nil _, rfl⟩
| mul x y _ _ ht hu =>
  obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
  exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩

Result:
no goals

Proof state:
case mp.mem.one
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = 1

Tactic:
exact ⟨[], List.forall_mem_nil _, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
this : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
⊢ (List.map List.prod [t]).sum = x

Tactic:
rw [List.map_singleton, List.sum_singleton, ht2]

Result:
no goals

Proof state:
case mp.mem.mem
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x : R
hx : x ∈ s
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Tactic:
exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x y : R
hx✝ : x ∈ Submonoid.closure s
hy✝ : y ∈ Submonoid.closure s
ht : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = y
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
u : List R
hu1 : ∀ y ∈ u, y ∈ s
hu2 : u.prod = y
⊢ (t ++ u).prod = x * y

Tactic:
rw [List.prod_append, ht2, hu2]

Result:
no goals

Proof state:
case mp.mul.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x y : R
hx✝ : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hy✝ : y ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s
HM2 : (List.map List.prod M).sum = y
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y

Tactic:
exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
  rw [List.map_append, List.sum_append, HL2, HM2]⟩

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
⊢ x ∈ closure s

Tactic:
exact HL2 ▸
  list_sum_mem fun r hr =>
    let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
    ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x y : R
hx✝ : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hy✝ : y ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s
HM2 : (List.map List.prod M).sum = y
⊢ (List.map List.prod (L ++ M)).sum = x + y

Tactic:
rw [List.map_append, List.sum_append, HL2, HM2]

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
induction hx using AddSubmonoid.closure_induction with
| mem x hx =>
  suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
    let ⟨t, ht1, ht2⟩ := this
    ⟨[t], List.forall_mem_singleton.2 ht1, by
      rw [List.map_singleton, List.sum_singleton, ht2]⟩
  induction hx using Submonoid.closure_induction with
  | mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
  | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
  | mul x y _ _ ht hu =>
    obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
    exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
| one => exact ⟨[], List.forall_mem_nil _, rfl⟩
| mul x y _ _ hL hM =>
  obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
  exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
    rw [List.map_append, List.sum_append, HL2, HM2]⟩

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s → ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
intro hx

Result:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ closure s
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Proof state:
case mp.mem
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
  let ⟨t, ht1, ht2⟩ := this
  ⟨[t], List.forall_mem_singleton.2 ht1, by
    rw [List.map_singleton, List.sum_singleton, ht2]⟩

Result:
case mp.mem
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ closure s
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
rw [mem_closure_iff] at hx

Result:
case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
hx : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Proof state:
case mp.mem.mul
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x y : R
hx✝ : x ∈ Submonoid.closure s
hy✝ : y ∈ Submonoid.closure s
ht : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = y
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y

Tactic:
obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu

Result:
case mp.mem.mul.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x y : R
hx✝ : x ∈ Submonoid.closure s
hy✝ : y ∈ Submonoid.closure s
ht : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
hu : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = y
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
u : List R
hu1 : ∀ y ∈ u, y ∈ s
hu2 : u.prod = y
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x * y