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

State before:
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
⊢ (M.map f hf).Basis I X ↔ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
h : (M.map f hf).Basis I X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀

case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
⊢ (∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).Basis I X

State before:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
⊢ (∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀) → (M.map f hf).Basis I X
Tactic:
rintro ⟨I, X, hIX, rfl, rfl⟩
State after:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I X : Set α
hIX : M.Basis I X
⊢ (M.map f hf).Basis (f '' I) (f '' X)

State before:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I X : Set α
hIX : M.Basis I X
⊢ (M.map f hf).Basis (f '' I) (f '' X)
Tactic:
exact hIX.map hf
State after:
no goals

State before:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set β
hf : InjOn f M.E
h : (M.map f hf).Basis I X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
Tactic:
obtain ⟨I, hI, rfl⟩ := subset_image_iff.1 h.indep.subset_ground
State after:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
X : Set β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ X = f '' X₀

State before:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
X : Set β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ X = f '' X₀
Tactic:
obtain ⟨X, hX, rfl⟩ := subset_image_iff.1 h.subset_ground
State after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) ((fun a => f a) '' X)
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀

State before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : (M.map f hf).Basis ((fun a => f a) '' I) ((fun a => f a) '' X)
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀
Tactic:
rw [map_basis_iff _ _ hI hX] at h
State after:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.Basis I X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀

State before:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
X : Set α
hX : X ⊆ M.E
h : M.Basis I X
⊢ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ (fun a => f a) '' I = f '' I₀ ∧ (fun a => f a) '' X = f '' X₀
Tactic:
exact ⟨I, X, h, rfl, rfl⟩
State after:
no goals