Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: 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

pp: 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

pp: 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

pp: 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

Tactic:
<;>

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