[GOAL]
α : Type u_1
inst✝¹ : Add α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (x + y) = ↑(equivShrink α).symm x + ↑(equivShrink α).symm y
[PROOFSTEP]
rw [Equiv.add_def]
[GOAL]
α : Type u_1
inst✝¹ : Add α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x + ↑(equivShrink α).symm y)) =
    ↑(equivShrink α).symm x + ↑(equivShrink α).symm y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Add α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x + y) = ↑(equivShrink α) x + ↑(equivShrink α) y
[PROOFSTEP]
rw [Equiv.add_def]
[GOAL]
α : Type u_1
inst✝¹ : Add α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x + y) =
    ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x) + ↑(equivShrink α).symm (↑(equivShrink α) y))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (x * y) = ↑(equivShrink α).symm x * ↑(equivShrink α).symm y
[PROOFSTEP]
rw [Equiv.mul_def]
[GOAL]
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x * ↑(equivShrink α).symm y)) =
    ↑(equivShrink α).symm x * ↑(equivShrink α).symm y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x * y) = ↑(equivShrink α) x * ↑(equivShrink α) y
[PROOFSTEP]
rw [Equiv.mul_def]
[GOAL]
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x * y) =
    ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x) * ↑(equivShrink α).symm (↑(equivShrink α) y))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Sub α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (x - y) = ↑(equivShrink α).symm x - ↑(equivShrink α).symm y
[PROOFSTEP]
rw [Equiv.sub_def]
[GOAL]
α : Type u_1
inst✝¹ : Sub α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x - ↑(equivShrink α).symm y)) =
    ↑(equivShrink α).symm x - ↑(equivShrink α).symm y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Sub α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x - y) = ↑(equivShrink α) x - ↑(equivShrink α) y
[PROOFSTEP]
rw [Equiv.sub_def]
[GOAL]
α : Type u_1
inst✝¹ : Sub α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x - y) =
    ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x) - ↑(equivShrink α).symm (↑(equivShrink α) y))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (x / y) = ↑(equivShrink α).symm x / ↑(equivShrink α).symm y
[PROOFSTEP]
rw [Equiv.div_def]
[GOAL]
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x / ↑(equivShrink α).symm y)) =
    ↑(equivShrink α).symm x / ↑(equivShrink α).symm y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x / y) = ↑(equivShrink α) x / ↑(equivShrink α) y
[PROOFSTEP]
rw [Equiv.div_def]
[GOAL]
α : Type u_1
inst✝¹ : Div α
inst✝ : Small.{u_2, u_1} α
x y : α
⊢ ↑(equivShrink α) (x / y) =
    ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x) / ↑(equivShrink α).symm (↑(equivShrink α) y))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Neg α
inst✝ : Small.{u_2, u_1} α
x : Shrink α
⊢ ↑(equivShrink α).symm (-x) = -↑(equivShrink α).symm x
[PROOFSTEP]
rw [Equiv.neg_def]
[GOAL]
α : Type u_1
inst✝¹ : Neg α
inst✝ : Small.{u_2, u_1} α
x : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (-↑(equivShrink α).symm x)) = -↑(equivShrink α).symm x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Neg α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ ↑(equivShrink α) (-x) = -↑(equivShrink α) x
[PROOFSTEP]
rw [Equiv.neg_def]
[GOAL]
α : Type u_1
inst✝¹ : Neg α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ ↑(equivShrink α) (-x) = ↑(equivShrink α).symm.symm (-↑(equivShrink α).symm (↑(equivShrink α) x))
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : Shrink α
⊢ ↑(equivShrink α).symm x⁻¹ = (↑(equivShrink α).symm x)⁻¹
[PROOFSTEP]
rw [Equiv.inv_def]
[GOAL]
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : Shrink α
⊢ ↑(equivShrink α).symm (↑(equivShrink α).symm.symm (↑(equivShrink α).symm x)⁻¹) = (↑(equivShrink α).symm x)⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ ↑(equivShrink α) x⁻¹ = (↑(equivShrink α) x)⁻¹
[PROOFSTEP]
rw [Equiv.inv_def]
[GOAL]
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ ↑(equivShrink α) x⁻¹ = ↑(equivShrink α).symm.symm (↑(equivShrink α).symm (↑(equivShrink α) x))⁻¹
[PROOFSTEP]
simp


[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]