-- Mathlib/Data/Matroid/Map.lean
lemma mapSetEmbedding_indep_iff' {f : M.E ↪ β} {I : Set β} :
    (M.mapSetEmbedding f).Indep I ↔ ∃ (I₀ : Set M.E), M.Indep ↑I₀ ∧ I = f '' I₀

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' I)
⊢ M.Indep (Subtype.val '' (⇑f ⁻¹' (⇑f '' I))) ∧ ∃ t, ⇑f '' t = ⇑f '' I

Tactic:
rw [preimage_image_eq _ f.injective]

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' I)
⊢ M.Indep (Subtype.val '' I) ∧ ∃ t, ⇑f '' t = ⇑f '' I

Proof state:
case mp.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' (⇑f ⁻¹' (⇑f '' I)))
⊢ ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ ⇑f '' I = ⇑f '' I₀

Tactic:
exact ⟨I, by rwa [preimage_image_eq _ f.injective] at hI, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' (⇑f ⁻¹' (⇑f '' I)))
⊢ M.Indep (Subtype.val '' I)

Tactic:
rwa [preimage_image_eq _ f.injective] at hI

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep (Subtype.val '' (⇑f ⁻¹' I)) ∧ ∃ t, ⇑f '' t = I) ↔ ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep (Subtype.val '' (⇑f ⁻¹' I)) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

case mpr
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀) → M.Indep (Subtype.val '' (⇑f ⁻¹' I)) ∧ ∃ t, ⇑f '' t = I

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.mapSetEmbedding f).Indep I ↔ ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

Tactic:
simp only [mapSetEmbedding_indep_iff, subset_range_iff_exists_image_eq]

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep (Subtype.val '' (⇑f ⁻¹' I)) ∧ ∃ t, ⇑f '' t = I) ↔ ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

Proof state:
case mp
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep (Subtype.val '' (⇑f ⁻¹' I)) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

Tactic:
rintro ⟨hI, I, rfl⟩

Result:
case mp.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' (⇑f ⁻¹' (⇑f '' I)))
⊢ ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ ⇑f '' I = ⇑f '' I₀

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' I)
⊢ M.Indep (Subtype.val '' I) ∧ ∃ t, ⇑f '' t = ⇑f '' I

Tactic:
exact ⟨hI, _, rfl⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀) → M.Indep (Subtype.val '' (⇑f ⁻¹' I)) ∧ ∃ t, ⇑f '' t = I

Tactic:
rintro ⟨I, hI, rfl⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' I)
⊢ M.Indep (Subtype.val '' (⇑f ⁻¹' (⇑f '' I))) ∧ ∃ t, ⇑f '' t = ⇑f '' I