ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>e : α<VAR>X : Set α<VAR>M : Matroid α<VAR>he : e ∈ M.E<VAR>hX : X ⊆ M.E<GOAL>insert e X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.E ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<GOAL>B ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>e : α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<VAR>hx : e ∈ B₁ \ B₂<GOAL>∃ y ∈ B₂ \ B₁, M.Base (insert y (B₁ \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>e : α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<VAR>hxB₁ : e ∈ B₁<VAR>hxB₂ : e ∉ B₂<GOAL>∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.Base (insert y (B₁ \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<VAR>hB₁B₂ : B₁ ⊆ B₂<GOAL>B₁ = B₂
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B X : Set α<VAR>hB : M.Base B<VAR>hX : X ⊂ B<GOAL>¬M.Base X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>e : α<VAR>hB : M.Base B<VAR>heB : e ∉ B<GOAL>¬M.Base (insert e B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<GOAL>(B₁ \ B₂).encard = (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<GOAL>(B₁ \ B₂).ncard = (B₂ \ B₁).ncard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<GOAL>B₁.encard = B₂.encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<GOAL>B₁.ncard = B₂.ncard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' : Set α<VAR>hB : M.Base B<VAR>h : B.Finite<VAR>hB' : M.Base B'<GOAL>B'.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ : Set α<VAR>hB : M.Base B<VAR>h : B.Infinite<VAR>hB₁ : M.Base B₁<GOAL>B₁.Infinite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>M.FiniteRk<VAR>hB : M.Base B<GOAL>B.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>M.InfiniteRk<VAR>hB : M.Base B<GOAL>B.Infinite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>h : M.RkPos<GOAL>¬M.Base ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>M.RkPos<VAR>hB : M.Base B<GOAL>B.Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<VAR>h : B.Nonempty<GOAL>M.RkPos
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<VAR>hfin : B.Finite<GOAL>M.FiniteRk
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<VAR>h : B.Infinite<GOAL>M.InfiniteRk
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>M.InfiniteRk<GOAL>¬M.FiniteRk
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>M.FiniteRk<GOAL>¬M.InfiniteRk
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.FiniteRk ∨ M.InfiniteRk
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<GOAL>(B₁ \ B₂).Finite ↔ (B₂ \ B₁).Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<GOAL>(B₁ \ B₂).Infinite ↔ (B₂ \ B₁).Infinite
<VAR>α : Type u_1<VAR>M₁ M₂ : Matroid α<VAR>hE : M₁.E = M₂.E<VAR>h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.Base B ↔ M₂.Base B)<GOAL>M₁ = M₂
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : B ⊆ M.E := by aesop_mat<GOAL>M.Base (M.E \ B) ↔ B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<GOAL>M.Indep I ↔ ∃ B, M.Base B ∧ I ⊆ B
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>{I | M.Indep I} = ↑(lowerClosure {B | M.Base B})
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>∃ B, M.Base B ∧ I ⊆ B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>D : Set α<GOAL>M.Dep D ↔ ¬M.Indep D ∧ D ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>{D | M.Dep D} = {I | M.Indep I}ᶜ ∩ Set.Iic M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>I ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>D : Set α<VAR>hD : M.Dep D<GOAL>D ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Indep X ∨ M.Dep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>¬M.Dep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>D : Set α<VAR>hD : M.Dep D<GOAL>¬M.Indep D
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>D : Set α<VAR>hD : ¬M.Indep D<VAR>hDE : D ⊆ M.E := by aesop_mat<GOAL>M.Dep D
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : ¬M.Dep I<VAR>hIE : I ⊆ M.E := by aesop_mat<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>¬M.Dep X ↔ M.Indep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>¬M.Indep X ↔ M.Dep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<GOAL>M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J : Set α<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>D X : Set α<VAR>hD : M.Dep D<VAR>hDX : D ⊆ X<VAR>hXE : X ⊆ M.E := by aesop_mat<GOAL>M.Dep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<GOAL>M.Indep B
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.Indep ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>D : Set α<VAR>hD : M.Dep D<GOAL>D.Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>M.FiniteRk<VAR>hI : M.Indep I<GOAL>I.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>hne : I.Nonempty<GOAL>M.RkPos
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>X : Set α<GOAL>M.Indep (I ∩ X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>X : Set α<GOAL>M.Indep (X ∩ I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>X : Set α<GOAL>M.Indep (I \ X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I : Set α<VAR>hB : M.Base B<VAR>hI : M.Indep I<VAR>hBI : B ⊆ I<GOAL>B = I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<GOAL>M.Base B ↔ M.Indep B ∧ ∀ (I : Set α), M.Indep I → B ⊆ I → B = I
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>{B | M.Base B} = maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>h : ∀ (J : Set α), M.Indep J → I ⊆ J → I = J<GOAL>M.Base I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B X : Set α<VAR>hB : M.Base B<VAR>h : B ⊂ X<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Dep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>e : α<VAR>hB : M.Base B<VAR>heB : e ∉ B<VAR>he : e ∈ M.E := by aesop_mat<GOAL>M.Dep (insert e B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>e : α<VAR>hB : M.Base B<VAR>heB : M.Indep (insert e B)<GOAL>e ∈ B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' : Set α<VAR>e : α<VAR>hB : M.Base B<VAR>hB' : M.Base B'<VAR>h : B \ B' = {e}<GOAL>∃ f ∈ B' \ B, B' = insert f B \ {e}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f (B \ {e}))<GOAL>M.Base (insert f (B \ {e}))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>he : e ∈ B<VAR>hf : f ∉ B<VAR>hI : M.Indep (insert f B \ {e})<GOAL>M.Base (insert f B \ {e})
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>e : α<VAR>hB : M.Base B<VAR>h : e ∈ M.E \ B<GOAL>M.Dep (insert e B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I : Set α<VAR>hI : M.Indep I<VAR>hI' : ¬M.Base I<VAR>hB : M.Base B<GOAL>∃ e ∈ B \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B : Set α<VAR>hI : M.Indep I<VAR>hInotmax : I ∉ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<VAR>hB : B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}<GOAL>∃ x ∈ B \ I, M.Indep (insert x I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Indep B<VAR>hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)<GOAL>M.Base B
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.Indep M.E ↔ M.Base M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊂ B<VAR>hB' : M.Base B'<GOAL>∃ e ∈ B' \ I, M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M₁ M₂ : Matroid α<VAR>hE : M₁.E = M₂.E<VAR>h : ∀ I ⊆ M₁.E, M₁.Indep I ↔ M₂.Indep I<GOAL>M₁ = M₂
<VAR>α : Type u_1<VAR>M₁ M₂ : Matroid α<GOAL>M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ I ⊆ M₁.E, M₁.Indep I ↔ M₂.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>self : M.Finitary<VAR>I : Set α<GOAL>(∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>M.Finitary<VAR>I : Set α<VAR>h : ∀ J ⊆ I, J.Finite → M.Indep J<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>I : Set α<VAR>M : Matroid α<VAR>M.Finitary<GOAL>M.Indep I ↔ ∀ J ⊆ I, J.Finite → M.Indep J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<GOAL>X ⊆ M.E → Matroid.ExistsMaximalSubsetProperty M.Indep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis' I X<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis I X<GOAL>M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis I X<GOAL>I ⊆ X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis I X<GOAL>M.Basis' I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis' I X<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis' I X<GOAL>I ⊆ X
<VAR>α : Type u_1<VAR>X : Set α<VAR>M : Matroid α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>{I | M.Basis I X} = maximals (fun x x_1 => x ⊆ x_1) ({I | M.Indep I} ∩ Set.Iic X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis I X<GOAL>X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis I X<GOAL>M.Basis I (X ∩ M.E)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis I X<GOAL>I ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J X : Set α<VAR>hI : M.Basis I X<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<GOAL>I = J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis I X<VAR>M.FiniteRk<GOAL>I.Finite
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<GOAL>M.Basis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Basis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<GOAL>M.Basis' I X ↔ M.Basis I (X ∩ M.E)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Basis' I X ↔ M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<GOAL>M.Basis I X ↔ M.Basis' I X ∧ X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hIX : M.Basis' I X<GOAL>M.Basis I (X ∩ M.E)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J X : Set α<VAR>hI : M.Basis' I X<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<VAR>hJX : J ⊆ X<GOAL>I = J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>e : α<VAR>hI : M.Basis' I X<VAR>he : e ∈ X \ I<GOAL>¬M.Indep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Basis I X ↔ I ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I ∧ I ⊆ X}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Basis I X ↔ I ∈ maximals (fun x x_1 => x ⊆ x_1) fun I => M.Indep I ∧ I ⊆ X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X Y : Set α<VAR>hI : M.Basis I X<VAR>hIY : I ⊆ Y<VAR>hYX : Y ⊆ X<GOAL>M.Basis I Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<GOAL>M.Basis I I ↔ M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>h : M.Indep I<GOAL>M.Basis I I
<VAR>α : Type u_1<VAR>I : Set α<VAR>M : Matroid α<GOAL>M.Basis I ∅ ↔ I = ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X Y : Set α<VAR>hI : M.Basis I X<VAR>hIY : I ⊂ Y<VAR>hYX : Y ⊆ X<GOAL>M.Dep Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>he : e ∈ X \ I<GOAL>M.Dep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>he : e ∈ X<VAR>hIe : M.Indep (insert e I)<GOAL>e ∈ I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>e : α<VAR>hI : M.Basis' I X<VAR>he : e ∈ X<VAR>hIe : M.Indep (insert e I)<GOAL>e ∈ I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J X : Set α<VAR>hI : M.Basis I X<VAR>hJI : J ⊂ I<GOAL>¬M.Basis J X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>∃ J, M.Basis J X ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<GOAL>∃ J, M.Basis' J X ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>∃ I, M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<GOAL>∃ I, M.Basis' I X
<VAR>α : Type u_1<VAR>X Y : Set α<VAR>M : Matroid α<VAR>hXY : X ⊆ Y<VAR>hY : Y ⊆ M.E := by aesop_mat<GOAL>∃ I J, M.Basis I X ∧ M.Basis J Y ∧ I ⊆ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X Y : Set α<VAR>hI : M.Basis I X<VAR>hXY : X ⊆ Y<VAR>hY : Y ⊆ M.E := by aesop_mat<GOAL>∃ J, M.Basis J Y ∧ J ∩ X = I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<VAR>hY : Y ⊆ M.E := by aesop_mat<GOAL>∃ I, M.Basis I (X ∪ Y) ∧ M.Basis (I ∩ Y) Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J : Set α<VAR>hI : M.Indep I<VAR>hJ : M.Basis J I<GOAL>J = I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Basis I X<GOAL>∃ B, M.Base B ∧ I = B ∩ X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<GOAL>M.Basis B M.E ↔ M.Base B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<GOAL>M.Basis B M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<GOAL>M.Basis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>he : ∀ e ∈ X \ I, M.Dep (insert e I)<GOAL>M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>e : α<VAR>hI : M.Indep I<GOAL>M.Basis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>ι : Type u_2<VAR>X I : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis (I i) (X i)<VAR>h_ind : M.Indep (⋃ i, I i)<GOAL>M.Basis (⋃ i, I i) (⋃ i, X i)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>ι : Type u_2<VAR>Nonempty ι<VAR>X : ι → Set α<VAR>hI : ∀ (i : ι), M.Basis I (X i)<GOAL>M.Basis I (⋃ i, X i)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>Xs : Set (Set α)<VAR>hne : Xs.Nonempty<VAR>h : ∀ X ∈ Xs, M.Basis I X<GOAL>M.Basis I (⋃₀ Xs)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.Basis I {x | M.Basis I (insert x I)}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J X Y : Set α<VAR>hIX : M.Basis I X<VAR>hJY : M.Basis J Y<VAR>h : M.Indep (I ∪ J)<GOAL>M.Basis (I ∪ J) (X ∪ Y)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X Y : Set α<VAR>hIX : M.Basis I X<VAR>hIY : M.Basis I Y<GOAL>M.Basis I (X ∪ Y)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J X : Set α<VAR>hI : M.Basis I X<VAR>hJ : M.Indep J<VAR>hIJ : I ⊆ J<GOAL>M.Basis J (J ∪ X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>h : M.Indep (insert e I)<GOAL>M.Basis (insert e I) (insert e X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I X : Set α<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<VAR>hIX : M.Basis I X<GOAL>M.Base I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I : Set α<VAR>hI : M.Indep I<VAR>hB : M.Base B<GOAL>∃ B', M.Base B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J X : Set α<VAR>hIX : M.Basis I X<VAR>hIJ : I ⊆ J<VAR>hJ : M.Indep J<GOAL>J ∩ X = I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I J X : Set α<VAR>hI : M.Basis' I X<VAR>hIJ : I ⊆ J<VAR>hJ : M.Indep J<GOAL>J ∩ X = I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<GOAL>M.Basis B X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : X ⊆ Y<VAR>hY : Y ⊆ M.E := by aesop_mat<GOAL>∃ I J, M.Basis I X ∧ M.Basis (I ∪ J) Y ∧ Disjoint X J
<VAR>α : Type u_1<VAR>E : Set α<VAR>hE : E.Finite<GOAL>{M | M.E ⊆ E}.Finite
<VAR>α : Type u_1<VAR>E : Set α<VAR>hE : E.Finite<GOAL>{M | M.E = E}.Finite
<VAR>α : Sort u<GOAL>Function.Injective PLift.up
<VAR>α : Sort u<GOAL>Function.Surjective PLift.up
<VAR>α : Sort u<GOAL>Function.Bijective PLift.up
<VAR>α : Sort u<VAR>x y : α<GOAL>{ down := x } = { down := y } ↔ x = y
<VAR>α : Sort u<GOAL>Function.Surjective PLift.down
<VAR>α : Sort u<GOAL>Function.Bijective PLift.down
<VAR>α : Sort u<VAR>p : PLift α → Prop<GOAL>(∀ (x : PLift α), p x) ↔ ∀ (x : α), p { down := x }
<VAR>α : Sort u<VAR>p : PLift α → Prop<GOAL>(∃ x, p x) ↔ ∃ x, p { down := x }
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<GOAL>Function.Injective (PLift.map f) ↔ Function.Injective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<GOAL>Function.Surjective (PLift.map f) ↔ Function.Surjective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<GOAL>Function.Bijective (PLift.map f) ↔ Function.Bijective f
<VAR>α : Type u<GOAL>Function.Injective ULift.up
<VAR>α : Type u<GOAL>Function.Surjective ULift.up
<VAR>α : Type u<GOAL>Function.Bijective ULift.up
<VAR>α : Type u<VAR>x y : α<GOAL>{ down := x } = { down := y } ↔ x = y
<VAR>α : Type u<GOAL>Function.Surjective ULift.down
<VAR>α : Type u<GOAL>Function.Bijective ULift.down
<VAR>α : Type u<VAR>p : ULift.{u_1, u} α → Prop<GOAL>(∀ (x : ULift.{u_1, u} α), p x) ↔ ∀ (x : α), p { down := x }
<VAR>α : Type u<VAR>p : ULift.{u_1, u} α → Prop<GOAL>(∃ x, p x) ↔ ∃ x, p { down := x }
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Injective (ULift.map f) ↔ Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Surjective (ULift.map f) ↔ Function.Surjective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Function.Bijective (ULift.map f) ↔ Function.Bijective f
<VAR>α : Type u<VAR>x y : ULift.{u_1, u} α<VAR>h : x.down = y.down<GOAL>x = y
<VAR>α : Type u_1<VAR>x y : ULift.{u_2, u_1} α<GOAL>x = y ↔ x.down = y.down
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<GOAL>s.sup f = (Multiset.map f s.val).sup
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>f : β → α<GOAL>∅.sup f = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>h : b ∉ s<GOAL>(Finset.cons b s h).sup f = f b ⊔ s.sup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<VAR>DecidableEq β<VAR>b : β<GOAL>(insert b s).sup f = f b ⊔ s.sup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>f : γ → β<VAR>g : β → α<GOAL>(Finset.image f s).sup g = s.sup (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset γ<VAR>f : γ ↪ β<VAR>g : β → α<GOAL>(Finset.map f s).sup g = s.sup (g ∘ ⇑f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>f : β → α<VAR>b : β<GOAL>{b}.sup f = f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f g : β → α<GOAL>s.sup (f ⊔ g) = s.sup f ⊔ s.sup g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s₁ s₂ : Finset β<VAR>f g : β → α<VAR>hs : s₁ = s₂<VAR>hfg : ∀ a ∈ s₂, f a = g a<GOAL>s₁.sup f = s₂.sup g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_5<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>FunLike F α β<VAR>SupBotHomClass F α β<VAR>f : F<VAR>s : Finset ι<VAR>g : ι → α<GOAL>f (s.sup g) = s.sup (⇑f ∘ g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>a : α<GOAL>(s.sup fun x => a) ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<VAR>b : β<VAR>hb : b ∈ s<GOAL>f b ≤ s.sup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<VAR>b : β<VAR>hb : b ∈ s<VAR>h : a ≤ f b<GOAL>a ≤ s.sup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s₁ s₂ : Finset β<VAR>f : β → α<VAR>DecidableEq β<GOAL>(s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>f : β → α<VAR>DecidableEq β<VAR>s : Finset γ<VAR>t : γ → Finset β<GOAL>(s.biUnion t).sup f = s.sup fun x => (t x).sup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>h : s.Nonempty<VAR>c : α<GOAL>(s.sup fun x => c) = c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<GOAL>(s.sup fun x => ⊥) = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f g : β → α<VAR>p : β → Prop<VAR>DecidablePred p<GOAL>(s.sup fun i => if p i then f i else g i) = (Finset.filter p s).sup f ⊔ (Finset.filter (fun i => ¬p i) s).sup g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f g : β → α<VAR>h : ∀ b ∈ s, f b ≤ g b<GOAL>s.sup f ≤ s.sup g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s₁ s₂ : Finset β<VAR>f : β → α<VAR>h : s₁ ⊆ s₂<GOAL>s₁.sup f ≤ s₂.sup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>t : Finset γ<VAR>f : β → γ → α<GOAL>(s.sup fun b => t.sup (f b)) = t.sup fun c => s.sup fun b => f b c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<GOAL>(s.attach.sup fun x => f ↑x) = s.sup f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>t : Finset γ<VAR>f : β × γ → α<GOAL>(s ×ˢ t).sup f = s.sup fun i => t.sup fun i' => f (i, i')
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>t : Finset γ<VAR>f : β × γ → α<GOAL>(s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f (i, i')
<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>OrderBot α<VAR>OrderBot β<VAR>s : Finset ι<VAR>t : Finset κ<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>f : ι → α<VAR>g : κ → β<GOAL>(s ×ˢ t).sup (Prod.map f g) = (s.sup f, t.sup g)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(s.erase ⊥).sup id = s.sup id
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>GeneralizedBooleanAlgebra α<VAR>s : Finset β<VAR>f : β → α<VAR>a : α<GOAL>(s.sup fun b => f b \ a) = s.sup f \ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>SemilatticeSup γ<VAR>OrderBot γ<VAR>s : Finset β<VAR>f : β → α<VAR>g : α → γ<VAR>g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y<VAR>bot : g ⊥ = ⊥<GOAL>g (s.sup f) = s.sup (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>P : α → Prop<VAR>Pbot : P ⊥<VAR>Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)<VAR>t : Finset β<VAR>f : β → { x // P x }<GOAL>↑(t.sup f) = t.sup fun x => ↑(f x)
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → Multiset β<GOAL>(s.sup f).toFinset = s.sup fun x => (f x).toFinset
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>DecidableEq α<VAR>l : List α<GOAL>List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l = l.toFinset.sup id
<VAR>s : Finset ℕ<GOAL>s ⊆ Finset.range (s.sup id).succ
<VAR>s : Finset ℕ<GOAL>∃ n, s ⊆ Finset.range n
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Finset β<VAR>f : β → α<VAR>p : α → Prop<VAR>hb : p ⊥<VAR>hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)<VAR>hs : ∀ b ∈ s, p (f b)<GOAL>p (s.sup f)
<VAR>α : Type u_7<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>t : Finset α<GOAL>(∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>s : Set α<VAR>w₁ : ⊥ ∈ s<VAR>w₂ : ∀ x ∈ s, ∀ y ∈ s, x ⊔ y ∈ s<VAR>ι : Type u_7<VAR>t : Finset ι<VAR>p : ι → α<VAR>h : ∀ i ∈ t, p i ∈ s<GOAL>t.sup p ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>f : β → α<VAR>S : Finset β<GOAL>S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥