α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ↑f
⊢ ↑(extendDomain e (Function.Embedding.toEquivRange f)) b =
    ↑f (↑e (Function.Injective.invOfMemRange (_ : Function.Injective ↑f) { val := b, property := h }))
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ↑f
⊢ ↑(viaFintypeEmbedding e f) b = ↑f (↑e (Function.Embedding.invOfMemRange f { val := b, property := h }))
simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ↑f
⊢ ↑(↑(Function.Embedding.toEquivRange f)
        (↑e (↑(Function.Embedding.toEquivRange f).symm { val := b, property := ?h }))) =
    ↑f (↑e (Function.Injective.invOfMemRange (_ : Function.Injective ↑f) { val := b, property := h }))

case h
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ↑f
⊢ b ∈ Set.range ↑f
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ↑f
⊢ ↑(extendDomain e (Function.Embedding.toEquivRange f)) b =
    ↑f (↑e (Function.Injective.invOfMemRange (_ : Function.Injective ↑f) { val := b, property := h }))
rw [Equiv.Perm.extendDomain_apply_subtype]
no goals
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ↑f
⊢ ↑(↑(Function.Embedding.toEquivRange f)
        (↑e (↑(Function.Embedding.toEquivRange f).symm { val := b, property := ?h }))) =
    ↑f (↑e (Function.Injective.invOfMemRange (_ : Function.Injective ↑f) { val := b, property := h }))

case h
α : Type u_2
β : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ↑f
⊢ b ∈ Set.range ↑f
congr