-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Map (goal)
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
⊢ ∃ (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
have 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
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)