Theorem: Matroid.rFin.contract_rFin (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C✝ D X Y Z : Set α
e f : α
h : M.rFin X
C : Set α
⊢ (M ／ C).rFin X
Tactic:
rw [← er_lt_top_iff] at *
State after:
α : Type u_1
M N : Matroid α
I J C✝ D X Y Z : Set α
e f : α
h : M.er X < ⊤
C : Set α
⊢ (M ／ C).er X < ⊤

State before:
α : Type u_1
M N : Matroid α
I J C✝ D X Y Z : Set α
e f : α
h : M.er X < ⊤
C : Set α
⊢ (M ／ C).er X < ⊤
Tactic:
exact (er_contract_le_er _ _ _).trans_lt h
State after:
no goals