[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
x✝ : α
⊢ invOfMemRange f ((fun a => { val := ↑f a, property := (_ : ↑f a ∈ Set.range ↑f) }) x✝) = x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
x✝ : ↑(Set.range ↑f)
⊢ (fun a => { val := ↑f a, property := (_ : ↑f a ∈ Set.range ↑f) }) (invOfMemRange f x✝) = x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
a : α
⊢ ↑(toEquivRange f).symm { val := ↑f a, property := (_ : ↑f a ∈ Set.range ↑f) } = a
[PROOFSTEP]
simp [Equiv.symm_apply_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
⊢ toEquivRange f = Equiv.ofInjective ↑f (_ : Injective ↑f)
[PROOFSTEP]
ext
[GOAL]
case H.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
x✝ : α
⊢ ↑(↑(toEquivRange f) x✝) = ↑(↑(Equiv.ofInjective ↑f (_ : Injective ↑f)) x✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ ↑(viaFintypeEmbedding e f) (↑f a) = ↑f (↑e a)
[PROOFSTEP]
rw [Equiv.Perm.viaFintypeEmbedding]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ ↑(extendDomain e (Function.Embedding.toEquivRange f)) (↑f a) = ↑f (↑e a)
[PROOFSTEP]
convert Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a
[GOAL]
α : Type u_1
β : Type u_2
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 }))
[PROOFSTEP]
simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]
[GOAL]
α : Type u_1
β : Type u_2
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 }))
[PROOFSTEP]
rw [Equiv.Perm.extendDomain_apply_subtype]
[GOAL]
α : Type u_1
β : Type u_2
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_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ↑f
⊢ b ∈ Set.range ↑f
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : ¬b ∈ Set.range ↑f
⊢ ↑(viaFintypeEmbedding e f) b = b
[PROOFSTEP]
rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e : Perm α
f : α ↪ β
inst✝¹ : DecidableEq α
inst✝ : Fintype β
⊢ ↑sign (viaFintypeEmbedding e f) = ↑sign e
[PROOFSTEP]
simp [Equiv.Perm.viaFintypeEmbedding]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(extendSubtype e) x = ↑(↑e { val := x, property := hx })
[PROOFSTEP]
dsimp only [extendSubtype]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(subtypeCongr e (toCompl e)) x = ↑(↑e { val := x, property := hx })
[PROOFSTEP]
simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(sumCompl fun x => q x) (Sum.map (↑e) (↑(toCompl e)) (↑(sumCompl fun x => p x).symm x)) =
    ↑(↑e { val := x, property := hx })
[PROOFSTEP]
rw [sumCompl_apply_symm_of_pos _ _ hx, Sum.map_inl, sumCompl_apply_inl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ q (↑(extendSubtype e) x)
[PROOFSTEP]
convert (e ⟨x, hx⟩).2
[GOAL]
case h.e'_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ ↑(extendSubtype e) x = ↑(↑e { val := x, property := hx })
[PROOFSTEP]
rw [e.extendSubtype_apply_of_mem _ hx]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ ↑(extendSubtype e) x = ↑(↑(toCompl e) { val := x, property := hx })
[PROOFSTEP]
dsimp only [extendSubtype]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ ↑(subtypeCongr e (toCompl e)) x = ↑(↑(toCompl e) { val := x, property := hx })
[PROOFSTEP]
simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ ↑(sumCompl fun x => q x) (Sum.map (↑e) (↑(toCompl e)) (↑(sumCompl fun x => p x).symm x)) =
    ↑(↑(toCompl e) { val := x, property := hx })
[PROOFSTEP]
rw [sumCompl_apply_symm_of_neg _ _ hx, Sum.map_inr, sumCompl_apply_inr]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ ¬q (↑(extendSubtype e) x)
[PROOFSTEP]
convert (e.toCompl ⟨x, hx⟩).2
[GOAL]
case h.e'_1.h.e'_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : DecidableEq β
e✝ : Perm α
f : α ↪ β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ ↑(extendSubtype e) x = ↑(↑(toCompl e) { val := x, property := hx })
[PROOFSTEP]
rw [e.extendSubtype_apply_of_not_mem _ hx]
