Theorem: Matroid.Basis.map (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Basis (f '' I) (f '' X)
Tactic:
refine (hIX.indep.map f hf).basis_of_forall_insert (image_subset _ hIX.subset) ?_
State after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis I X
f : α → β
hf : InjOn f M.E
⊢ ∀ e ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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'⟩
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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))

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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))

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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)]
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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))

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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]
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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
State after:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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

State before:
case intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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))
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
X : Set α
hIX : M.Basis 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
State after:
no goals