Theorem: Matroid.rFin_ground_iff_finiteRk (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 : α
⊢ M.rFin M.E ↔ M.FiniteRk
Tactic:
obtain ⟨B, hB⟩ := M.exists_base
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 : α
B : Set α
hB : M.Base B
⊢ M.rFin M.E ↔ M.FiniteRk

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 : α
B : Set α
hB : M.Base B
⊢ M.rFin M.E ↔ M.FiniteRk
Tactic:
use fun h => ⟨⟨B, hB, h.finite_of_indep_subset hB.indep hB.subset_ground⟩⟩
State after:
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → M.rFin M.E

State before:
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → M.rFin M.E
Tactic:
simp_rw [rFin_iff (rfl.subset), basis_ground_iff]
State after:
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → ∃ I, M.Base I ∧ I.Finite

State before:
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → ∃ I, M.Base I ∧ I.Finite
Tactic:
exact fun ⟨h⟩ ↦ h
State after:
no goals