Theorem: Matroid.indep_iff_er_eq_encard_of_finite (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 : α
hI : I.Finite
⊢ M.Indep I ↔ M.er I = I.encard
Tactic:
refine' ⟨fun h ↦ by rw [h.er], fun h ↦ _⟩
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
⊢ M.Indep I

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

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep I
Tactic:
rw [← hI.eq_of_subset_of_encard_le hJ.subset]
State after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep J

case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ I.encard ≤ J.encard

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ I.encard ≤ J.encard
Tactic:
rw [← h, ← hJ.er_eq_encard]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.Indep I
⊢ M.er I = I.encard
Tactic:
rw [h.er]
State after:
no goals

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hI : I.Finite
h : M.er I = I.encard
J : Set α
hJ : M.Basis' J I
⊢ M.Indep J
Tactic:
exact hJ.indep
State after:
no goals