-- Mathlib/Algebra/Group/Submonoid/Finsupp.lean
theorem exists_finsupp_of_mem_closure_range (hx : x ∈ closure (Set.range f)) :
    ∃ a : ι →₀ ℕ, x = a.prod (f · ^ ·)

Proof state:
case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 => f x1 ^ x2

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ f i = (Finsupp.single i 1).prod fun x1 x2 => f x1 ^ x2

Tactic:
simp

Result:
no goals

Proof state:
case mul
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x✝ x y : M
hx : x ∈ closure (Set.range f)
hy : y ∈ closure (Set.range f)
hx' : ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2
hy' : ∃ a, y = a.prod fun x1 x2 => f x1 ^ x2
⊢ ∃ a, x * y = a.prod fun x1 x2 => f x1 ^ x2

Tactic:
obtain ⟨⟨v, rfl⟩, w, rfl⟩ := And.intro hx' hy'

Result:
case mul.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
⊢ ∃ a, ((v.prod fun x1 x2 => f x1 ^ x2) * w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2

Proof state:
case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
⊢ ((v.prod fun x1 x2 => f x1 ^ x2) * w.prod fun x1 x2 => f x1 ^ x2) = (v + w).prod fun x1 x2 => f x1 ^ x2

Tactic:
rw [Finsupp.prod_add_index]

Result:
case h.h_zero
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, f a ^ 0 = 1

case h.h_add
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℕ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂

Proof state:
case h.h_zero
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, f a ^ 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
case mem
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x✝ x : M
h : x ∈ Set.range f
⊢ ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2

Tactic:
obtain ⟨i, rfl⟩ := h

Result:
case mem.intro
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ a, f i = a.prod fun x1 x2 => f x1 ^ x2

Proof state:
case h.h_add
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℕ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂

Tactic:
simp [pow_add]

Result:
no goals

Proof state:
case mem.intro
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
i : ι
⊢ ∃ a, f i = a.prod fun x1 x2 => f x1 ^ x2

Tactic:
exact ⟨Finsupp.single i 1, by simp⟩

Result:
no goals

Proof state:
case mul.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
⊢ ∃ a, ((v.prod fun x1 x2 => f x1 ^ x2) * w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2

Tactic:
use v + w

Result:
case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 => f x1 ^ x2) = a.prod fun x1 x2 => f x1 ^ x2
⊢ ((v.prod fun x1 x2 => f x1 ^ x2) * w.prod fun x1 x2 => f x1 ^ x2) = (v + w).prod fun x1 x2 => f x1 ^ x2

Proof state:
case one
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ ∃ a, 1 = a.prod fun x1 x2 => f x1 ^ x2

Tactic:
use 0

Result:
case h
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
⊢ 1 = Finsupp.prod 0 fun x1 x2 => f x1 ^ x2