Theorem: Matroid.map_image_base_iff (Matroid/Map.lean)

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

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀) ↔ M.Base B
Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨B, h, rfl⟩⟩
State after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.Base J
hIJ : f '' B = f '' J
⊢ M.Base B

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.Base J
hIJ : f '' B = f '' J
⊢ M.Base B
Tactic:
rw [hf.image_eq_image_iff hB hJ.subset_ground] at hIJ
State after:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.Base J
hIJ : B = J
⊢ M.Base B

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.Base B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.Base J
hIJ : B = J
⊢ M.Base B
Tactic:
rwa [hIJ]
State after:
no goals