ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>hexI₀ : ∃ I₀ ⊆ I, I₀.Finite ∧ ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<VAR>J : Set α<VAR>hJmax : ∀ a' ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}, id J ≤ id a' → id J = id a'<VAR>hB₀J : B₀ ⊆ J<VAR>hJ : Indep J<VAR>hJss : J ⊆ E₀<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<VAR>J : Set α<VAR>hJmax : ∀ a' ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}, id J ≤ id a' → id J = id a'<VAR>hB₀J : B₀ ⊆ J<VAR>hJ : Indep J<VAR>hJss : J ⊆ E₀<VAR>heI₀ : e ∉ I₀<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<VAR>J : Set α<VAR>hJmax : ∀ a' ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}, id J ≤ id a' → id J = id a'<VAR>hB₀J : B₀ ⊆ J<VAR>hJ : Indep J<VAR>hJss : J ⊆ E₀<VAR>heI₀ : e ∉ I₀<VAR>heI₀i : Indep (insert e I₀)<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<VAR>J : Set α<VAR>hJmax : ∀ a' ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}, id J ≤ id a' → id J = id a'<VAR>hB₀J : B₀ ⊆ J<VAR>hJ : Indep J<VAR>hJss : J ⊆ E₀<VAR>heI₀ : e ∉ I₀<VAR>heI₀i : Indep (insert e I₀)<VAR>heJ : e ∉ J<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<VAR>J : Set α<VAR>hJmax : ∀ a' ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}, id J ≤ id a' → id J = id a'<VAR>hB₀J : B₀ ⊆ J<VAR>hJ : Indep J<VAR>hJss : J ⊆ E₀<VAR>heI₀ : e ∉ I₀<VAR>heI₀i : Indep (insert e I₀)<VAR>heJ : e ∉ J<VAR>hJfin : J.Finite<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<VAR>J : Set α<VAR>hJmax : ∀ a' ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}, id J ≤ id a' → id J = id a'<VAR>hB₀J : B₀ ⊆ J<VAR>hJ : Indep J<VAR>hJss : J ⊆ E₀<VAR>heI₀ : e ∉ I₀<VAR>heI₀i : Indep (insert e I₀)<VAR>heJ : e ∉ J<VAR>hJfin : J.Finite<VAR>hcard : (insert e I₀).ncard ≤ J.ncard<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<VAR>J : Set α<VAR>hJmax : ∀ a' ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}, id J ≤ id a' → id J = id a'<VAR>hB₀J : B₀ ⊆ J<VAR>hJ : Indep J<VAR>hJss : J ⊆ E₀<VAR>heI₀ : e ∉ I₀<VAR>heI₀i : Indep (insert e I₀)<VAR>heJ : e ∉ J<VAR>hJfin : J.Finite<VAR>hcard : I₀.ncard < J.ncard<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B✝ X E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>I B : Set α<VAR>hI : Indep I<VAR>hBmax : Indep B ∧ ∀ ⦃y : Set α⦄, Indep y → B ⊆ y → B = y<VAR>I' : Set α<VAR>hI' : Indep I'<VAR>hII' : I ⊆ I'<VAR>hne : ¬I = I'<VAR>e : α<VAR>heI' : e ∈ I'<VAR>heI : e ∉ I<VAR>hins : Indep (insert e I)<VAR>heB : e ∉ B<VAR>hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)<VAR>heBdep : ¬Indep (insert e B)<VAR>B₀ : Set α<VAR>hB₀B : B₀ ⊆ B<VAR>hB₀fin : B₀.Finite<VAR>hB₀e : ¬Indep (insert e B₀)<VAR>hB₀ : Indep B₀<VAR>I₀ : Set α<VAR>hI₀I : I₀ ⊆ I<VAR>hI₀fin : I₀.Finite<VAR>hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)<VAR>E₀ : Set α := insert e (I₀ ∪ B₀)<VAR>hE₀fin : E₀.Finite<VAR>J : Set α<VAR>hJmax : ∀ a' ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}, id J ≤ id a' → id J = id a'<VAR>hB₀J : B₀ ⊆ J<VAR>hJ : Indep J<VAR>hJss : J ⊆ E₀<VAR>heI₀ : e ∉ I₀<VAR>heI₀i : Indep (insert e I₀)<VAR>heJ : e ∉ J<VAR>hJfin : J.Finite<VAR>hcard : I₀.ncard < J.ncard<VAR>f : α<VAR>hfJ : f ∈ J<VAR>hfI₀ : f ∉ I₀<VAR>hfi : Indep (insert f I₀)<GOAL>False
<VAR>α : Type u_1<VAR>I✝ B X✝ E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>X I : Set α<VAR>hI : Indep I<VAR>hIX : I ⊆ X<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty
<VAR>α : Type u_1<VAR>I✝ B X✝ E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>X I : Set α<VAR>hI : Indep I<VAR>hIX : I ⊆ X<VAR>hzorn : ∃ m ∈ {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}, I ⊆ m ∧ ∀ a ∈ {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}, m ⊆ a → a = m<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}).Nonempty
<VAR>α : Type u_1<VAR>I✝ B X✝ E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>X I : Set α<VAR>hI : Indep I<VAR>hIX : I ⊆ X<GOAL>∀ c ⊆ {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}, IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}, ∀ s ∈ c, s ⊆ ub
<VAR>α : Type u_1<VAR>I✝ B X✝ E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>X I : Set α<VAR>hI : Indep I<VAR>hIX : I ⊆ X<VAR>Is : Set (Set α)<VAR>hIs : Is ⊆ {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hchain : IsChain (fun x x_1 => x ⊆ x_1) Is<VAR>x✝ : Is.Nonempty<VAR>K : Set α<VAR>hK : K ∈ Is<GOAL>Indep (⋃₀ Is)
<VAR>α : Type u_1<VAR>I✝ B X✝ E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>X I : Set α<VAR>hI : Indep I<VAR>hIX : I ⊆ X<VAR>Is : Set (Set α)<VAR>hIs : Is ⊆ {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hchain : IsChain (fun x x_1 => x ⊆ x_1) Is<VAR>x✝ : Is.Nonempty<VAR>K : Set α<VAR>hK : K ∈ Is<GOAL>I ⊆ ⋃₀ Is
<VAR>α : Type u_1<VAR>I✝ B X✝ E : Set α<VAR>Indep : Set α → Prop<VAR>indep_empty : Indep ∅<VAR>indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I<VAR>indep_aug : ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)<VAR>indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I<VAR>subset_ground : ∀ (I : Set α), Indep I → I ⊆ E<VAR>htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)<VAR>X I : Set α<VAR>hI : Indep I<VAR>hIX : I ⊆ X<VAR>Is : Set (Set α)<VAR>hIs : Is ⊆ {Y | Indep Y ∧ I ⊆ Y ∧ Y ⊆ X}<VAR>hchain : IsChain (fun x x_1 => x ⊆ x_1) Is<VAR>x✝ : Is.Nonempty<VAR>K : Set α<VAR>hK : K ∈ Is<GOAL>⋃₀ Is ⊆ X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t✝ : Set α<VAR>a b : α<VAR>s t : Set α<VAR>hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y<VAR>ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x<GOAL>sSup s = sSup t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s t✝ : Set α<VAR>a b : α<VAR>t : Set α<VAR>hs : ∀ x ∈ ∅, ∃ y ∈ t, x ≤ y<VAR>ht : ∀ y ∈ t, ∃ x ∈ ∅, y ≤ x<GOAL>sSup ∅ = sSup t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t✝ : Set α<VAR>a b : α<VAR>s t : Set α<VAR>hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y<VAR>ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x<VAR>s_ne : s.Nonempty<GOAL>sSup s = sSup t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>s_ne : s.Nonempty<VAR>hs : ∀ x ∈ s, ∃ y ∈ ∅, x ≤ y<VAR>ht : ∀ y ∈ ∅, ∃ x ∈ s, y ≤ x<GOAL>sSup s = sSup ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t✝ : Set α<VAR>a b : α<VAR>s t : Set α<VAR>hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y<VAR>ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x<VAR>s_ne : s.Nonempty<VAR>t_ne : t.Nonempty<GOAL>sSup s = sSup t
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Prime p<VAR>hs : p ∉ s<VAR>hn : n ∈ factoredNumbers s<GOAL>p.Coprime n
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Prime p<VAR>hs : p ∉ s<VAR>hn : n ∈ factoredNumbers s<GOAL>p ∉ n.primeFactorsList
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>n : ℕ<VAR>inst✝ : Nontrivial R<VAR>b : Basis (Fin n) R M<VAR>k : Fin (n + 1)<VAR>l : Fin n<GOAL>b.flag k ≤ LinearMap.ker (b.coord l) ↔ k ≤ l.castSucc
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>a : CliffordAlgebra Q<VAR>r : R<GOAL>(contractLeft d) (a * (algebraMap R (CliffordAlgebra Q)) r) = (contractLeft d) a * (algebraMap R (CliffordAlgebra Q)) r