Theorem: Matroid.uniqueBaseOn_finiteRk (Matroid/Constructions/Basic.lean)

State before:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn I E).FiniteRk
Tactic:
rw [← uniqueBaseOn_inter_ground_eq]
State after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).FiniteRk

State before:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).FiniteRk
Tactic:
refine ⟨I ∩ E, ?_⟩
State after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).Base (I ∩ E) ∧ (I ∩ E).Finite

State before:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (uniqueBaseOn (I ∩ E) E).Base (I ∩ E) ∧ (I ∩ E).Finite
Tactic:
rw [uniqueBaseOn_base_iff inter_subset_right, and_iff_right rfl]
State after:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite

State before:
α : Type u_1
E I : Set α
hI : I.Finite
⊢ (I ∩ E).Finite
Tactic:
exact hI.subset inter_subset_left
State after:
no goals