α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
⊢ (if h : ↑f a ∈ map f v.support then
      (fun h =>
          ↑v (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)))
        h
    else (fun h => 0) h) =
    ↑v a
α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
⊢ ↑(embDomain f v) (↑f a) = ↑v a
change dite _ _ _ = _
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ↑f a ∈ map f v.support
h : a ∈ v.support
⊢ (fun h => ↑v (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)))
      h✝ =
    ↑v a

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ¬↑f a ∈ map f v.support
h : ¬a ∈ v.support
⊢ (fun h => 0) h✝ = ↑v a
α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
⊢ (if h : ↑f a ∈ map f v.support then
      (fun h =>
          ↑v (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)))
        h
    else (fun h => 0) h) =
    ↑v a
split_ifs with h <;> rw [Finset.mem_map' f] at h
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ↑f a ∈ map f v.support
h : a ∈ v.support
⊢ Embedding.toFun f
      (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)) =
    Embedding.toFun f a
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ↑f a ∈ map f v.support
h : a ∈ v.support
⊢ (fun h => ↑v (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)))
      h✝ =
    ↑v a
refine' congr_arg (v : α → M) (f.inj' _)
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ↑f a ∈ map f v.support
h : a ∈ v.support
⊢ Embedding.toFun f
      (choose (fun a₁ => ↑f a₁ = ↑f a) v.support (_ : ∃! a_1, a_1 ∈ v.support ∧ (fun a₁ => ↑f a₁ = ↑f a) a_1)) =
    Embedding.toFun f a
exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.193446
ι : Type ?u.193449
M : Type u_3
M' : Type ?u.193455
N : Type ?u.193458
P : Type ?u.193461
G : Type ?u.193464
H : Type ?u.193467
R : Type ?u.193470
S : Type ?u.193473
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
a : α
h✝ : ¬↑f a ∈ map f v.support
h : ¬a ∈ v.support
⊢ (fun h => 0) h✝ = ↑v a
exact (not_mem_support_iff.1 h).symm