Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
have htofin : ∀ I e, Indep I → ¬ Indep (insert e I) →
        ∃ I₀, I₀ ⊆ I ∧ I₀.Finite ∧ ¬ Indep (insert e I₀) := by
        by_contra! ⟨I, e, -, hIe, h⟩
        refine hIe <| indep_compact _ fun J hJss hJfin ↦ ?_
        exact indep_subset (h (J \ {e}) (by rwa [sdiff_subset_iff]) hJfin.sdiff) (by simp)
      intro I B hI hImax hBmax
      obtain ⟨e, heI, hins⟩ := exists_insert_of_not_maximal indep_subset hI hImax
      by_cases heB : e ∈ B
      · exact ⟨e, ⟨heB, heI⟩, hins⟩
      by_contra! hcon
      have heBdep := hBmax.not_prop_of_ssuperset (ssubset_insert heB)
      -- There is a finite subset `B₀` of `B` so that `B₀ + e` is dependent
      obtain ⟨B₀, hB₀B, hB₀fin, hB₀e⟩ := htofin B e hBmax.1 heBdep
      have hB₀ := indep_subset hBmax.1 hB₀B
      -- `I` has a finite subset `I₀` that doesn't extend into `B₀`
      have hexI₀ : ∃ I₀, I₀ ⊆ I ∧ I₀.Finite ∧ ∀ x, x ∈ B₀ \ I₀ → ¬Indep (insert x I₀) := by
        have hch : ∀ (b : ↑(B₀ \ I)), ∃ Ib, Ib ⊆ I ∧ Ib.Finite ∧ ¬Indep (insert (b : α) Ib) := by
          rintro ⟨b, hb⟩; exact htofin I b hI (hcon b ⟨hB₀B hb.1, hb.2⟩)
        choose! f hf using hch
        have : Finite ↑(B₀ \ I) := hB₀fin.sdiff.to_subtype
        refine ⟨iUnion f ∪ (B₀ ∩ I),
          union_subset (iUnion_subset (fun i ↦ (hf i).1)) inter_subset_right,
          (finite_iUnion fun i ↦ (hf i).2.1).union (hB₀fin.subset inter_subset_left),
          fun x ⟨hxB₀, hxn⟩ hi ↦ ?_⟩
        have hxI : x ∉ I := fun hxI ↦ hxn <| Or.inr ⟨hxB₀, hxI⟩
        refine (hf ⟨x, ⟨hxB₀, hxI⟩⟩).2.2 (indep_subset hi <| insert_subset_insert ?_)
        apply subset_union_of_subset_left
        apply subset_iUnion
      obtain ⟨I₀, hI₀I, hI₀fin, hI₀⟩ := hexI₀
      set E₀ := insert e (I₀ ∪ B₀)
      have hE₀fin : E₀.Finite := (hI₀fin.union hB₀fin).insert e
      -- Extend `B₀` to a maximal independent subset of `I₀ ∪ B₀ + e`
      obtain ⟨J, ⟨hB₀J, hJ, hJss⟩, hJmax⟩ := Finite.exists_maximalFor (f := id)
        (s := {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀})
        (hE₀fin.finite_subsets.subset (by simp))
        ⟨B₀, Subset.rfl, hB₀, subset_union_right.trans (subset_insert _ _)⟩
      have heI₀ : e ∉ I₀ := notMem_subset hI₀I heI
      have heI₀i : Indep (insert e I₀) := indep_subset hins (insert_subset_insert hI₀I)
      have heJ : e ∉ J := fun heJ ↦ hB₀e (indep_subset hJ <| insert_subset heJ hB₀J)
      have hJfin := hE₀fin.subset hJss
      -- We have `|I₀ + e| ≤ |J|`, since otherwise we could extend the maximal set `J`
      have hcard : (insert e I₀).ncard ≤ J.ncard := by
        refine not_lt.1 fun hlt ↦ ?_
        obtain ⟨f, hfI, hfJ, hfi⟩ := indep_aug hJ hJfin heI₀i (hI₀fin.insert e) hlt
        have hfE₀ : f ∈ E₀ := mem_of_mem_of_subset hfI (insert_subset_insert subset_union_left)
        exact hfJ <| insert_eq_self.1 <| le_imp_eq_iff_le_imp_ge'.2 (hJmax
          ⟨hB₀J.trans <| subset_insert _ _, hfi, insert_subset hfE₀ hJss⟩) (subset_insert _ _)
      -- But this means `|I₀| < |J|`, and extending `I₀` into `J` gives a contradiction
      rw [ncard_insert_of_notMem heI₀ hI₀fin, ← Nat.lt_iff_add_one_le] at hcard
      obtain ⟨f, hfJ, hfI₀, hfi⟩ := indep_aug (indep_subset hI hI₀I) hI₀fin hJ hJfin hcard
      exact hI₀ f ⟨Or.elim (hJss hfJ) (fun hfe ↦ (heJ <| hfe ▸ hfJ).elim) (by aesop), hfI₀⟩ hfi

Goal state after: