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

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
State after:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z

State before:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans hXY)
State after:
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J✝ C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z

State before:
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J✝ C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain ⟨K, hK, hJK⟩ := hJ.indep.subset_basis'_of_subset (hJ.subset.trans hYZ)
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 α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
K : Set α
hK : M.Basis' K Z
hJK : J ⊆ K
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z

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 α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
K : Set α
hK : M.Basis' K Z
hJK : J ⊆ K
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain rfl := hI.inter_eq_of_subset_indep hIJ hJ.indep
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 α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
J : Set α
hJ : M.Basis' J Y
K : Set α
hK : M.Basis' K Z
hJK : J ⊆ K
hI : M.Basis' (J ∩ X) X
hIJ : J ∩ X ⊆ J
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z

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 α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
J : Set α
hJ : M.Basis' J Y
K : Set α
hK : M.Basis' K Z
hJK : J ⊆ K
hI : M.Basis' (J ∩ X) X
hIJ : J ∩ X ⊆ J
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain rfl := hJ.inter_eq_of_subset_indep hJK hK.indep
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 α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z

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 α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
rw [hJ.relRank_eq_encard_diff_of_subset hXY hI, hK.relRank_eq_encard_diff_of_subset hYZ hJ,
  hK.relRank_eq_encard_diff_of_subset (hXY.trans hYZ)
  (by rwa [inter_assoc, inter_eq_self_of_subset_right hXY] at hI),
  ← encard_union_eq, diff_eq, diff_eq, inter_assoc, ← inter_union_distrib_left,
  inter_union_distrib_right, union_compl_self, univ_inter, ← compl_inter,
  inter_eq_self_of_subset_left hXY, diff_eq]
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 α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ Disjoint ((K ∩ Y) \ X) (K \ Y)

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 α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ Disjoint ((K ∩ Y) \ X) (K \ Y)
Tactic:
exact disjoint_of_subset_left (diff_subset.trans inter_subset_right)
  disjoint_sdiff_right
State after:
no goals

State before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ M.Basis' (K ∩ X) X
Tactic:
rwa [inter_assoc, inter_eq_self_of_subset_right hXY] at hI
State after:
no goals