Lean4
/-- Given `M : Matroid α`, the `IndepMatroid α` whose independent sets are
the subsets of `M.E` that are disjoint from some base of `M` -/
@[simps]
def dualIndepMatroid (M : Matroid α) : IndepMatroid α
where
E := M.E
Indep I := I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B
indep_empty := ⟨empty_subset M.E, M.exists_isBase.imp (fun _ hB ↦ ⟨hB, empty_disjoint _⟩)⟩
indep_subset := by
rintro I J ⟨hJE, B, hB, hJB⟩ hIJ
exact ⟨hIJ.trans hJE, ⟨B, hB, disjoint_of_subset_left hIJ hJB⟩⟩
indep_aug := by
rintro I X ⟨hIE, B, hB, hIB⟩ hI_not_max hX_max
have hXE := hX_max.1.1
have hB' := (isBase_compl_iff_maximal_disjoint_isBase hXE).mpr hX_max
set B' := M.E \ X with hX
have hI := (not_iff_not.mpr (isBase_compl_iff_maximal_disjoint_isBase)).mpr hI_not_max
obtain ⟨B'', hB'', hB''₁, hB''₂⟩ := (hB'.indep.diff I).exists_isBase_subset_union_isBase hB
rw [← compl_subset_compl, ← hIB.sdiff_eq_right, ← union_diff_distrib, diff_eq, compl_inter, compl_compl,
union_subset_iff, compl_subset_compl] at hB''₂
have hssu :=
(subset_inter (hB''₂.2) hIE).ssubset_of_ne
(by { rintro rfl; apply hI; convert hB''; simp [hB''.subset_ground]
})
obtain ⟨e, ⟨(heB'' : e ∉ _), heE⟩, heI⟩ := exists_of_ssubset hssu
use e
simp_rw [mem_diff, insert_subset_iff, and_iff_left heI, and_iff_right heE, and_iff_right hIE]
refine ⟨by_contra (fun heX ↦ heB'' (hB''₁ ⟨?_, heI⟩)), ⟨B'', hB'', ?_⟩⟩
· rw [hX]; exact ⟨heE, heX⟩
rw [← union_singleton, disjoint_union_left, disjoint_singleton_left, and_iff_left heB'']
exact disjoint_of_subset_left hB''₂.2 disjoint_compl_left
indep_maximal := by
rintro X - I' ⟨hI'E, B, hB, hI'B⟩ hI'X
obtain ⟨I, hI⟩ := M.exists_isBasis (M.E \ X)
obtain ⟨B', hB', hIB', hB'IB⟩ := hI.indep.exists_isBase_subset_union_isBase hB
obtain rfl : I = B' \ X :=
hI.eq_of_subset_indep (hB'.indep.diff _) (subset_diff.2 ⟨hIB', (subset_diff.1 hI.subset).2⟩)
(diff_subset_diff_left hB'.subset_ground)
simp_rw [maximal_subset_iff']
refine ⟨(X \ B') ∩ M.E, ?_, ⟨⟨inter_subset_right, ?_⟩, ?_⟩, ?_⟩
· rw [subset_inter_iff, and_iff_left hI'E, subset_diff, and_iff_right hI'X]
exact Disjoint.mono_right hB'IB <| disjoint_union_right.2 ⟨disjoint_sdiff_right.mono_left hI'X, hI'B⟩
· exact ⟨B', hB', (disjoint_sdiff_left (t := X)).mono_left inter_subset_left⟩
· exact inter_subset_left.trans diff_subset
simp only [subset_inter_iff, subset_diff, and_imp, forall_exists_index]
refine fun J hJE B'' hB'' hdj hJX hXJ ↦ ⟨⟨hJX, ?_⟩, hJE⟩
have hI' : (B'' ∩ X) ∪ (B' \ X) ⊆ B' :=
by
rw [union_subset_iff, and_iff_left diff_subset, ← union_diff_cancel hJX, inter_union_distrib_left,
hdj.symm.inter_eq, empty_union, diff_eq, ← inter_assoc, ← diff_eq, diff_subset_comm, diff_eq, inter_assoc, ←
diff_eq, inter_comm]
exact subset_trans (inter_subset_inter_right _ hB''.subset_ground) hXJ
obtain ⟨B₁, hB₁, hI'B₁, hB₁I⟩ := (hB'.indep.subset hI').exists_isBase_subset_union_isBase hB''
rw [union_comm, ← union_assoc, union_eq_self_of_subset_right inter_subset_left] at hB₁I
obtain rfl : B₁ = B' := by
refine hB₁.eq_of_subset_indep hB'.indep (fun e he ↦ ?_)
refine (hB₁I he).elim (fun heB'' ↦ ?_) (fun h ↦ h.1)
refine (em (e ∈ X)).elim (fun heX ↦ hI' (Or.inl ⟨heB'', heX⟩)) (fun heX ↦ hIB' ?_)
refine hI.mem_of_insert_indep ⟨hB₁.subset_ground he, heX⟩ ?_
exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))
by_contra hdj'
obtain ⟨e, heJ, heB'⟩ := not_disjoint_iff.mp hdj'
obtain (heB'' | ⟨-, heX⟩) := hB₁I heB'
· exact hdj.ne_of_mem heJ heB'' rfl
exact heX (hJX heJ)
subset_ground := by tauto
