Theorem: Matroid.Indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
B B' I I' J K X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
obtain ⟨K, hK, hIK⟩ := hI.subset_basis_of_subset (subset_union_left (s := I) (t := J))
State after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk

State before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have hsk := (hK.indep.subset_skew_diff hIK)
State after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew I (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk

State before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew I (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
rw [skew_iff_cl_skew_left] at hsk
State after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk

State before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have' hdj := hsk.disjoint_of_indep_subset_right (hK.indep.diff _) Subset.rfl
State after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk

State before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have hb' : ∀ ⦃B⦄, M.Basis B (M.cl I) →
    (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard := by
  intro B hB
  rw [(hb hB).1.erk_dual_restrict, union_diff_left,
    ← encard_diff_add_encard_inter (J \ (K \ I)) B, add_comm, inter_comm _ B,
    inter_diff_distrib_left, (hdj.mono_left hB.subset).inter_eq, diff_empty]
State after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk

State before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have hind : ∀ Y, (M ↾ (Y ∪ J)).Indep (K \ I) := by
  intro Y
  rw [restrict_indep_iff, and_iff_right (hK.indep.diff I), diff_subset_iff, union_comm Y,
    ← union_assoc]
  exact hK.subset.trans subset_union_left
State after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk

State before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
have hI'b := hII'.symm ▸ hI'.basis_cl
State after:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
hI'b : M.Basis I' (M.cl I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk

State before:
case intro.intro
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
hI'b : M.Basis I' (M.cl I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
Tactic:
rw [← (hind I).contract_er_dual_eq,  ← (hind I').contract_er_dual_eq,
  restrict_contract_eq_contract_restrict _ (hb hI.basis_cl).2,
  restrict_contract_eq_contract_restrict _ (hb hI'b).2,
  union_diff_distrib, sdiff_eq_left.2 disjoint_sdiff_right,
  union_diff_distrib, sdiff_eq_left.2 (hdj.mono_left hI'b.subset), hb' hI.basis_cl, hb' hI'b]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
⊢ ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
Tactic:
refine fun B hB ↦ ⟨Indep.basis_of_subset_of_subset_cl ?_ ?_ ?_, ?_⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ (M ／ (K \ I)).Indep B

case refine_2
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ⊆ B ∪ J \ (K \ I)

case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ (M ／ (K \ I)).cl B

case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K \ I ⊆ B ∪ J

State before:
case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K \ I ⊆ B ∪ J
Tactic:
rw [diff_subset_iff, union_comm B, ← union_assoc]
State after:
case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K ⊆ I ∪ J ∪ B

State before:
case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K ⊆ I ∪ J ∪ B
Tactic:
exact hK.subset.trans <| subset_union_left
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ (M ／ (K \ I)).Indep B
Tactic:
rw [(hK.indep.diff _).contract_indep_iff]
State after:
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ Disjoint B (K \ I) ∧ M.Indep (B ∪ K \ I)

State before:
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ Disjoint B (K \ I) ∧ M.Indep (B ∪ K \ I)
Tactic:
exact ⟨hdj.mono_left hB.subset,
  hsk.union_indep_of_indep_subsets hB.indep hB.subset (hK.indep.diff _) Subset.rfl⟩
State after:
no goals

State before:
case refine_2
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ⊆ B ∪ J \ (K \ I)
Tactic:
exact subset_union_left
State after:
no goals

State before:
case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ (M ／ (K \ I)).cl B
Tactic:
rw [contract_cl_eq, subset_diff, disjoint_union_left, and_iff_left disjoint_sdiff_left,
  and_iff_left (hdj.mono_left hB.subset), ← cl_union_cl_left_eq, hB.cl_eq_cl, cl_cl,
  cl_union_cl_left_eq, union_diff_self, union_eq_self_of_subset_left hIK, hK.cl_eq_cl]
State after:
case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ M.cl (I ∪ J)

State before:
case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ M.cl (I ∪ J)
Tactic:
exact union_subset (hB.subset.trans (M.cl_subset_cl subset_union_left))
  (M.subset_cl_of_subset (diff_subset.trans subset_union_right))
State after:
no goals

State before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
⊢ ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Tactic:
intro B hB
State after:
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
B : Set α
hB : M.Basis B (M.cl I)
⊢ (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard

State before:
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
B : Set α
hB : M.Basis B (M.cl I)
⊢ (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Tactic:
rw [(hb hB).1.erk_dual_restrict, union_diff_left,
  ← encard_diff_add_encard_inter (J \ (K \ I)) B, add_comm, inter_comm _ B,
  inter_diff_distrib_left, (hdj.mono_left hB.subset).inter_eq, diff_empty]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
⊢ ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
Tactic:
intro Y
State after:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y✝ : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Y : Set α
⊢ (M ↾ (Y ∪ J)).Indep (K \ I)

State before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y✝ : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Y : Set α
⊢ (M ↾ (Y ∪ J)).Indep (K \ I)
Tactic:
rw [restrict_indep_iff, and_iff_right (hK.indep.diff I), diff_subset_iff, union_comm Y,
  ← union_assoc]
State after:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y✝ : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Y : Set α
⊢ K ⊆ I ∪ J ∪ Y

State before:
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y✝ : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
Y : Set α
⊢ K ⊆ I ∪ J ∪ Y
Tactic:
exact hK.subset.trans subset_union_left
State after:
no goals