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

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
B : Set α
hB : M.Base B
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).Base (f '' B)
Tactic:
rw [map_base_iff]
State after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
B : Set α
hB : M.Base B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
B : Set α
hB : M.Base B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
Tactic:
exact ⟨B, hB, rfl⟩
State after:
no goals