-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : 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} α) ↦
        ((Equiv.ulift : (a : bif false then ULift.{u, v} β else ULift.{v, u} α) → α) a : α))
      (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 (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                  (a : ULift.{v, u} α ⊕ ULift.{u, v} β) → (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                a) ''
            (fun (a : α ⊕ β) ↦
                Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
              I) :
        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} α) ↦
        ((Equiv.ulift : (a : bif true then ULift.{u, v} β else ULift.{v, u} α) → β) a : β))
      (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 (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
              (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                  (a : ULift.{v, u} α ⊕ ULift.{u, v} β) → (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                a) ''
            (fun (a : α ⊕ β) ↦
                Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                  (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
              I) :
        Set (bif true then ULift.{u, v} β else ULift.{v, u} α))
⊢ M.Indep
        (image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
            ((Equiv.ulift : (a : bif false then ULift.{u, v} β else ULift.{v, u} α) → α) a : α))
          (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 (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                      (a : ULift.{v, u} α ⊕ ULift.{u, v} β) →
                        (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                    a) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
                  I) :
            Set (bif false then ULift.{u, v} β else ULift.{v, u} α))) ∧
      N.Indep
        (image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
          (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
            ((Equiv.ulift : (a : bif true then ULift.{u, v} β else ULift.{v, u} α) → β) a : β))
          (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 (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                  (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                      (a : ULift.{v, u} α ⊕ ULift.{u, v} β) →
                        (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                    a) ''
                (fun (a : α ⊕ β) ↦
                    Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                      (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
                  I) :
            Set (bif true then ULift.{u, v} β else ULift.{v, u} α))) ↔
    M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl