-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma mapEmbedding_isBasis_iff {f : α ↪ β} {I X : Set β} :
    (M.mapEmbedding f).IsBasis I X ↔ M.IsBasis (f ⁻¹' I) (f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range f

Proof state:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) → M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

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

Result:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set α
hIX : M.IsBasis I X
⊢ M.IsBasis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X)) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (M.mapEmbedding f).IsBasis I X ↔ M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

Tactic:
rw [mapEmbedding, map_isBasis_iff']

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) ↔ M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
X : Set α
hX : ⇑f '' X ⊆ range ⇑f
I : Set α
x✝ : M.IsBasis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X)) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X))
hIX : ⇑f '' I ⊆ ⇑f '' X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ ⇑f '' I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀

Tactic:
exact ⟨I, X, by simpa [preimage_image_eq _ f.injective] using hb⟩

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set α
hIX : M.IsBasis I X
⊢ M.IsBasis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X)) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f

Tactic:
simp [preimage_image_eq _ f.injective, image_subset f hIX.subset, hIX]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) ↔ M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

Tactic:
refine ⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) → M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
x✝ : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X)
hIX : I ⊆ X
hX : X ⊆ range ⇑f
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀

Proof state:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
x✝ : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X)
hIX : I ⊆ X
hX : X ⊆ range ⇑f
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀

Tactic:
obtain ⟨X, rfl⟩ := subset_range_iff_exists_image_eq.1 hX

Result:
case refine_2.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
X : Set α
x✝ : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' (⇑f '' X)) ∧ I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' (⇑f '' X))
hIX : I ⊆ ⇑f '' X
hX : ⇑f '' X ⊆ range ⇑f
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
X : Set α
hX : ⇑f '' X ⊆ range ⇑f
I : Set α
x✝ : M.IsBasis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X)) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X))
hIX : ⇑f '' I ⊆ ⇑f '' X
⊢ M.IsBasis I X ∧ ⇑f '' I = ⇑f '' I ∧ ⇑f '' X = ⇑f '' X

Tactic:
simpa [preimage_image_eq _ f.injective] using hb

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set β
X : Set α
x✝ : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' (⇑f '' X)) ∧ I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' (⇑f '' X))
hIX : I ⊆ ⇑f '' X
hX : ⇑f '' X ⊆ range ⇑f
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀

Tactic:
obtain ⟨I, -, rfl⟩ := subset_image_iff.1 hIX

Result:
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
X : Set α
hX : ⇑f '' X ⊆ range ⇑f
I : Set α
x✝ : M.IsBasis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X)) ∧ ⇑f '' I ⊆ ⇑f '' X ∧ ⇑f '' X ⊆ range ⇑f
hb : M.IsBasis (⇑f ⁻¹' (⇑f '' I)) (⇑f ⁻¹' (⇑f '' X))
hIX : ⇑f '' I ⊆ ⇑f '' X
⊢ ∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ ⇑f '' I = ⇑f '' I₀ ∧ ⇑f '' X = ⇑f '' X₀