-- Mathlib/Data/Matroid/Map.lean
lemma map_isBasis_iff' {I X : Set β} {hf} :
    (M.map f hf).IsBasis I X ↔ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

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

Tactic:
rw [map_isBasis_iff _ _ hI hX] at h

Result:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.IsBasis I X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀

Proof state:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
X : Set β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ X = f '' X₀

Tactic:
obtain ⟨X, hX, rfl⟩ := subset_image_iff.1 h.subset_ground

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

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
⊢ (M.map f hf).IsBasis (f '' I) (f '' X)

Tactic:
exact hIX.map hf

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).IsBasis I X

Tactic:
rintro ⟨I, X, hIX, rfl, rfl⟩

Result:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I X : Set α
hIX : M.IsBasis I X
⊢ (M.map f hf).IsBasis (f '' I) (f '' X)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
⊢ (M.map f hf).IsBasis I X ↔ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
h : (M.map f hf).IsBasis I X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

case refine_2
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).IsBasis I X

Proof state:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I X : Set β
hf : InjOn f M.E
h : (M.map f hf).IsBasis I X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

Tactic:
obtain ⟨I, hI, rfl⟩ := subset_image_iff.1 h.indep.subset_ground

Result:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
X : Set β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ X = f '' X₀

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.IsBasis I X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ f '' I = f '' I₀ ∧ f '' X = f '' X₀

Tactic:
exact ⟨I, X, h, rfl, rfl⟩

Result:
no goals