-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sum_isBasis_iff {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))

Proof state:
α : 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 <;> exact ext <| by simp

Result:
no goals

Proof state:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ ∀ (x : β),
    x ∈ Sum.inr ⁻¹' X ↔
      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)))

Tactic:
simp

Result:
no goals

Proof state:
α : 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)

Tactic:
simp only [Matroid.sum, mapEquiv_isBasis_iff, Equiv.sumCongr_symm,
  Equiv.sumCongr_apply, Equiv.symm_symm, sigma_isBasis_iff, Bool.forall_bool, Equiv.ulift_apply,
  Equiv.sumEquivSigmaBool, Equiv.coe_fn_mk, Equiv.ulift]

Result:
α : 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)