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

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
⊢ (M.mapEquiv f).Base B ↔ M.Base (⇑f.symm '' B)
Tactic:
rw [mapEquiv_eq_map, map_base_iff]
State after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.Base B₀ ∧ B = ⇑f '' B₀) ↔ M.Base (⇑f.symm '' B)

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.Base B₀ ∧ B = ⇑f '' B₀) ↔ M.Base (⇑f.symm '' B)
Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.Base B₀ ∧ B = ⇑f '' B₀) → M.Base (⇑f.symm '' B)
Tactic:
rintro ⟨I, hI, rfl⟩
State after:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Base I
⊢ M.Base (⇑f.symm '' (⇑f '' I))

State before:
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Base I
⊢ M.Base (⇑f.symm '' (⇑f '' I))
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
B : Set β
h : M.Base (⇑f.symm '' B)
⊢ B = ⇑f '' (⇑f.symm '' B)
Tactic:
simp
State after:
no goals