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

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).rFin X
hC : M.rFin C
⊢ M.rFin (X ∪ C)
Tactic:
rw [← er_lt_top_iff, ← M.relRank_add_er_eq, relRank]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).rFin X
hC : M.rFin C
⊢ (M ／ C).er X + M.er C < ⊤

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).rFin X
hC : M.rFin C
⊢ (M ／ C).er X + M.er C < ⊤
Tactic:
rw [← er_ne_top_iff] at hC hX
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).er X ≠ ⊤
hC : M.er C ≠ ⊤
⊢ (M ／ C).er X + M.er C < ⊤

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).er X ≠ ⊤
hC : M.er C ≠ ⊤
⊢ (M ／ C).er X + M.er C < ⊤
Tactic:
rw [lt_top_iff_ne_top, Ne, WithTop.add_eq_top, not_or]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).er X ≠ ⊤
hC : M.er C ≠ ⊤
⊢ ¬(M ／ C).er X = ⊤ ∧ ¬M.er C = ⊤

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).er X ≠ ⊤
hC : M.er C ≠ ⊤
⊢ ¬(M ／ C).er X = ⊤ ∧ ¬M.er C = ⊤
Tactic:
exact ⟨hX, hC⟩
State after:
no goals