Theorem: Matroid.rFin.union (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 : α
hX : M.rFin X
hY : M.rFin Y
⊢ M.rFin (X ∪ Y)
Tactic:
rw [← er_lt_top_iff] at *
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er (X ∪ Y) < ⊤

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er (X ∪ Y) < ⊤
Tactic:
apply (M.er_union_le_er_add_er X Y).trans_lt
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er X + M.er Y < ⊤

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er X + M.er Y < ⊤
Tactic:
rw [WithTop.add_lt_top]
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er X < ⊤ ∧ M.er Y < ⊤

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er X < ⊤ ∧ M.er Y < ⊤
Tactic:
exact ⟨hX, hY⟩
State after:
no goals