Theorem: Matroid.mapSetEmbedding_indep_iff' (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.mapSetEmbedding f).Indep I ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
Tactic:
simp only [mapSetEmbedding_indep_iff, subset_range_iff_exists_image_eq]
State after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀

case mpr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀) → M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I

State before:
case mpr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀) → M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I
Tactic:
rintro ⟨I, hI, rfl⟩
State after:
case mpr.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑I
⊢ M.Indep ↑(⇑f ⁻¹' (⇑f '' I)) ∧ ∃ t, ⇑f '' t = ⇑f '' I

State before:
case mpr.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑I
⊢ M.Indep ↑(⇑f ⁻¹' (⇑f '' I)) ∧ ∃ t, ⇑f '' t = ⇑f '' I
Tactic:
rw [preimage_image_eq _ f.injective]
State after:
case mpr.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑I
⊢ M.Indep ↑I ∧ ∃ t, ⇑f '' t = ⇑f '' I

State before:
case mpr.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑I
⊢ M.Indep ↑I ∧ ∃ t, ⇑f '' t = ⇑f '' I
Tactic:
exact ⟨hI, _, rfl⟩
State after:
no goals

State before:
case mp
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set β
⊢ (M.Indep ↑(⇑f ⁻¹' I) ∧ ∃ t, ⇑f '' t = I) → ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
Tactic:
rintro ⟨hI, I, rfl⟩
State after:
case mp.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑(⇑f ⁻¹' (⇑f '' I))
⊢ ∃ I₀, M.Indep ↑I₀ ∧ ⇑f '' I = ⇑f '' I₀

State before:
case mp.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑(⇑f ⁻¹' (⇑f '' I))
⊢ ∃ I₀, M.Indep ↑I₀ ∧ ⇑f '' I = ⇑f '' I₀
Tactic:
exact ⟨I, by rwa [preimage_image_eq _ f.injective] at hI, rfl⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep ↑(⇑f ⁻¹' (⇑f '' I))
⊢ M.Indep ↑I
Tactic:
rwa [preimage_image_eq _ f.injective] at hI
State after:
no goals