-- Mathlib/Data/Matroid/Map.lean
lemma map_isBasis_iff {I X : Set α} (f : α → β) (hf) (hI : I ⊆ M.E) (hX : X ⊆ M.E) :
    (M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
⊢ M.IsBasis I X

Tactic:
refine hI'.isBasis_of_maximal_subset hss (fun J hJ hIJ hJX ↦ ?_)

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ J ⊆ I

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ J ⊆ I

Tactic:
have hIJ' := h.eq_of_subset_indep (hJ.map f hf) (image_subset f hIJ) (image_subset f hJX)

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : f '' I = f '' J
⊢ J ⊆ I

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.IsBasis I X

Tactic:
obtain rfl := hII'

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
⊢ M.IsBasis I X

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
⊢ (M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map hf⟩

Result:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ M.IsBasis I X

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : f '' I = f '' J
⊢ J ⊆ I

Tactic:
rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ'

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : I = J
⊢ J ⊆ I

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ M.IsBasis I X

Tactic:
obtain ⟨I', hI', hII'⟩ := map_indep_iff.1 h.indep

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : f '' I = f '' I'
⊢ M.IsBasis I X

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : f '' I = f '' I'
⊢ M.IsBasis I X

Tactic:
rw [hf.image_eq_image_iff hI hI'.subset_ground] at hII'

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.IsBasis I X

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
hIJ' : I = J
⊢ J ⊆ I

Tactic:
exact hIJ'.symm.subset

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
⊢ M.IsBasis I X

Tactic:
have hss := (hf.image_subset_image_iff hI hX).1 h.subset

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
⊢ M.IsBasis I X