ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : ι → Set E<VAR>s : Finset ι<VAR>h_card : finrank 𝕜 E + 1 ≤ s.card<VAR>h_convex : ∀ i ∈ s, Convex 𝕜 (F i)<VAR>h_inter : ∀ I ⊆ s, I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<VAR>I : Finset ι<VAR>hI_ss : I ⊆ s<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Finset ι<VAR>hI_ss_J : I ⊆ J<VAR>hJ_ss : J ⊆ s<VAR>hJ_card : J.card = finrank 𝕜 E + 1<GOAL>(⋂ i ∈ I, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : ι → Set E<VAR>s : Finset ι<VAR>h_card : finrank 𝕜 E + 1 ≤ s.card<VAR>h_convex : ∀ i ∈ s, Convex 𝕜 (F i)<VAR>h_inter : ∀ I ⊆ s, I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<VAR>I : Finset ι<VAR>hI_ss : I ⊆ s<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Finset ι<VAR>hI_ss_J : I ⊆ J<VAR>hJ_ss : J ⊆ s<VAR>hJ_card : J.card = finrank 𝕜 E + 1<GOAL>(⋂ x ∈ fun a => a ∈ J.val, F x).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>x✝ : Set α<GOAL>x✝ ∈ l ↔ ∃ i, (∃ i_1, p i_1 ∧ s i_1 = i) ∧ id i ⊆ x✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f✝ g✝ : ι → M<VAR>s t : Finset ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁸ : Category.{u_5, u_1} C₁<VAR>inst✝⁷ : Category.{u_6, u_2} C₂<VAR>inst✝⁶ : Category.{u_4, u_3} D<VAR>inst✝⁵ : Preadditive C₁<VAR>inst✝⁴ : Preadditive C₂<VAR>inst✝³ : Preadditive D<VAR>K₁ : CochainComplex C₁ ℤ<VAR>K₂ : CochainComplex C₂ ℤ<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝² : F.Additive<VAR>inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>x y : ℤ<VAR>inst✝ : K₁.HasMapBifunctor K₂ F<GOAL>(HomologicalComplex₂.total.map (K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x).hom (ComplexShape.up ℤ) ≫ ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂)).totalShift₁Iso x).hom) ≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).map (HomologicalComplex₂.total.map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom (ComplexShape.up ℤ) ≫ ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).totalShift₂Iso y).hom) = (x * y).negOnePow • (HomologicalComplex₂.total.map (((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom (ComplexShape.up ℤ) ≫ ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁)).obj K₂).totalShift₂Iso y).hom) ≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map (HomologicalComplex₂.total.map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom (ComplexShape.up ℤ) ≫ ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).totalShift₁Iso x).hom) ≫ (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app (K₁.mapBifunctor K₂ F)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁸ : Category.{u_5, u_1} C₁<VAR>inst✝⁷ : Category.{u_6, u_2} C₂<VAR>inst✝⁶ : Category.{u_4, u_3} D<VAR>inst✝⁵ : Preadditive C₁<VAR>inst✝⁴ : Preadditive C₂<VAR>inst✝³ : Preadditive D<VAR>K₁ : CochainComplex C₁ ℤ<VAR>K₂ : CochainComplex C₂ ℤ<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝² : F.Additive<VAR>inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>x y : ℤ<VAR>inst✝ : K₁.HasMapBifunctor K₂ F<GOAL>HomologicalComplex₂.total.map (((K₁.mapBifunctorHomologicalComplexShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x).hom ≫ (HomologicalComplex₂.shiftFunctor₁ D x).map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom) ≫ (HomologicalComplex₂.shiftFunctor₁₂CommIso D x y).hom.app (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)) (ComplexShape.up ℤ) ≫ (((HomologicalComplex₂.shiftFunctor₁ D x).obj (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).totalShift₂Iso y).hom ≫ (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) y).map ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).totalShift₁Iso x).hom ≫ (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).total (ComplexShape.up ℤ)) = HomologicalComplex₂.total.map ((((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom ≫ (HomologicalComplex₂.shiftFunctor₂ D y).map (K₁.mapBifunctorHomologicalComplexShift₁Iso K₂ F x).hom) (ComplexShape.up ℤ) ≫ (((HomologicalComplex₂.shiftFunctor₁ D x).obj (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).totalShift₂Iso y).hom ≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).totalShift₁Iso x).hom ≫ (shiftFunctorComm (CochainComplex D ℤ) x y).hom.app (K₁.mapBifunctor K₂ F)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁸ : Category.{u_5, u_1} C₁<VAR>inst✝⁷ : Category.{u_6, u_2} C₂<VAR>inst✝⁶ : Category.{u_4, u_3} D<VAR>inst✝⁵ : Preadditive C₁<VAR>inst✝⁴ : Preadditive C₂<VAR>inst✝³ : Preadditive D<VAR>K₁ : CochainComplex C₁ ℤ<VAR>K₂ : CochainComplex C₂ ℤ<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>inst✝² : F.Additive<VAR>inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>x y : ℤ<VAR>inst✝ : K₁.HasMapBifunctor K₂ F<VAR>a b : ℤ<GOAL>(𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))) ≫ 𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y)))) ≫ 𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))) = 𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y))) ≫ 𝟙 ((F.obj (K₁.X (a + x))).obj (K₂.X (b + y)))
<VAR>I : Type u<VAR>inst✝⁵ : DecidableEq I<VAR>i✝ : I<VAR>R : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>A : I → Type w<VAR>inst✝³ : (i : I) → Semiring (A i)<VAR>inst✝² : (i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>i : I<GOAL>(RingQuot.mkAlgHom R (rel R A)) ((ι R) ((DirectSum.lof R I A i) 1)) = 1
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Iio l) = ⨅ a, ⨅ (_ : a ≠ ⊥), 𝓟 (Iio a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<GOAL>(a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace α'<VAR>inst✝³ : One β<VAR>inst✝² : One γ<VAR>inst✝¹ : One δ<VAR>g : β → γ<VAR>f : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝ : R1Space α<GOAL>(∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ : C<VAR>f g h : j₁ ⟶ j₂<GOAL>g ≫ coeqHom f g ≫ leftToMax (coeq f g) (coeq g h) ≫ coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) = h ≫ coeqHom f g ≫ leftToMax (coeq f g) (coeq g h) ≫ coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ : C<VAR>f g h : j₁ ⟶ j₂<GOAL>g ≫ (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫ coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) = h ≫ coeqHom f g ≫ leftToMax (coeq f g) (coeq g h) ≫ coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ : C<VAR>f g h : j₁ ⟶ j₂<GOAL>g ≫ (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫ coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) = h ≫ (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫ coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ : C<VAR>f g h : j₁ ⟶ j₂<GOAL>((h ≫ coeqHom g h) ≫ rightToMax (coeq f g) (coeq g h)) ≫ coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) = h ≫ (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫ coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
<VAR>x y : ℝ<VAR>h : 0 < x<GOAL>log x < 0 ↔ x < 1
<VAR>x y : ℝ<VAR>h : 0 < x<GOAL>log x < log 1 ↔ x < 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hαβ : s.IsPWO<VAR>a : α<VAR>f : Lex (α × β) → β := fun x => (ofLex x).2<VAR>h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})<GOAL>(f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})).IsPWO
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hαβ : s.IsPWO<VAR>a : α<VAR>f : Lex (α × β) → β := fun x => (ofLex x).2<VAR>h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})<GOAL>MonotoneOn f (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hαβ : s.IsPWO<VAR>a : α<VAR>f : Lex (α × β) → β := fun x => (ofLex x).2<VAR>h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})<VAR>b : Lex (α × β)<VAR>hb : b ∈ (fun x => (ofLex x).1) ⁻¹' {a}<VAR>c : Lex (α × β)<VAR>hc : c ∈ (fun x => (ofLex x).1) ⁻¹' {a}<VAR>hbc : b ≤ c<GOAL>f b ≤ f c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hαβ : s.IsPWO<VAR>a : α<VAR>f : Lex (α × β) → β := fun x => (ofLex x).2<VAR>h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})<VAR>b c : Lex (α × β)<VAR>hbc : b ≤ c<VAR>hb : (ofLex b).1 = a<VAR>hc : (ofLex c).1 = a<GOAL>f b ≤ f c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>s : Set (Lex (α × β))<VAR>hαβ : s.IsPWO<VAR>a : α<VAR>f : Lex (α × β) → β := fun x => (ofLex x).2<VAR>h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x => (ofLex x).1) ⁻¹' {a})<VAR>b c : Lex (α × β)<VAR>hbc : b ≤ c<VAR>hb : (ofLex b).1 = a<VAR>hc : (ofLex c).1 = a<VAR>this : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c<GOAL>f b ≤ f c
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X : Set α<VAR>M : Matroid α<VAR>I J : Set α<VAR>hJE : J ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hJB : Disjoint J B<VAR>hIJ : I ⊆ J<GOAL>I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>hB' : M.Base (M.E \ X)<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hB''₁ : B' \ I ⊆ B''<VAR>hB''₂ : B'' ⊆ B' \ I ∪ B<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hB''₁ : B' \ I ⊆ B''<VAR>hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hB''₁ : B' \ I ⊆ B''<VAR>hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ<VAR>hssu : I ⊂ B''ᶜ ∩ M.E<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hB''₁ : B' \ I ⊆ B''<VAR>hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ<VAR>hssu : I ⊂ B''ᶜ ∩ M.E<VAR>e : α<VAR>heI : e ∉ I<VAR>heB'' : e ∉ B''<VAR>heE : e ∈ M.E<GOAL>∃ x ∈ X \ I, (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert x I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hB''₁ : B' \ I ⊆ B''<VAR>hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ<VAR>hssu : I ⊂ B''ᶜ ∩ M.E<VAR>e : α<VAR>heI : e ∉ I<VAR>heB'' : e ∉ B''<VAR>heE : e ∈ M.E<GOAL>e ∈ X \ I ∧ (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (insert e I)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hB''₁ : B' \ I ⊆ B''<VAR>hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ<VAR>hssu : I ⊂ B''ᶜ ∩ M.E<VAR>e : α<VAR>heI : e ∉ I<VAR>heB'' : e ∉ B''<VAR>heE : e ∈ M.E<GOAL>e ∈ X ∧ ∃ B, M.Base B ∧ Disjoint (insert e I) B
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hB''₁ : B' \ I ⊆ B''<VAR>hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ<VAR>hssu : I ⊂ B''ᶜ ∩ M.E<VAR>e : α<VAR>heI : e ∉ I<VAR>heB'' : e ∉ B''<VAR>heE : e ∈ M.E<GOAL>Disjoint (insert e I) B''
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIE : I ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : Disjoint I B<VAR>hI_not_max : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hX_max : X ∈ maximals (fun x x_1 => x ⊆ x_1) {I | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) I}<VAR>hXE : X ⊆ M.E<VAR>B' : Set α := M.E \ X<VAR>hB' : M.Base B'<VAR>hX : B' = M.E \ X<VAR>hI : ¬M.Base (M.E \ I)<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hB''₁ : B' \ I ⊆ B''<VAR>hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ<VAR>hssu : I ⊂ B''ᶜ ∩ M.E<VAR>e : α<VAR>heI : e ∉ I<VAR>heB'' : e ∉ B''<VAR>heE : e ∈ M.E<GOAL>Disjoint I B''
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) Y ∧ I' ⊆ Y ∧ Y ⊆ X}).Nonempty
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) Y ∧ I' ⊆ Y ∧ Y ⊆ X}).Nonempty
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<GOAL>(maximals (fun x x_1 => x ⊆ x_1) {Y | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) Y ∧ I' ⊆ Y ∧ Y ⊆ X}).Nonempty
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<GOAL>(fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) (X \ B' ∩ M.E)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<GOAL>I' ⊆ X ∧ Disjoint I' B'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<GOAL>∀ ⦃b : Set α⦄, b ∈ {Y | (fun I => I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B) Y ∧ I' ⊆ Y ∧ Y ⊆ X} → (fun x x_1 => x ⊆ x_1) (X \ B' ∩ M.E) b → (fun x x_1 => x ⊆ x_1) b (X \ B' ∩ M.E)
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<GOAL>∀ ⦃b : Set α⦄, b ⊆ M.E → ∀ (x : Set α), M.Base x → Disjoint b x → I' ⊆ b → b ⊆ X → X \ B' ∩ M.E ⊆ b → b ⊆ X \ B' ∧ b ⊆ M.E
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>hssJ : X \ B' ∩ M.E ⊆ J<GOAL>J ⊆ X \ B' ∧ J ⊆ M.E
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>hssJ : X \ B' ∩ M.E ⊆ J<GOAL>J ⊆ X \ B'
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>I✝ B✝ X✝ : Set α<VAR>M : Matroid α<VAR>X I' : Set α<VAR>hI'E : I' ⊆ M.E<VAR>B : Set α<VAR>hB : M.Base B<VAR>hI'B : Disjoint I' B<VAR>hI'X : I' ⊆ X<VAR>I : Set α<VAR>hI : M.Basis I (M.E \ X)<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hIB' : I ⊆ B'<VAR>hB'IB : B' ⊆ I ∪ B<VAR>J : Set α<VAR>hJE : J ⊆ M.E<VAR>B'' : Set α<VAR>hB'' : M.Base B''<VAR>hdj : Disjoint J B''<VAR>a✝ : I' ⊆ J<VAR>hJX : J ⊆ X<VAR>hssJ : X ∩ M.E ⊆ B' ∪ J<GOAL>J ⊆ X \ B'