-- Module: Mathlib.Data.Fin.Tuple.Embedding
Goal:
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
pos :
  ∀ (hi : i = 0),
    Eq (α := α)
      (((fun
                  (x :
                    (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1)) ↦
                (match (motive :=
                    (↑{x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a ≠ b} :
                        Type u_1) →
                      Fin 2 ↪ α)
                    x with
                  | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
                  Fin 2 ↪ α))
              ((fun (e : Fin 2 ↪ α) ↦
                  (Subtype.mk (p := fun (x : α × α) ↦
                      Membership.mem (γ := Set (α × α))
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b}
                        x)
                      ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
                    { x : α × α //
                      Membership.mem (γ := Set (α × α))
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b}
                        x }))
                e) :
            (a : Fin 2) → α)
          i :
        α)
      ((e : (a : Fin 2) → α) i : α)
neg :
  ∀ (hi : ¬i = 0),
    Eq (α := α)
      (((fun
                  (x :
                    (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1)) ↦
                (match (motive :=
                    (↑{x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a ≠ b} :
                        Type u_1) →
                      Fin 2 ↪ α)
                    x with
                  | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
                  Fin 2 ↪ α))
              ((fun (e : Fin 2 ↪ α) ↦
                  (Subtype.mk (p := fun (x : α × α) ↦
                      Membership.mem (γ := Set (α × α))
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b}
                        x)
                      ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
                    { x : α × α //
                      Membership.mem (γ := Set (α × α))
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b}
                        x }))
                e) :
            (a : Fin 2) → α)
          i :
        α)
      ((e : (a : Fin 2) → α) i : α)
⊢ Eq (α := α)
    (((fun
                (x :
                  (↑{x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b} :
                    Type u_1)) ↦
              (match (motive :=
                  (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1) →
                    Fin 2 ↪ α)
                  x with
                | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
                Fin 2 ↪ α))
            ((fun (e : Fin 2 ↪ α) ↦
                (Subtype.mk (p := fun (x : α × α) ↦
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x)
                    ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
                  { x : α × α //
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x }))
              e) :
          (a : Fin 2) → α)
        i :
      α)
    ((e : (a : Fin 2) → α) i : α)

Tactic:
by_cases hi : i = 0