Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ M.IsBasis
        ((fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I)
        ((fun a ↦ a.down) ''
          Sigma.mk false ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X) ∧
      N.IsBasis
        ((fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                I)
        ((fun a ↦ a.down) ''
          Sigma.mk true ⁻¹'
            (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
              (fun a ↦
                  Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                    (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
                X) ↔
    M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)

Tactic:
convert! Iff.rfl

Goal state after:
case e'_2.e'_1.e'_3
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' I =
    (fun a ↦ a.down) ''
      Sigma.mk false ⁻¹'
        (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
          (fun a ↦
              Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
            I

case e'_2.e'_1.e'_4
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ Sum.inl ⁻¹' X =
    (fun a ↦ a.down) ''
      Sigma.mk false ⁻¹'
        (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
          (fun a ↦
              Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
            X

case e'_2.e'_2.e'_3
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' I =
    (fun a ↦ a.down) ''
      Sigma.mk true ⁻¹'
        (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
          (fun a ↦
              Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
            I

case e'_2.e'_2.e'_4
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ Sum.inr ⁻¹' X =
    (fun a ↦ a.down) ''
      Sigma.mk true ⁻¹'
        (fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) ''
          (fun a ↦
              Sum.map (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm)
                (⇑{ toFun := ULift.down, invFun := ULift.up, left_inv := ⋯, right_inv := ⋯ }.symm) a) ''
            X