Theorem: Matroid.le_er_iff (Matroid/Rank.lean)

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
⊢ n ≤ M.er X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic:
refine' ⟨fun h ↦ _, fun ⟨I, hIX, hI, hIc⟩ ↦ _⟩
State after:
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.er X

State before:
case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ n ≤ M.er X
Tactic:
rw [← hIc, ← hI.er]
State after:
case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ M.er I ≤ M.er X

State before:
case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ M.er I ≤ M.er X
Tactic:
exact M.er_mono hIX
State after:
no goals

State before:
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' X
State after:
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
J : Set α
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

State before:
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : n ≤ M.er X
J : Set α
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic:
rw [← hJ.encard] at h
State after:
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
J : Set α
h : n ≤ J.encard
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

State before:
case refine'_1.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
J : Set α
h : n ≤ J.encard
hJ : M.Basis' J X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
Tactic:
obtain ⟨I, hIJ, rfl⟩ :=  exists_subset_encard_eq h
State after:
case refine'_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
e f : α
J : Set α
hJ : M.Basis' J X
I : Set α
hIJ : I ⊆ J
h : I.encard ≤ J.encard
⊢ ∃ I_1 ⊆ X, M.Indep I_1 ∧ I_1.encard = I.encard

State before:
case refine'_1.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
e f : α
J : Set α
hJ : M.Basis' J X
I : Set α
hIJ : I ⊆ J
h : I.encard ≤ J.encard
⊢ ∃ I_1 ⊆ X, M.Indep I_1 ∧ I_1.encard = I.encard
Tactic:
exact ⟨_, hIJ.trans hJ.subset, hJ.indep.subset hIJ, rfl⟩
State after:
no goals