-- Module: Mathlib.Combinatorics.Matroid.Map
Goal:
α : Type u_1
β : Type u_2
f_1 : α → β
E I : Set α
M_1 : Matroid α
N : Matroid β
M : Matroid α
f : Embedding.{u_1 + 1, u_2 + 1} (↑M.E : Type u_1) β
inl :
  ∀ (f : Embedding.{u_1 + 1, u_2 + 1} (↑(emptyOn α).E : Type u_1) β),
    ∃ (M : Matroid β),
      range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1)) (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) = M.E ∧
        ∀ (I : Set β),
          M.Indep I ↔
            (fun (I : Set β) ↦
                (emptyOn α).Indep
                    (image (α := { x : α // x ∈ (emptyOn α).E }) (Subtype.val (p := fun (x : α) ↦ x ∈ (emptyOn α).E))
                      ((⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β) ⁻¹' I)) ∧
                  I ⊆
                    range.{u_2, u_1 + 1} (ι := (↑(emptyOn α).E : Type u_1))
                      (⇑f : (a : (↑(emptyOn α).E : Type u_1)) → β))
              I
inr inr₁ :
  ∀ (e : α) (he : e ∈ M.E),
    ∃ (M_2 : Matroid β),
      range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β) = M_2.E ∧
        ∀ (I : Set β),
          M_2.Indep I ↔
            (fun (I : Set β) ↦
                M.Indep
                    (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                      ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                  I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
              I
inr₂ :
  ∀ (e : α) (he : e ∈ M.E),
    Nonempty.{u_1 + 1} (↑M.E : Type u_1) →
      ∃ (M_2 : Matroid β),
        range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β) = M_2.E ∧
          ∀ (I : Set β),
            M_2.Indep I ↔
              (fun (I : Set β) ↦
                  M.Indep
                      (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                        ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                    I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
                I
inr₃ :
  ∀ (e : α) (he : e ∈ M.E),
    Nonempty.{u_1 + 1} (↑M.E : Type u_1) →
      Nonempty α →
        ∃ (M_2 : Matroid β),
          range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β) = M_2.E ∧
            ∀ (I : Set β),
              M_2.Indep I ↔
                (fun (I : Set β) ↦
                    M.Indep
                        (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                          ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                      I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
                  I
inr₄ :
  ∀ (e : α) (he : e ∈ M.E) (x : Nonempty.{u_1 + 1} (↑M.E : Type u_1)),
    Nonempty α →
      ∀ (I : Set β),
        Indep
            (M.comapOn (range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
              fun (x_2 : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_2) : α))
            I ↔
          (fun (I : Set β) ↦
              M.Indep
                  (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                    ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
            I
inr₅ :
  ∀ (e : α) (he : e ∈ M.E) (x : Nonempty.{u_1 + 1} (↑M.E : Type u_1)),
    Nonempty α →
      ∀ (I : Set β),
        (∃ (t : Set (↑M.E : Type u_1)), (⇑f : (a : (↑M.E : Type u_1)) → β) '' t = I) →
          (M.Indep ((fun (x_2 : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_2) : α)) '' I) ∧
              InjOn.{u_2, u_1} (β := α) (fun (x_2 : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_2) : α))
                I ↔
            M.Indep
              (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)))
inr₆ :
  ∀ (e : α) (he : e ∈ M.E) (x : Nonempty.{u_1 + 1} (↑M.E : Type u_1)),
    Nonempty α →
      ∀ (I : Set (↑M.E : Type u_1)),
        M.Indep
              ((fun (x_2 : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_2) : α)) ''
                (⇑f : (a : (↑M.E : Type u_1)) → β) '' I) ∧
            InjOn.{u_2, u_1} (β := α) (fun (x_2 : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_2) : α))
              ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) ↔
          M.Indep
            (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
              (preimage.{u_1, u_2} (β := β) (⇑f : (a : (↑M.E : Type u_1)) → β)
                ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)))
inr₇ :
  ∀ (e : α) (he : e ∈ M.E) (x : Nonempty.{u_1 + 1} (↑M.E : Type u_1)),
    Nonempty α →
      ∀ (I : Set (↑M.E : Type u_1)),
        M.Indep ↑I →
          InjOn.{u_2, u_1} (β := α) (fun (x_2 : β) ↦ (↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_2) : α))
            ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I)
inr₈ :
  ∀ (e : α) (he : e ∈ M.E) (x : Nonempty.{u_1 + 1} (↑M.E : Type u_1)),
    Nonempty α →
      ∀ (I : Set (↑M.E : Type u_1)) ⦃x_2 : β⦄
        (hx : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) x_2) ⦃y : β⦄
        (hy : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) y),
        Eq.{u_1 + 1} (α := α)
            ((fun (x_3 : β) ↦ ((↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_3) : α) : α)) x_2)
            ((fun (x_3 : β) ↦ ((↑(invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_3) : α) : α)) y) →
          x_2 = y
inr₉ :
  ∀ (e : α) (he : e ∈ M.E) (x : Nonempty.{u_1 + 1} (↑M.E : Type u_1)),
    Nonempty α →
      ∀ (I : Set (↑M.E : Type u_1)) ⦃x_2 : β⦄
        (hx : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) x_2) ⦃y : β⦄
        (hy : Membership.mem (γ := Set β) ((⇑f : (a : (↑M.E : Type u_1)) → β) '' I) y),
        Eq.{max 1 (u_1 + 1)} (α := { x : α // x ∈ M.E }) (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ x_2)
            (invFunOn (⇑f : (a : (↑M.E : Type u_1)) → β) univ y) →
          x_2 = y
⊢ ∃ (M_2 : Matroid β),
    range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β) = M_2.E ∧
      ∀ (I : Set β),
        M_2.Indep I ↔
          (fun (I : Set β) ↦
              M.Indep
                  (image (α := { x : α // x ∈ M.E }) (Subtype.val (p := fun (x : α) ↦ x ∈ M.E))
                    ((⇑f : (a : (↑M.E : Type u_1)) → β) ⁻¹' I)) ∧
                I ⊆ range.{u_2, u_1 + 1} (ι := (↑M.E : Type u_1)) (⇑f : (a : (↑M.E : Type u_1)) → β))
            I

Tactic:
classical
    obtain (rfl | ⟨⟨e, he⟩⟩) := eq_emptyOn_or_nonempty M
    · refine ⟨emptyOn β, ?_⟩
      simp only [emptyOn_ground] at f
      simp [range_eq_empty f, subset_empty_iff]
    have _ : Nonempty M.E := ⟨⟨e,he⟩⟩
    have _ : Nonempty α := ⟨e⟩
    refine ⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), rfl, ?_⟩
    simp_rw [comapOn_indep_iff, ← and_assoc, and_congr_left_iff, subset_range_iff_exists_image_eq]
    rintro _ ⟨I, rfl⟩
    rw [← image_image, InjOn.invFunOn_image f.injective.injOn (subset_univ _),
      preimage_image_eq _ f.injective, and_iff_left_iff_imp]
    rintro - x hx y hy
    simp only [Subtype.val_inj]
    exact (invFunOn_injOn_image f univ) (image_mono (subset_univ I) hx)
      (image_mono (subset_univ I) hy)

Premises used: Set.image_image, Subtype.val_inj, Matroid.comapOn_indep_iff, Matroid.emptyOn_ground, Matroid.eq_emptyOn_or_nonempty, Set.subset_range_iff_exists_image_eq, and_congr_left_iff, and_assoc, Function.Embedding.injective, Set.preimage_image_eq, Set.subset_empty_iff, and_iff_left_iff_imp, rfl