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

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (M.mapEmbedding f).Indep I ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Tactic:
rw [mapEmbedding, map_indep_iff]
State after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Tactic:
refine ⟨?_, fun ⟨h,h'⟩ ↦ ⟨f ⁻¹' I, h, by rwa [eq_comm, image_preimage_eq_iff]⟩⟩
State after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
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.Indep I
⊢ M.Indep (⇑f ⁻¹' (⇑f '' I)) ∧ ⇑f '' I ⊆ range ⇑f

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.Indep I
⊢ M.Indep (⇑f ⁻¹' (⇑f '' I)) ∧ ⇑f '' I ⊆ range ⇑f
Tactic:
rw [preimage_image_eq _ f.injective]
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.Indep I
⊢ M.Indep I ∧ ⇑f '' I ⊆ range ⇑f

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.Indep I
⊢ M.Indep I ∧ ⇑f '' I ⊆ range ⇑f
Tactic:
exact ⟨hI, image_subset_range _ _⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ↪ β
I : Set β
x✝ : M.Indep (⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
h : M.Indep (⇑f ⁻¹' I)
h' : I ⊆ range ⇑f
⊢ I = ⇑f '' (⇑f ⁻¹' I)
Tactic:
rwa [eq_comm, image_preimage_eq_iff]
State after:
no goals