my naive matroid lib

Stream: Is there code for X?

[Asei Inoue]

I am working on formalizing matroid theory. (I know that mathlib has code for this, I want to do this by myself)

But stacked to show there exists base X ⊆ B for all independent set X. (see Matroid.base_of_ind) how to show this?

Better formalization needed?

import Mathlib.Tactic
import Mathlib.Data.Set.Card

set_option autoImplicit false
set_option relaxedAutoImplicit false

class Matroid {α : Type} (E : Finset α) (I : Set (Set E)) where
  empty : ∅ ∈ I

  sub_closed {X Y : Set E} : X ∈ I → Y ⊆ X → Y ∈ I

  augment {X Y : Set E} (hx : X ∈ I) (hy : Y ∈ I) :
    X.ncard > Y.ncard → ∃ e ∈ X \ Y, ({e} ∪ Y) ∈ I

variable {α : Type} {E : Finset α} (I : Set (Set E))

def Matroid.Base (I : Set (Set E)) [Matroid E I] (B : Set E) : Prop :=
  B ∈ I ∧ ∀ e ∈ Bᶜ, ({e} ∪ B) ∉ I

theorem Matroid.base_up_closed (I : Set (Set E)) [Matroid E I] {B : Set E} (hB : Matroid.Base I B) {X : Set E} :
    X ⊆ B → X ∈ I := by
  have : B ∈ I := by exact hB.left
  exact Matroid.sub_closed this

theorem Matroid.base_equicardinality (I : Set (Set E)) [Matroid E I] {B B' : Set E}
    (hB : Matroid.Base I B) (hB' : Matroid.Base I B') : B.ncard = B'.ncard := by

  by_contra! hne

  wlog hlt : B.ncard < B'.ncard with H

  case inr =>
    replace hlt : B.ncard > B'.ncard := by omega
    apply @H α E I _ B' B <;> try assumption
    omega

  guard_hyp hlt : B.ncard < B'.ncard
  clear hne

  have indb : B ∈ I := by exact hB.left
  replace hB' : B' ∈ I := by exact hB'.left

  replace hB' : ∃ e ∈ B' \ B, ({e} ∪ B) ∈ I := by
    apply Matroid.augment hB' indb
    omega

  have := hB.right
  aesop

theorem Matroid.base_of_ind (I : Set (Set E)) [Matroid E I] {X : Set E} (hX : X ∈ I) :
    ∃ B, Matroid.Base I B ∧ X ⊆ B := by
  induction' h : (Xᶜ : Set E).ncard

  case zero =>
    replace h : X = Set.univ ∨ Xᶜ.Infinite := by
      simp_all [Set.ncard]

    replace h : Xᶜ = ∅ := by
      rcases h with h | h
      · simp_all
      · exfalso
        simp_all [Set.toFinite Xᶜ]

    replace h : X = Set.univ := by
      simp_all

    use X

    refine ⟨?_, by simp⟩

    dsimp [Base]
    refine ⟨by assumption, ?_⟩
    intro e he
    exfalso
    simp [h] at he

  case succ n ih =>
    sorry

[Asei Inoue]

is it impossible to show Matroid.base_of_ind?

[Asei Inoue]

I think I need to know the right way to handle finiteness...

[Jihoon Hyun]

  induction' h : (Xᶜ : Set E).ncard generalizing X

Maybe you can continue now.