-- Module: Mathlib.Combinatorics.Matroid.Sum
Goal:
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
refine_1 :
  ∀ (hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)),
    (I ⊆ X ∧
        (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
          X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E) →
      ∀ (hIX : I ⊆ X)
        (h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t)
        (h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E) (i : ι) (I₀ : Set (α i)) (hI₀ : (M i).Indep I₀)
        (hI₀X : I₀ ⊆ Sigma.mk (β := α) i ⁻¹' X) (hII₀ : Sigma.mk (β := α) i ⁻¹' I ⊆ I₀), Sigma.mk (β := α) i ⁻¹' I = I₀
refine_2 :
  ∀ (hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)),
    (I ⊆ X ∧
        (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
          X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E) →
      ∀ (hIX : I ⊆ X)
        (h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t)
        (h' : X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E) (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E
refine_3 :
  ∀ (hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)),
    ((∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
        (∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
          ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E) →
      ∀ (hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X)
        (h' :
          ∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t)
        (h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E), I ⊆ X
refine_4 :
  ∀ (hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)),
    ((∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
        (∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
          ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E) →
      ∀ (hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X)
        (h' :
          ∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t)
        (h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E) ⦃t : Set ((i : ι) × α i)⦄,
        (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t
refine_5 :
  ∀ (hI : ∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)),
    ((∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
        (∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
          ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E) →
      ∀ (hIX : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X)
        (h' :
          ∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t)
        (h'' : ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E), X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' I)) →
    ((I ⊆ X ∧
        (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk (β := α) i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
          X ⊆ Set.sigma (α := α) univ fun (i : ι) ↦ (M i).E) ↔
      (∀ (x : ι), Sigma.mk (β := α) x ⁻¹' I ⊆ Sigma.mk (β := α) x ⁻¹' X) ∧
        (∀ (x : ι) ⦃t : Set (α x)⦄,
            (M x).Indep t →
              t ⊆ Sigma.mk (β := α) x ⁻¹' X → Sigma.mk (β := α) x ⁻¹' I ⊆ t → Sigma.mk (β := α) x ⁻¹' I = t) ∧
          ∀ (x : ι), Sigma.mk (β := α) x ⁻¹' X ⊆ (M x).E)

Tactic:
refine fun hI ↦ ⟨fun ⟨hIX, h, h'⟩ ↦ ⟨fun i ↦ preimage_mono hIX, fun i I₀ hI₀ hI₀X hII₀ ↦ ?_, ?_⟩,
    fun ⟨hIX, h', h''⟩ ↦ ⟨?_, ?_, ?_⟩⟩