Theorem: Matroid.er_union_eq_of_subset_of_er_le_er (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 : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)
Tactic:
obtain hX' | hX' := em (M.rFin X)
State after:
case inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : M.rFin X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)

case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)

State before:
case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)
Tactic:
rw [er_eq_top_iff.2, er_eq_top_iff.2]
State after:
case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (Y ∪ Z)

case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (X ∪ Z)

State before:
case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (X ∪ Z)
Tactic:
exact not_rFin_of_er_ge hX' (M.er_mono subset_union_left)
State after:
no goals

State before:
case inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : M.rFin X
⊢ M.er (X ∪ Z) = M.er (Y ∪ Z)
Tactic:
rw [← er_union_cl_left_eq, hX'.cl_eq_cl_of_subset_of_er_ge_er hXY hr, er_union_cl_left_eq]
State after:
no goals

State before:
case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (Y ∪ Z)
Tactic:
exact not_rFin_of_er_ge hX' (M.er_mono (subset_union_of_subset_left hXY _))
State after:
no goals