internlm/Lean-Github huggingface dataset:
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A B ≥ 1
Tactic:
rcases Set.mem_insert_iff.mp hy with rfl | hy
Proof state after:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
M : RankMatroid α
y : α
B : Set α := I
hI_indep : M.Indep B
A : Set α := I \ {y}
hxy : ¬y = y
C : Set α := Set.insert y I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
hx : y ∈ M.E \ B
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A B ≥ 1

case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy✝ : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
hy : y ∈ I
⊢ M.relRank A B ≥ 1
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy✝ : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
hy : y ∈ I
⊢ M.relRank A B ≥ 1
Tactic:
have := hI_indep.indep y hy
Proof state after:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy✝ : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
hy : y ∈ I
this : M.relRank (B \ {y}) B > 0
⊢ M.relRank A B ≥ 1
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case inr
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy✝ : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
hy : y ∈ I
this : M.relRank (B \ {y}) B > 0
⊢ M.relRank A B ≥ 1
Tactic:
exact ENat.one_le_iff_pos.mpr this
Proof state after:
no goals
Theorem: RankMatroid.insert_indep_iff_relRank_insert_pos
Proof state before:
case inl
α : Type u_1
A✝ B✝ I J X : Set α
M : RankMatroid α
y : α
B : Set α := I
hI_indep : M.Indep B
A : Set α := I \ {y}
hxy : ¬y = y
C : Set α := Set.insert y I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
hx : y ∈ M.E \ B
h : M.relRank A C ≤ 1
h' : M.relRank A C = M.relRank A B + M.relRank B C
⊢ M.relRank A B ≥ 1
Tactic:
contradiction
Proof state after:
no goals
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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 ↦ ?_⟩
Proof 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}
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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)
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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'
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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))
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof state after:
no goals
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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}
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof state after:
no goals
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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]
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof state after:
no goals
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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⟩
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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, ?_⟩
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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⟩
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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}
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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}
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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⟩
Proof 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)
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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⟩
Proof 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)
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof state after:
no goals
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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]
Proof state after:
no goals
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof state after:
no goals