-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ (M.sum N).IsBasis I X ↔ M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)
have simp : 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 := 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) ''
                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 := 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 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 := 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) ''
                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 := 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} α))) ↔
  M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)
Tactic: simp only [Matroid.sum, mapEquiv_isBasis_iff, Equiv.sumCongr_symm,
    Equiv.sumCongr_apply, Equiv.symm_symm, sigma_isBasis_iff, Bool.forall_bool,
    Equiv.sumEquivSigmaBool, Equiv.coe_fn_mk, Equiv.ulift]