Theorem: Matroid.relRank_add_er_eq (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X : Set α
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
Tactic:
obtain ⟨I, D, hIC, hD, -, hM⟩ := M.exists_eq_contract_indep_delete C
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X I D : Set α
hIC : M.Basis I (C ∩ M.E)
hD : D ⊆ (M ／ I).E
hM : M ／ C = M ／ I ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X I D : Set α
hIC : M.Basis I (C ∩ M.E)
hD : D ⊆ (M ／ I).E
hM : M ／ C = M ／ I ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
Tactic:
obtain ⟨J, hJ, rfl⟩ := hIC.exists_basis_inter_eq_of_superset
  (subset_union_right (s := X ∩ M.E)) (by simp)
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J✝ C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X D J : Set α
hJ : M.Basis J (X ∩ M.E ∪ C ∩ M.E)
hIC : M.Basis (J ∩ (C ∩ M.E)) (C ∩ M.E)
hD : D ⊆ (M ／ (J ∩ (C ∩ M.E))).E
hM : M ／ C = M ／ (J ∩ (C ∩ M.E)) ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J✝ C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X D J : Set α
hJ : M.Basis J (X ∩ M.E ∪ C ∩ M.E)
hIC : M.Basis (J ∩ (C ∩ M.E)) (C ∩ M.E)
hD : D ⊆ (M ／ (J ∩ (C ∩ M.E))).E
hM : M ／ C = M ／ (J ∩ (C ∩ M.E)) ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
Tactic:
rw [← relRank_inter_ground_left, ← relRank_inter_ground_right,
  hJ.basis'.relRank_eq_encard_diff hIC.basis', ← er_inter_ground_eq,
  ← hIC.encard, encard_diff_add_encard_inter, hJ.encard, ← union_inter_distrib_right,
  er_inter_ground_eq]
State after:
no goals

State before:
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X I D : Set α
hIC : M.Basis I (C ∩ M.E)
hD : D ⊆ (M ／ I).E
hM : M ／ C = M ／ I ＼ D
⊢ X ∩ M.E ∪ C ∩ M.E ⊆ M.E
Tactic:
simp
State after:
no goals