-- Mathlib/Data/Finsupp/Defs.lean
lemma range_mapRange (e : M → N) (he₀ : e 0 = 0) :
    Set.range (Finsupp.mapRange (α := α) e he₀) = {g | ∀ i, g i ∈ Set.range e}

Proof state:
case h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ g ∈ Set.range (mapRange e he₀) ↔ g ∈ {g | ∀ (i : α), g i ∈ Set.range e}

Tactic:
simp only [Set.mem_range, Set.mem_setOf]

Result:
case h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∃ y, mapRange e he₀ y = g) ↔ ∀ (i : α), ∃ y, e y = g i

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
⊢ Set.range (mapRange e he₀) = {g | ∀ (i : α), g i ∈ Set.range e}

Tactic:
ext g

Result:
case h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ g ∈ Set.range (mapRange e he₀) ↔ g ∈ {g | ∀ (i : α), g i ∈ Set.range e}

Proof state:
case h.mpr
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ ∃ y, mapRange e he₀ y = g

Tactic:
use onFinset g.support (Set.indicator g.support f) (by aesop)

Result:
case h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ mapRange e he₀ (onFinset g.support ((↑g.support).indicator f) ⋯) = g

Proof state:
case h.mp
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∃ y, mapRange e he₀ y = g) → ∀ (i : α), ∃ y, e y = g i

Tactic:
rintro ⟨g, rfl⟩ i

Result:
case h.mp.intro
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ M
i : α
⊢ ∃ y, e y = (mapRange e he₀ g) i

Proof state:
case h.mp.intro
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ M
i : α
⊢ ∃ y, e y = (mapRange e he₀ g) i

Tactic:
simp

Result:
no goals

Proof state:
case h.mpr
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ y, e y = g i
⊢ ∃ y, mapRange e he₀ y = g

Tactic:
choose f h using h

Result:
case h.mpr
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ ∃ y, mapRange e he₀ y = g

Proof state:
case h.mpr
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∀ (i : α), ∃ y, e y = g i) → ∃ y, mapRange e he₀ y = g

Tactic:
intro h

Result:
case h.mpr
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ y, e y = g i
⊢ ∃ y, mapRange e he₀ y = g

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ ∀ (a : α), (↑g.support).indicator f a ≠ 0 → a ∈ g.support

Tactic:
aesop

Result:
no goals

Proof state:
case h.h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
i : α
⊢ e (if i ∈ ↑g.support then f i else 0) = g i

Tactic:
split_ifs <;> simp_all

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
⊢ mapRange e he₀ (onFinset g.support ((↑g.support).indicator f) ⋯) = g

Tactic:
ext i

Result:
case h.h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
i : α
⊢ (mapRange e he₀ (onFinset g.support ((↑g.support).indicator f) ⋯)) i = g i

Proof state:
case h.h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
i : α
⊢ (mapRange e he₀ (onFinset g.support ((↑g.support).indicator f) ⋯)) i = g i

Tactic:
simp only [mapRange_apply, onFinset_apply, Set.indicator_apply]

Result:
case h.h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
f : α → M
h : ∀ (i : α), e (f i) = g i
i : α
⊢ e (if i ∈ ↑g.support then f i else 0) = g i

Proof state:
case h
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∃ y, mapRange e he₀ y = g) ↔ ∀ (i : α), ∃ y, e y = g i

Tactic:
constructor

Result:
case h.mp
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∃ y, mapRange e he₀ y = g) → ∀ (i : α), ∃ y, e y = g i

case h.mpr
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
⊢ (∀ (i : α), ∃ y, e y = g i) → ∃ y, mapRange e he₀ y = g

Proof state:
case h.mpr
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
e : M → N
he₀ : e 0 = 0
g : α →₀ N
h : ∀ (i : α), ∃ y, e y = g i
⊢ ∃ y, mapRange e he₀ y = g

Tactic:
classical
choose f h using h
use onFinset g.support (Set.indicator g.support f) (by aesop)
ext i
simp only [mapRange_apply, onFinset_apply, Set.indicator_apply]
split_ifs <;> simp_all

Result:
no goals