-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
h :
  Sum.inl ⁻¹' I =
    image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
      (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
      (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
          (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) false)
          ((fun (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              Sum.elim
                (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                s) ''
            (fun (a : α ⊕ β) ↦
                Sum.map
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : β) → ULift.{u, v} β)
                  a) ''
              I) :
        Set (bif false then ULift.{u, v} β else ULift.{v, u} α))
h₁ :
  Sum.inl ⁻¹' X =
    image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
      (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
      (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
          (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) false)
          ((fun (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              Sum.elim
                (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                s) ''
            (fun (a : α ⊕ β) ↦
                Sum.map
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : β) → ULift.{u, v} β)
                  a) ''
              X) :
        Set (bif false then ULift.{u, v} β else ULift.{v, u} α))
h₂ :
  Sum.inr ⁻¹' I =
    image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
      (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
      (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
          (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) true)
          ((fun (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              Sum.elim
                (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                  Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                s) ''
            (fun (a : α ⊕ β) ↦
                Sum.map
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                    (a : β) → ULift.{u, v} β)
                  a) ''
              I) :
        Set (bif true then ULift.{u, v} β else ULift.{v, u} α))
⊢ M.IsBasis
        (image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
          (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
              (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) false)
              ((fun (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  Sum.elim
                    (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                    (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                    s) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : β) → ULift.{u, v} β)
                      a) ''
                  I) :
            Set (bif false then ULift.{u, v} β else ULift.{v, u} α)))
        (image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
          (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
              (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) false)
              ((fun (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  Sum.elim
                    (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                    (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                    s) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : β) → ULift.{u, v} β)
                      a) ''
                  X) :
            Set (bif false then ULift.{u, v} β else ULift.{v, u} α))) ∧
      N.IsBasis
        (image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
          (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
              (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) true)
              ((fun (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  Sum.elim
                    (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                    (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                    s) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : β) → ULift.{u, v} β)
                      a) ''
                  I) :
            Set (bif true then ULift.{u, v} β else ULift.{v, u} α)))
        (image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
          (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
              (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) true)
              ((fun (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  Sum.elim
                    (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
                    (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                      Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
                    s) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }) :
                        (a : β) → ULift.{u, v} β)
                      a) ''
                  X) :
            Set (bif true then ULift.{u, v} β else ULift.{v, u} α))) ↔
    M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)
have h₃ : Sum.inr ⁻¹' X =
  image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
    (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦ a.down)
    (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
        (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) true)
        ((fun (s : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
            Sum.elim
              (fun (x : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
                Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) false x)
              (fun (x : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
                Sigma.mk (β := fun (b : Bool) ↦ bif b then ULift.{u, v} β else ULift.{v, u} α) true x)
              s) ''
          (fun (a : α ⊕ β) ↦
              Sum.map
                (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := sorry, right_inv := sorry }) :
                  (a : α) → ULift.{v, u} α)
                (⇑(Equiv.symm { toFun := ULift.down, invFun := ULift.up, left_inv := sorry, right_inv := sorry }) :
                  (a : β) → ULift.{u, v} β)
                a) ''
            X) :
      Set (bif true then ULift.{u, v} β else ULift.{v, u} α))
Tactic: convert! Iff.rfl