-- Mathlib/Data/Matroid/Map.lean
lemma IsBasis.map {X : Set α} (hIX : M.IsBasis I X) {f : α → β} (hf) :
    (M.map f hf).IsBasis (f '' I) (f '' X)

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ¬(M.map f hf).Indep (insert (f e) (f '' I))

Tactic:
simp only [map_indep_iff, not_exists, not_and]

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ∀ (x : Set α), M.Indep x → ¬insert (f e) (f '' I) = f '' x

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ∀ (x : Set α), M.Indep x → ¬insert (f e) (f '' I) = f '' x

Tactic:
intro J hJ hins

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ False

Proof state:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
⊢ ∀ e ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))

Tactic:
rintro _ ⟨⟨e,he,rfl⟩, he'⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
⊢ (M.map f hf).Dep (insert (f e) (f '' I))

Proof state:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ insert (f e) (f '' I) ⊆ (M.map f hf).E

Tactic:
simpa [← image_insert_eq] using image_subset f hss

Result:
no goals

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

Tactic:
refine (hIX.indep.map f hf).isBasis_of_forall_insert (image_subset _ hIX.subset) ?_

Result:
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
⊢ ∀ e ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))

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

Tactic:
have hss := insert_subset (hIX.subset_ground he) hIX.indep.subset_ground

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ (M.map f hf).Dep (insert (f e) (f '' I))

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert (f e) (f '' I) = f '' J
⊢ False

Tactic:
rw [← image_insert_eq, hf.image_eq_image_iff hss hJ.subset_ground] at hins

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ False

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
J : Set α
hJ : M.Indep J
hins : insert e I = J
⊢ False

Tactic:
obtain rfl := hins

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
hJ : M.Indep (insert e I)
⊢ False

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ (M.map f hf).Dep (insert (f e) (f '' I))

Tactic:
rw [← not_indep_iff (by simpa [← image_insert_eq] using image_subset f hss)]

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
⊢ ¬(M.map f hf).Indep (insert (f e) (f '' I))

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
I : Set α
M : Matroid α
X : Set α
hIX : M.IsBasis I X
f : α → β
hf : InjOn f M.E
e : α
he : e ∈ X
he' : f e ∉ f '' I
hss : insert e I ⊆ M.E
hJ : M.Indep (insert e I)
⊢ False

Tactic:
exact he' (mem_image_of_mem f (hIX.mem_of_insert_indep he hJ))

Result:
no goals