-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Bipartite (goal)
Goal:
V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
W₁ : Type u_2
W₂ : Type u_3
inst : DecidableRel fun (x1 : V) (x2 : Set V) ↦ x1 ∈ x2
hG : G.IsBipartiteWith s t
val : Sym2 V
a : V × V
property : Quot.mk (Sym2.Rel V) a ∈ G.edgeSet
val_1 : Sym2 V
a_1 : V × V
property_1 : Quot.mk (Sym2.Rel V) a_1 ∈ G.edgeSet
⊢ Eq.{u_1 + 1} (α := (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
      ((fun (x : (↑G.edgeSet : Type u_1)) ↦
          (match (motive :=
              (↑G.edgeSet : Type u_1) →
                (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
              x with
            | ⟨e, he⟩ =>
              Sym2.hrec (motive := fun (x : Sym2 V) ↦
                x ∈ G.edgeSet → (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
                (fun (u v : V) (h : s(u, v) ∈ G.edgeSet) ↦
                  ⋯.by_cases
                    (fun (h : (u, v).1 ∈ s ∧ (u, v).2 ∈ t) ↦
                      Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
                        Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
                          (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
                        s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u ⋯),
                          Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v ⋯))
                        ⋯)
                    fun (h : (u, v).1 ∈ t ∧ (u, v).2 ∈ s) ↦
                    Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
                      Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
                        (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
                      s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v ⋯),
                        Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) u ⋯))
                      ⋯)
                ⋯ e he :
            (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1)))
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) property))
      ((fun (x : (↑G.edgeSet : Type u_1)) ↦
          (match (motive :=
              (↑G.edgeSet : Type u_1) →
                (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
              x with
            | ⟨e, he⟩ =>
              Sym2.hrec (motive := fun (x : Sym2 V) ↦
                x ∈ G.edgeSet → (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
                (fun (u v : V) (h : s(u, v) ∈ G.edgeSet) ↦
                  ⋯.by_cases
                    (fun (h : (u, v).1 ∈ s ∧ (u, v).2 ∈ t) ↦
                      Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
                        Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
                          (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
                        s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u ⋯),
                          Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v ⋯))
                        ⋯)
                    fun (h : (u, v).1 ∈ t ∧ (u, v).2 ∈ s) ↦
                    Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
                      Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
                        (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
                      s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v ⋯),
                        Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) u ⋯))
                      ⋯)
                ⋯ e he :
            (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1)))
        (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) property_1)) →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) property =
      Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) property_1
have mk : Eq.{u_1 + 1} (α := (↑(edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) : Type u_1))
    (if x : (a.1, a.2).1 ∈ s ∧ (a.1, a.2).2 ∈ t then
      Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
        Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
          (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
        s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) a.1 sorry), Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) a.2 sorry))
        sorry
    else
      Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
        Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
          (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
        s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) a.2 sorry), Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) a.1 sorry))
        sorry)
    (if x : (a_1.1, a_1.2).1 ∈ s ∧ (a_1.1, a_1.2).2 ∈ t then
      Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
        Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
          (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
        s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) a_1.1 sorry),
          Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) a_1.2 sorry))
        sorry
    else
      Subtype.mk (p := fun (x : Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))) ↦
        Membership.mem (γ := Set (Sym2 ((↑s : Type u_1) ⊕ (↑t : Type u_1))))
          (edgeSet (completeBipartiteGraph (↑s : Type u_1) (↑t : Type u_1))) x)
        s(Sum.inl (Subtype.mk (p := fun (x : V) ↦ x ∈ s) a_1.2 sorry),
          Sum.inr (Subtype.mk (p := fun (x : V) ↦ x ∈ t) a_1.1 sorry))
        sorry) →
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a) property =
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) (Quot.mk (Sym2.Rel V) a_1) property_1
Tactic: change (if _ : _ then _ else _) = (if _ : _ then _ else _) → _