Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero (Matroid/Constructions/RankAxioms.lean)

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X} ↔ M.relRank I X = 0
Tactic:
refine ⟨fun hI_max ↦ ?_, fun hr ↦ ?_⟩
State after:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
⊢ M.relRank I X = 0

case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.relRank I X = 0
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}

State before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.relRank I X = 0
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
Tactic:
contrapose! hr
State after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
⊢ M.relRank I X ≠ 0

State before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
⊢ M.relRank I X ≠ 0
Tactic:
unfold maximals at hr
State after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr :
  I ∉
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ X} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ M.relRank I X ≠ 0

State before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr :
  I ∉
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ X} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ M.relRank I X ≠ 0
Tactic:
simp only [Set.mem_setOf_eq, and_imp, not_and, not_forall, Classical.not_imp, exists_prop, exists_and_left] at hr
State after:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
⊢ M.relRank I X ≠ 0

State before:
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
⊢ M.relRank I X ≠ 0
Tactic:
obtain ⟨I', hI'_indep, hI', hI'_ssubset⟩ := hr hI_indep hI
State after:
case refine_2.intro.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊆ I' ∧ ¬I' ⊆ I
⊢ M.relRank I X ≠ 0

State before:
case refine_2.intro.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊆ I' ∧ ¬I' ⊆ I
⊢ M.relRank I X ≠ 0
Tactic:
rw [<-Set.ssubset_def] at hI'_ssubset
State after:
case refine_2.intro.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
⊢ M.relRank I X ≠ 0

State before:
case refine_2.intro.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
⊢ M.relRank I X ≠ 0
Tactic:
obtain ⟨x, hxI', hxI⟩ := Set.exists_of_ssubset hI'_ssubset
State after:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
⊢ M.relRank I X ≠ 0

State before:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
⊢ M.relRank I X ≠ 0
Tactic:
have : M.Indep (Set.insert x I) := by
  exact indep_subset hI'_indep (Set.insert_subset hxI' hI'_ssubset.subset)
State after:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.Indep (Set.insert x I)
⊢ M.relRank I X ≠ 0

State before:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.Indep (Set.insert x I)
⊢ M.relRank I X ≠ 0
Tactic:
have hx : x ∈ M.E := hI'_indep.subset_ground hxI'
State after:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.Indep (Set.insert x I)
hx : x ∈ M.E
⊢ M.relRank I X ≠ 0

State before:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.Indep (Set.insert x I)
hx : x ∈ M.E
⊢ M.relRank I X ≠ 0
Tactic:
rw [insert_indep_iff_relRank_insert_pos hI_indep ((Set.mem_diff x).mpr ⟨hx, hxI⟩)] at this
State after:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
⊢ M.relRank I X ≠ 0

State before:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
⊢ M.relRank I X ≠ 0
Tactic:
have : M.relRank I X > 0 := by
  rw [M.relRank_add_cancel (Set.subset_insert x I) (Set.insert_subset (hI' hxI') hI)]
  exact Left.add_pos_of_pos_of_nonneg this (zero_le (M.relRank (Set.insert x I) X))
State after:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this✝ : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
this : M.relRank I X > 0
⊢ M.relRank I X ≠ 0

State before:
case refine_2.intro.intro.intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this✝ : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
this : M.relRank I X > 0
⊢ M.relRank I X ≠ 0
Tactic:
exact pos_iff_ne_zero.mp this
State after:
no goals

State before:
case refine_1
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
⊢ M.relRank I X = 0
Tactic:
by_cases hXI : X = I
State after:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : X = I
⊢ M.relRank I X = 0

case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
⊢ M.relRank I X = 0

State before:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
⊢ M.relRank I X = 0
Tactic:
set S := {(insert x I) | x ∈ X \ I}
State after:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
⊢ M.relRank I X = 0

State before:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
⊢ M.relRank I X = 0
Tactic:
have := M.relRank_sUnion_eq_zero h
State after:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
⊢ M.relRank I X = 0

State before:
case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
hXU : X = ⋃₀ S
⊢ M.relRank I X = 0
Tactic:
rwa [<-hXU] at this
State after:
no goals

State before:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : X = I
⊢ M.relRank I X = 0
Tactic:
rw [hXI]
State after:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : X = I
⊢ M.relRank I I = 0

State before:
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : X = I
⊢ M.relRank I I = 0
Tactic:
exact relRank_self_eq_zero
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
⊢ ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
Tactic:
rintro A ⟨x, hx_mem, rfl⟩
State after:
case intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
⊢ I ⊆ insert x I ∧ M.relRank I (insert x I) = 0

State before:
case intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
⊢ I ⊆ insert x I ∧ M.relRank I (insert x I) = 0
Tactic:
refine ⟨Set.subset_insert x I, ?_⟩
State after:
case intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
⊢ M.relRank I (insert x I) = 0

State before:
case intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
⊢ M.relRank I (insert x I) = 0
Tactic:
rcases (Set.mem_diff x).mpr hx_mem with ⟨hxX, hxI⟩
State after:
case intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
⊢ M.relRank I (insert x I) = 0

State before:
case intro.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
⊢ M.relRank I (insert x I) = 0
Tactic:
by_cases hx : x ∉ M.E
State after:
case pos
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∉ M.E
⊢ M.relRank I (insert x I) = 0

case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : ¬x ∉ M.E
⊢ M.relRank I (insert x I) = 0

State before:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : ¬x ∉ M.E
⊢ M.relRank I (insert x I) = 0
Tactic:
simp only [not_not] at hx
State after:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
⊢ M.relRank I (insert x I) = 0

State before:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
⊢ M.relRank I (insert x I) = 0
Tactic:
contrapose! hI_max
State after:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max : M.relRank I (insert x I) ≠ 0
⊢ I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}

State before:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max : M.relRank I (insert x I) ≠ 0
⊢ I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
Tactic:
have hI_max : M.relRank I (insert x I) > 0 := by exact pos_iff_ne_zero.mpr hI_max
State after:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
⊢ I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}

State before:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
⊢ I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
Tactic:
suffices h : M.Indep (insert x I) by
  have : (insert x I) ∈ {S | M.Indep S ∧ S ⊆ X} := ⟨h, Set.insert_subset hxX hI⟩
  apply mem_maximals_iff.not.mpr
  push_neg; intro; use (insert x I)
  exact ⟨this, Set.subset_insert x I, by exact Set.ne_insert_of_not_mem I hxI⟩
State after:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
⊢ M.Indep (insert x I)

State before:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
⊢ M.Indep (insert x I)
Tactic:
have hxEI : x ∈ M.E \ I := by exact (Set.mem_diff x).mpr ⟨hx, hxI⟩
State after:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
hxEI : x ∈ M.E \ I
⊢ M.Indep (insert x I)

State before:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
hxEI : x ∈ M.E \ I
⊢ M.Indep (insert x I)
Tactic:
exact (insert_indep_iff_relRank_insert_pos hI_indep hxEI).mpr hI_max
State after:
no goals

State before:
case pos
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∉ M.E
⊢ M.relRank I (insert x I) = 0
Tactic:
rw [<-M.relRank_inter_ground, Set.insert_inter_of_not_mem hx, M.relRank_self_eq_zero]
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max : M.relRank I (insert x I) ≠ 0
⊢ M.relRank I (insert x I) > 0
Tactic:
exact pos_iff_ne_zero.mpr hI_max
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
⊢ I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
Tactic:
have : (insert x I) ∈ {S | M.Indep S ∧ S ⊆ X} := ⟨h, Set.insert_subset hxX hI⟩
State after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
Tactic:
apply mem_maximals_iff.not.mpr
State after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ ¬(I ∈ {S | M.Indep S ∧ S ⊆ X} ∧ ∀ ⦃y : Set α⦄, y ∈ {S | M.Indep S ∧ S ⊆ X} → I ⊆ y → I = y)

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ ¬(I ∈ {S | M.Indep S ∧ S ⊆ X} ∧ ∀ ⦃y : Set α⦄, y ∈ {S | M.Indep S ∧ S ⊆ X} → I ⊆ y → I = y)
Tactic:
push_neg
State after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ I ∈ {S | M.Indep S ∧ S ⊆ X} → ∃ y ∈ {S | M.Indep S ∧ S ⊆ X}, I ⊆ y ∧ I ≠ y

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ I ∈ {S | M.Indep S ∧ S ⊆ X} → ∃ y ∈ {S | M.Indep S ∧ S ⊆ X}, I ⊆ y ∧ I ≠ y
Tactic:
intro
State after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
_✝ : I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ ∃ y ∈ {S | M.Indep S ∧ S ⊆ X}, I ⊆ y ∧ I ≠ y

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
_✝ : I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ ∃ y ∈ {S | M.Indep S ∧ S ⊆ X}, I ⊆ y ∧ I ≠ y
Tactic:
use (insert x I)
State after:
case h
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
_✝ : I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ insert x I ∈ {S | M.Indep S ∧ S ⊆ X} ∧ I ⊆ insert x I ∧ I ≠ insert x I

State before:
case h
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
_✝ : I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ insert x I ∈ {S | M.Indep S ∧ S ⊆ X} ∧ I ⊆ insert x I ∧ I ≠ insert x I
Tactic:
exact ⟨this, Set.subset_insert x I, by exact Set.ne_insert_of_not_mem I hxI⟩
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
h : M.Indep (insert x I)
this : insert x I ∈ {S | M.Indep S ∧ S ⊆ X}
_✝ : I ∈ {S | M.Indep S ∧ S ⊆ X}
⊢ I ≠ insert x I
Tactic:
exact Set.ne_insert_of_not_mem I hxI
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
⊢ x ∈ M.E \ I
Tactic:
exact (Set.mem_diff x).mpr ⟨hx, hxI⟩
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
⊢ X = ⋃₀ S
Tactic:
apply Set.eq_of_subset_of_subset
State after:
case a
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
⊢ X ⊆ ⋃₀ S

case a
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
⊢ ⋃₀ S ⊆ X

State before:
case a
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
⊢ ⋃₀ S ⊆ X
Tactic:
apply Set.sUnion_subset_iff.mpr
State after:
case a
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
⊢ ∀ t' ∈ S, t' ⊆ X

State before:
case a
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
⊢ ∀ t' ∈ S, t' ⊆ X
Tactic:
rintro Ax ⟨x, hx_mem, rfl⟩
State after:
case a.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx_mem : x ∈ X \ I
⊢ insert x I ⊆ X

State before:
case a.intro.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx_mem : x ∈ X \ I
⊢ insert x I ⊆ X
Tactic:
exact Set.insert_subset ((Set.mem_diff x).mpr hx_mem).left hI
State after:
no goals

State before:
case a
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
⊢ X ⊆ ⋃₀ S
Tactic:
intro x hx
State after:
case a
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
⊢ x ∈ ⋃₀ S

State before:
case a
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
⊢ x ∈ ⋃₀ S
Tactic:
simp only [Set.mem_sUnion]
State after:
case a
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
⊢ ∃ t ∈ S, x ∈ t

State before:
case a
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
⊢ ∃ t ∈ S, x ∈ t
Tactic:
by_cases h : x ∈ I
State after:
case pos
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
⊢ ∃ t ∈ S, x ∈ t

case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∉ I
⊢ ∃ t ∈ S, x ∈ t

State before:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∉ I
⊢ ∃ t ∈ S, x ∈ t
Tactic:
have hx := (Set.mem_diff x).mpr ⟨hx, h⟩
State after:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ ∃ t ∈ S, x ∈ t

State before:
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ ∃ t ∈ S, x ∈ t
Tactic:
use insert x I
State after:
case h
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ insert x I ∈ S ∧ x ∈ insert x I

State before:
case h
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ insert x I ∈ S ∧ x ∈ insert x I
Tactic:
constructor
State after:
case h.left
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ insert x I ∈ S

case h.right
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ x ∈ insert x I

State before:
case h.right
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ x ∈ insert x I
Tactic:
exact Set.mem_insert x I
State after:
no goals

State before:
case pos
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
⊢ ∃ t ∈ S, x ∈ t
Tactic:
have hXU_ssubset := Set.ssubset_iff_subset_ne.mpr ⟨hI, Ne.symm hXI⟩
State after:
case pos
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
⊢ ∃ t ∈ S, x ∈ t

State before:
case pos
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
⊢ ∃ t ∈ S, x ∈ t
Tactic:
rcases Set.exists_of_ssubset hXU_ssubset with ⟨y, hy⟩
State after:
case pos.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy : y ∈ X ∧ y ∉ I
⊢ ∃ t ∈ S, x ∈ t

State before:
case pos.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy : y ∈ X ∧ y ∉ I
⊢ ∃ t ∈ S, x ∈ t
Tactic:
have hy := (Set.mem_diff y).mpr hy
State after:
case pos.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
⊢ ∃ t ∈ S, x ∈ t

State before:
case pos.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
⊢ ∃ t ∈ S, x ∈ t
Tactic:
set Ay := insert y I
State after:
case pos.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
Ay : Set α := insert y I
⊢ ∃ t ∈ S, x ∈ t

State before:
case pos.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
Ay : Set α := insert y I
⊢ ∃ t ∈ S, x ∈ t
Tactic:
have : Ay ∈ S := by use y
State after:
case pos.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this✝ : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
Ay : Set α := insert y I
this : Ay ∈ S
⊢ ∃ t ∈ S, x ∈ t

State before:
case pos.intro
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this✝ : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
Ay : Set α := insert y I
this : Ay ∈ S
⊢ ∃ t ∈ S, x ∈ t
Tactic:
use Ay
State after:
case h
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this✝ : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
Ay : Set α := insert y I
this : Ay ∈ S
⊢ Ay ∈ S ∧ x ∈ Ay

State before:
case h
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this✝ : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
Ay : Set α := insert y I
this : Ay ∈ S
⊢ Ay ∈ S ∧ x ∈ Ay
Tactic:
exact ⟨this, (Set.subset_insert y I) h⟩
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx : x ∈ X
h : x ∈ I
hXU_ssubset : I ⊂ X
y : α
hy✝ : y ∈ X ∧ y ∉ I
hy : y ∈ X \ I
Ay : Set α := insert y I
⊢ Ay ∈ S
Tactic:
use y
State after:
no goals

State before:
case h.left
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
h✝ : ∀ A ∈ S, I ⊆ A ∧ M.relRank I A = 0
this : M.relRank I (⋃₀ S) = 0
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ insert x I ∈ S
Tactic:
use x
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
⊢ M.Indep (Set.insert x I)
Tactic:
exact indep_subset hI'_indep (Set.insert_subset hxI' hI'_ssubset.subset)
State after:
no goals

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
⊢ M.relRank I X > 0
Tactic:
rw [M.relRank_add_cancel (Set.subset_insert x I) (Set.insert_subset (hI' hxI') hI)]
State after:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
⊢ M.relRank I (insert x I) + M.relRank (insert x I) X > 0

State before:
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
I' : Set α
hI'_indep : M.Indep I'
hI' : I' ⊆ X
hI'_ssubset : I ⊂ I'
x : α
hxI' : x ∈ I'
hxI : x ∉ I
this : M.relRank I (Set.insert x I) > 0
hx : x ∈ M.E
⊢ M.relRank I (insert x I) + M.relRank (insert x I) X > 0
Tactic:
exact Left.add_pos_of_pos_of_nonneg this (zero_le (M.relRank (Set.insert x I) X))
State after:
no goals