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

State before:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ (M.map f hf).Base B ↔ ∃ B₀, M.Base B₀ ∧ B = f '' B₀
Tactic:
rw [base_iff_maximal_indep, map_indep_iff]
State after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
⊢ ((∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I) ↔
    ∃ B₀, M.Base B₀ ∧ B = f '' B₀

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

case refine_2
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : ∃ B₀, M.Base B₀ ∧ B = f '' B₀
⊢ (∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I

State before:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : ∃ B₀, M.Base B₀ ∧ B = f '' B₀
⊢ (∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
Tactic:
obtain ⟨B₀, hB, rfl⟩ := h
State after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
⊢ (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I

State before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
⊢ (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
Tactic:
refine ⟨⟨B₀, hB.indep, rfl⟩, fun I hI hB₀I ↦ ?_⟩
State after:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set β
hI : (M.map f hf).Indep I
hB₀I : f '' B₀ ⊆ I
⊢ f '' B₀ = I

State before:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set β
hI : (M.map f hf).Indep I
hB₀I : f '' B₀ ⊆ I
⊢ f '' B₀ = I
Tactic:
obtain ⟨I, hI', rfl⟩ := map_indep_iff.1 hI
State after:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set α
hI' : M.Indep I
hI : (M.map f hf).Indep (f '' I)
hB₀I : f '' B₀ ⊆ f '' I
⊢ f '' B₀ = f '' I

State before:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set α
hI' : M.Indep I
hI : (M.map f hf).Indep (f '' I)
hB₀I : f '' B₀ ⊆ f '' I
⊢ f '' B₀ = f '' I
Tactic:
rw [hf.image_subset_image_iff hB.subset_ground hI'.subset_ground] at hB₀I
State after:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set α
hI' : M.Indep I
hI : (M.map f hf).Indep (f '' I)
hB₀I : B₀ ⊆ I
⊢ f '' B₀ = f '' I

State before:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB : M.Base B₀
I : Set α
hI' : M.Indep I
hI : (M.map f hf).Indep (f '' I)
hB₀I : B₀ ⊆ I
⊢ f '' B₀ = f '' I
Tactic:
rw [hB.eq_of_subset_indep hI' hB₀I]
State after:
no goals

State before:
case refine_1
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
x✝ : (∃ I₀, M.Indep I₀ ∧ B = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
h : ∃ I₀, M.Indep I₀ ∧ B = f '' I₀
hB : ∀ (I : Set β), (M.map f hf).Indep I → B ⊆ I → B = I
⊢ ∃ B₀, M.Base B₀ ∧ B = f '' B₀
Tactic:
obtain ⟨B₀, hB₀, rfl⟩ := h
State after:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
⊢ ∃ B₀_1, M.Base B₀_1 ∧ f '' B₀ = f '' B₀_1

State before:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
⊢ ∃ B₀_1, M.Base B₀_1 ∧ f '' B₀ = f '' B₀_1
Tactic:
refine ⟨_, hB₀.base_of_maximal fun J hJ hB₀J ↦ ?_, rfl⟩
State after:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B₀ = J

State before:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
hB : ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B₀ = J
Tactic:
specialize hB (f '' J) ((map_image_indep_iff hJ.subset_ground).2 hJ) (image_subset _ hB₀J)
State after:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
hB : f '' B₀ = f '' J
⊢ B₀ = J

State before:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
B₀ : Set α
hB₀ : M.Indep B₀
x✝ : (∃ I₀, M.Indep I₀ ∧ f '' B₀ = f '' I₀) ∧ ∀ (I : Set β), (M.map f hf).Indep I → f '' B₀ ⊆ I → f '' B₀ = I
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
hB : f '' B₀ = f '' J
⊢ B₀ = J
Tactic:
rwa [hf.image_eq_image_iff hB₀.subset_ground hJ.subset_ground] at hB
State after:
no goals