internlm/Lean-Github huggingface dataset:
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
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⟩
Proof 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}
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
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
Proof 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)
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
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
Proof 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
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
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
Proof 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
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
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)
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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⟩
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
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
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
hI_max : M.relRank I (insert x I) > 0
⊢ x ∈ M.E \ I
Tactic:
exact (Set.mem_diff x).mpr ⟨hx, hxI⟩
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}
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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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⟩
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof state after:
no goals
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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]
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
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}
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
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
x : α
hx : x ∈ X
h : x ∉ I
⊢ ∃ t ∈ S, x ∈ t
Tactic:
have hx := (Set.mem_diff x).mpr ⟨hx, 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
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ ∃ t ∈ S, x ∈ t
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
x : α
hx✝ : x ∈ X
h : x ∉ I
hx : x ∈ X \ I
⊢ ∃ t ∈ S, x ∈ t
Tactic:
use insert x I
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
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}
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⟩
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}
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
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}
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⟩
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
Proof 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
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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⟩
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}
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
Proof state after:
no goals
Theorem: RankMatroid.indep_subset_maximal_iff_relRank_zero
Proof 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
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
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)
Proof state after:
no goals