Theorem: Matroid.er_add_er_eq_er_union_add_conn (Matroid/Connectivity.lean)

State before:
α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝ Y✝ : Set α
M : Matroid α
X Y : Set α
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
State after:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y

State before:
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis' Y
State after:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y

State before:
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
obtain ⟨B, hB⟩ := M.exists_basis' (I ∪ J)
State after:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y

State before:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
have hB' : M.Basis' B (X ∪ Y) := by
  rw [basis'_iff_basis_cl, ← cl_cl_union_cl_eq_cl_union, ← hI.cl_eq_cl, ← hJ.cl_eq_cl,
     cl_cl_union_cl_eq_cl_union, ← hB.cl_eq_cl]
  exact ⟨hB.indep.basis_cl, hB.subset.trans (union_subset_union hI.subset hJ.subset)⟩
State after:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
hB' : M.Basis' B (X ∪ Y)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y

State before:
case intro.intro.intro
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
hB' : M.Basis' B (X ∪ Y)
⊢ M.er X + M.er Y = M.er (X ∪ Y) + M.conn X Y
Tactic:
rw [hI.conn_eq hJ, ← hI.encard, ← hJ.encard, ← encard_union_add_encard_inter, ← hB'.encard,
  ← (base_restrict_iff'.2 hB).encard_compl_eq, restrict_ground_eq, ← add_assoc, add_comm B.encard,
  add_assoc, add_comm B.encard, encard_diff_add_encard_of_subset hB.subset, add_comm]
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.Basis' B (X ∪ Y)
Tactic:
rw [basis'_iff_basis_cl, ← cl_cl_union_cl_eq_cl_union, ← hI.cl_eq_cl, ← hJ.cl_eq_cl,
   cl_cl_union_cl_eq_cl_union, ← hB.cl_eq_cl]
State after:
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.Basis B (M.cl B) ∧ B ⊆ X ∪ Y

State before:
α : Type u_1
M✝ : Matroid α
B✝ B' I✝ I' J✝ K X✝ Y✝ : Set α
M : Matroid α
X Y I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
B : Set α
hB : M.Basis' B (I ∪ J)
⊢ M.Basis B (M.cl B) ∧ B ⊆ X ∪ Y
Tactic:
exact ⟨hB.indep.basis_cl, hB.subset.trans (union_subset_union hI.subset hJ.subset)⟩
State after:
no goals