[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ Disjoint (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst)
    (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd)
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ ∀ ⦃a : γ⦄,
    a ∈ Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst →
      ¬a ∈ Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd
[PROOFSTEP]
rintro _ ⟨a, h⟩ ⟨b, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h :
  ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst a =
    ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd b
⊢ False
[PROOFSTEP]
simp only [trans_apply, inl_apply, inr_apply] at h 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h : ↑(Function.Embedding.trans inl f) a = ↑(Function.Embedding.trans inr f) b
⊢ False
[PROOFSTEP]
have : Sum.inl a = Sum.inr b := f.injective h
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h : ↑(Function.Embedding.trans inl f) a = ↑(Function.Embedding.trans inr f) b
this : Sum.inl a = Sum.inr b
⊢ False
[PROOFSTEP]
simp only at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
⊢ Function.Injective fun x =>
    match x with
    | Sum.inl a => ↑f a
    | Sum.inr b => ↑g b
[PROOFSTEP]
rintro (a₁ | b₁) (a₂ | b₂) f_eq
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ a₂ : α
f_eq :
  (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inl a₁) =
    (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq 
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ : α
b₂ : β
f_eq :
  (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inl a₁) =
    (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq 
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ : β
a₂ : α
f_eq :
  (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inr b₁) =
    (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq 
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ b₂ : β
f_eq :
  (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inr b₁) =
    (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq 
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ a₂ : α
f_eq : ↑f a₁ = ↑f a₂
⊢ Sum.inl a₁ = Sum.inl a₂
[PROOFSTEP]
rw [f.injective f_eq]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ : α
b₂ : β
f_eq : ↑f a₁ = ↑g b₂
⊢ Sum.inl a₁ = Sum.inr b₂
[PROOFSTEP]
exfalso
[GOAL]
case inl.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ : α
b₂ : β
f_eq : ↑f a₁ = ↑g b₂
⊢ False
[PROOFSTEP]
refine disj.le_bot ⟨⟨a₁, f_eq⟩, ⟨b₂, by simp [f_eq]⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ : α
b₂ : β
f_eq : ↑f a₁ = ↑g b₂
⊢ ↑(f, g).snd b₂ = ↑g b₂
[PROOFSTEP]
simp [f_eq]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ : β
a₂ : α
f_eq : ↑g b₁ = ↑f a₂
⊢ Sum.inr b₁ = Sum.inl a₂
[PROOFSTEP]
exfalso
[GOAL]
case inr.inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ : β
a₂ : α
f_eq : ↑g b₁ = ↑f a₂
⊢ False
[PROOFSTEP]
exact disj.le_bot ⟨⟨a₂, rfl⟩, ⟨b₁, f_eq⟩⟩
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ b₂ : β
f_eq : ↑g b₁ = ↑g b₂
⊢ Sum.inr b₁ = Sum.inr b₂
[PROOFSTEP]
rw [g.injective f_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ (fun x =>
        match x with
        | { val := (f, g), property := disj } =>
          {
            toFun := fun x =>
              match x with
              | Sum.inl a => ↑f a
              | Sum.inr b => ↑g b,
            inj' :=
              (_ :
                ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                  (fun x =>
                          match x with
                          | Sum.inl a => ↑f a
                          | Sum.inr b => ↑g b)
                        a₁ =
                      (fun x =>
                          match x with
                          | Sum.inl a => ↑f a
                          | Sum.inr b => ↑g b)
                        a₂ →
                    a₁ = a₂) })
      ((fun f =>
          { val := (Function.Embedding.trans inl f, Function.Embedding.trans inr f),
            property :=
              (_ :
                Disjoint (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst)
                  (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd)) })
        f) =
    f
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ {
      toFun := fun x =>
        match x with
        | Sum.inl a => ↑(Function.Embedding.trans inl f) a
        | Sum.inr b => ↑(Function.Embedding.trans inr f) b,
      inj' :=
        (_ :
          ∀ ⦃a₁ a₂ : α ⊕ β⦄,
            ((match a₁ with
                | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                | Sum.inr b => ↑(Function.Embedding.trans inr f) b) =
                match a₂ with
                | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                | Sum.inr b => ↑(Function.Embedding.trans inr f) b) →
              a₁ = a₂) } =
    f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
x : α ⊕ β
⊢ ↑{
          toFun := fun x =>
            match x with
            | Sum.inl a => ↑(Function.Embedding.trans inl f) a
            | Sum.inr b => ↑(Function.Embedding.trans inr f) b,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                ((match a₁ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) =
                    match a₂ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) →
                  a₁ = a₂) }
      x =
    ↑f x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : α
⊢ ↑{
          toFun := fun x =>
            match x with
            | Sum.inl a => ↑(Function.Embedding.trans inl f) a
            | Sum.inr b => ↑(Function.Embedding.trans inr f) b,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                ((match a₁ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) =
                    match a₂ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) →
                  a₁ = a₂) }
      (Sum.inl val✝) =
    ↑f (Sum.inl val✝)
[PROOFSTEP]
simp!
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : β
⊢ ↑{
          toFun := fun x =>
            match x with
            | Sum.inl a => ↑(Function.Embedding.trans inl f) a
            | Sum.inr b => ↑(Function.Embedding.trans inr f) b,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                ((match a₁ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) =
                    match a₂ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) →
                  a₁ = a₂) }
      (Sum.inr val✝) =
    ↑f (Sum.inr val✝)
[PROOFSTEP]
simp!
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
property✝ : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
⊢ (fun f =>
        { val := (Function.Embedding.trans inl f, Function.Embedding.trans inr f),
          property :=
            (_ :
              Disjoint (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst)
                (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd)) })
      ((fun x =>
          match x with
          | { val := (f, g), property := disj } =>
            {
              toFun := fun x =>
                match x with
                | Sum.inl a => ↑f a
                | Sum.inr b => ↑g b,
              inj' :=
                (_ :
                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                    (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₁ =
                        (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₂ →
                      a₁ = a₂) })
        { val := (f, g), property := property✝ }) =
    { val := (f, g), property := property✝ }
[PROOFSTEP]
simp only [Prod.mk.inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
property✝ : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
⊢ {
      val :=
        (Function.Embedding.trans inl
            {
              toFun := fun x =>
                match x with
                | Sum.inl a => ↑f a
                | Sum.inr b => ↑g b,
              inj' :=
                (_ :
                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                    (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₁ =
                        (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₂ →
                      a₁ = a₂) },
          Function.Embedding.trans inr
            {
              toFun := fun x =>
                match x with
                | Sum.inl a => ↑f a
                | Sum.inr b => ↑g b,
              inj' :=
                (_ :
                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                    (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₁ =
                        (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₂ →
                      a₁ = a₂) }),
      property :=
        (_ :
          Disjoint
            (Set.range
              ↑(Function.Embedding.trans inl
                      ((fun x =>
                          match x with
                          | { val := (f, g), property := disj } =>
                            {
                              toFun := fun x =>
                                match x with
                                | Sum.inl a => ↑f a
                                | Sum.inr b => ↑g b,
                              inj' :=
                                (_ :
                                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                                    (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₁ =
                                        (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₂ →
                                      a₁ = a₂) })
                        { val := (f, g), property := property✝ }),
                    Function.Embedding.trans inr
                      ((fun x =>
                          match x with
                          | { val := (f, g), property := disj } =>
                            {
                              toFun := fun x =>
                                match x with
                                | Sum.inl a => ↑f a
                                | Sum.inr b => ↑g b,
                              inj' :=
                                (_ :
                                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                                    (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₁ =
                                        (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₂ →
                                      a₁ = a₂) })
                        { val := (f, g), property := property✝ })).fst)
            (Set.range
              ↑(Function.Embedding.trans inl
                      ((fun x =>
                          match x with
                          | { val := (f, g), property := disj } =>
                            {
                              toFun := fun x =>
                                match x with
                                | Sum.inl a => ↑f a
                                | Sum.inr b => ↑g b,
                              inj' :=
                                (_ :
                                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                                    (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₁ =
                                        (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₂ →
                                      a₁ = a₂) })
                        { val := (f, g), property := property✝ }),
                    Function.Embedding.trans inr
                      ((fun x =>
                          match x with
                          | { val := (f, g), property := disj } =>
                            {
                              toFun := fun x =>
                                match x with
                                | Sum.inl a => ↑f a
                                | Sum.inr b => ↑g b,
                              inj' :=
                                (_ :
                                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                                    (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₁ =
                                        (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₂ →
                                      a₁ = a₂) })
                        { val := (f, g), property := property✝ })).snd)) } =
    { val := (f, g), property := property✝ }
[PROOFSTEP]
constructor
[GOAL]
α : Type u_1
β : Type u_2
bs : Set β
x : { f // ∀ (a : α), ↑f a ∈ bs }
⊢ (fun f => { val := Function.Embedding.trans f (subtype fun x => x ∈ bs), property := (_ : ∀ (a : α), ↑(↑f a) ∈ bs) })
      ((fun f => Function.Embedding.codRestrict bs ↑f (_ : ∀ (a : α), ↑↑f a ∈ bs)) x) =
    x
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
β : Type u_2
bs : Set β
x : { f // ∀ (a : α), ↑f a ∈ bs }
x✝ : α
⊢ ↑↑((fun f =>
              { val := Function.Embedding.trans f (subtype fun x => x ∈ bs),
                property := (_ : ∀ (a : α), ↑(↑f a) ∈ bs) })
            ((fun f => Function.Embedding.codRestrict bs ↑f (_ : ∀ (a : α), ↑↑f a ∈ bs)) x))
      x✝ =
    ↑↑x x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
bs : Set β
x : α ↪ ↑bs
⊢ (fun f => Function.Embedding.codRestrict bs ↑f (_ : ∀ (a : α), ↑↑f a ∈ bs))
      ((fun f =>
          { val := Function.Embedding.trans f (subtype fun x => x ∈ bs), property := (_ : ∀ (a : α), ↑(↑f a) ∈ bs) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u_1
β : Type u_2
bs : Set β
x : α ↪ ↑bs
x✝ : α
⊢ ↑(↑((fun f => Function.Embedding.codRestrict bs ↑f (_ : ∀ (a : α), ↑↑f a ∈ bs))
            ((fun f =>
                { val := Function.Embedding.trans f (subtype fun x => x ∈ bs),
                  property := (_ : ∀ (a : α), ↑(↑f a) ∈ bs) })
              x))
        x✝) =
    ↑(↑x x✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
⊢ (fun b => Disjoint (Set.range ↑a) (Set.range ↑b)) = fun f => ∀ (a_1 : β), ↑f a_1 ∈ (Set.range ↑a)ᶜ
[PROOFSTEP]
ext f
[GOAL]
case h.a
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
f : β ↪ γ
⊢ Disjoint (Set.range ↑a) (Set.range ↑f) ↔ ∀ (a_1 : β), ↑f a_1 ∈ (Set.range ↑a)ᶜ
[PROOFSTEP]
rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
⊢ (fun x =>
        { toFun := fun x_1 => x, inj' := (_ : ∀ (x_1 x_2 : α), (fun x_3 => x) x_1 = (fun x_3 => x) x_2 → x_1 = x_2) })
      ((fun f => ↑f default) x✝) =
    x✝
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ ↑((fun x =>
            { toFun := fun x_1 => x,
              inj' := (_ : ∀ (x_1 x_2 : α), (fun x_3 => x) x_1 = (fun x_3 => x) x_2 → x_1 = x_2) })
          ((fun f => ↑f default) x✝))
      x =
    ↑x✝ x
[PROOFSTEP]
simp_rw [Function.Embedding.coeFn_mk]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ ↑x✝ default = ↑x✝ x
[PROOFSTEP]
congr 1
[GOAL]
case h.h.e_6.h
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ default = x
[PROOFSTEP]
exact Subsingleton.elim _ x
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : β
⊢ (fun f => ↑f default)
      ((fun x =>
          { toFun := fun x_1 => x, inj' := (_ : ∀ (x_1 x_2 : α), (fun x_3 => x) x_1 = (fun x_3 => x) x_2 → x_1 = x_2) })
        x✝) =
    x✝
[PROOFSTEP]
simp
