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

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

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) ↔ M.Dep (⇑f.symm '' D)
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 : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) → M.Dep (⇑f.symm '' D)
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.Dep I
⊢ M.Dep (⇑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.Dep I
⊢ M.Dep (⇑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 : α ≃ β
D : Set β
h : M.Dep (⇑f.symm '' D)
⊢ D = ⇑f '' (⇑f.symm '' D)
Tactic:
simp
State after:
no goals