ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>E B : Set α<GOAL>(N.comapOn E f).Base B ↔ N.Basis' (f '' B) (f '' E) ∧ Set.InjOn f B ∧ B ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>E B : Set α<VAR>h : Set.SurjOn f E N.E<GOAL>(N.comapOn E f).Base B ↔ N.Base (f '' B) ∧ Set.InjOn f B ∧ B ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>E B : Set α<VAR>h : Set.BijOn f E N.E<GOAL>(N.comapOn E f).Base B ↔ N.Base (f '' B) ∧ B ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>N : Matroid β<VAR>E : Set α<VAR>h : Set.BijOn f E N.E<GOAL>(N.comapOn E f)✶ = N✶.comapOn E f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : ↑M.E ↪ β<GOAL>(M.mapSetEmbedding f).E = Set.range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : ↑M.E ↪ β<VAR>I : Set β<GOAL>(M.mapSetEmbedding f).Indep I ↔ M.Indep ↑(⇑f ⁻¹' I) ∧ I ⊆ Set.range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : ↑M.E ↪ β<VAR>I : Set β<VAR>hI : (M.mapSetEmbedding f).Indep I<GOAL>∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : ↑M.E ↪ β<VAR>I : Set β<GOAL>(M.mapSetEmbedding f).Indep I ↔ ∃ I₀, M.Indep ↑I₀ ∧ I = ⇑f '' I₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : Set.InjOn f M.E<GOAL>(M.map f hf).E = f '' M.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>M : Matroid α<VAR>hf : Set.InjOn f M.E<VAR>I : Set β<GOAL>(M.map f hf).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>I : Set α<VAR>M : Matroid α<VAR>hI : M.Indep I<VAR>f : α → β<VAR>hf : Set.InjOn f M.E<GOAL>(M.map f hf).Indep (f '' I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>M : Matroid α<VAR>I : Set β<VAR>hf : Set.InjOn f M.E<VAR>hI : (M.map f hf).Indep I<GOAL>∃ I₀, M.Indep I₀ ∧ Set.BijOn f I₀ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>M : Matroid α<VAR>hf : Set.InjOn f M.E<VAR>I : Set α<VAR>hI : I ⊆ M.E<GOAL>(M.map f hf).Indep (f '' I) ↔ M.Indep I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : Set.InjOn f M.E<VAR>B : Set β<GOAL>(M.map f hf).Base B ↔ ∃ B₀, M.Base B₀ ∧ B = f '' B₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<VAR>f : α → β<VAR>hf : Set.InjOn f M.E<GOAL>(M.map f hf).Base (f '' B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>M : Matroid α<VAR>hf : Set.InjOn f M.E<VAR>D : Set β<GOAL>(M.map f hf).Dep D ↔ ∃ D₀, M.Dep D₀ ∧ D = f '' D₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>M : Matroid α<VAR>hf : Set.InjOn f M.E<VAR>B : Set α<VAR>hB : B ⊆ M.E<GOAL>(M.map f hf).Base (f '' B) ↔ M.Base B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>I : Set α<VAR>M : Matroid α<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : Set.InjOn f M.E<GOAL>(M.map f hf).Basis (f '' I) (f '' X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>I X : Set α<VAR>f : α → β<VAR>hf : Set.InjOn f M.E<VAR>hI : I ⊆ M.E<VAR>hX : X ⊆ M.E<GOAL>(M.map f hf).Basis (f '' I) (f '' X) ↔ M.Basis I X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>M : Matroid α<VAR>I X : Set β<VAR>hf : Set.InjOn f M.E<GOAL>(M.map f hf).Basis I X ↔ ∃ I₀ X₀, M.Basis I₀ X₀ ∧ I = f '' I₀ ∧ X = f '' X₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>M : Matroid α<VAR>hf : Set.InjOn f M.E<GOAL>(M.map f hf)✶ = M✶.map f hf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>(Matroid.emptyOn α).map f ⋯ = Matroid.emptyOn β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Set α<VAR>f : α → β<VAR>hf : Set.InjOn f (Matroid.loopyOn E).E<GOAL>(Matroid.loopyOn E).map f hf = Matroid.loopyOn (f '' E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Set α<VAR>f : α → β<VAR>hf : Set.InjOn f (Matroid.freeOn E).E<GOAL>(Matroid.freeOn E).map f hf = Matroid.freeOn (f '' E)
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.map id ⋯ = M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>N : Matroid β<VAR>f : α → β<VAR>h_range : N.E ⊆ Set.range f<VAR>hf : Set.InjOn f (f ⁻¹' N.E)<GOAL>(N.comap f).map f hf = N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>(M.map f ⋯).comap f = M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>E : Set β<VAR>e : ↑M.E ≃ ↑E<VAR>I : Set β<GOAL>(M.mapSetEquiv e).Indep I ↔ M.Indep ↑(⇑e.symm '' E ↓∩ I) ∧ I ⊆ E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>E : Set β<VAR>e : ↑M.E ≃ ↑E<GOAL>(M.mapSetEquiv e).E = E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ↪ β<GOAL>(M.mapEmbedding f).E = ⇑f '' M.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ↪ β<VAR>I : Set β<GOAL>(M.mapEmbedding f).Indep I ↔ M.Indep (⇑f ⁻¹' I) ∧ I ⊆ Set.range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>I : Set α<VAR>M : Matroid α<VAR>hI : M.Indep I<VAR>f : α ↪ β<GOAL>(M.mapEmbedding f).Indep (⇑f '' I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<VAR>f : α ↪ β<GOAL>(M.mapEmbedding f).Base (⇑f '' B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>I : Set α<VAR>M : Matroid α<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α ↪ β<GOAL>(M.mapEmbedding f).Basis (⇑f '' I) (⇑f '' X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ↪ β<VAR>B : Set β<GOAL>(M.mapEmbedding f).Base B ↔ M.Base (⇑f ⁻¹' B) ∧ B ⊆ Set.range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ↪ β<VAR>I X : Set β<GOAL>(M.mapEmbedding f).Basis I X ↔ M.Basis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ Set.range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ≃ β<GOAL>(M.mapEquiv f).E = ⇑f '' M.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ≃ β<GOAL>M.mapEquiv f = M.map ⇑f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ≃ β<VAR>I : Set β<GOAL>(M.mapEquiv f).Indep I ↔ M.Indep (⇑f.symm '' I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ≃ β<VAR>D : Set β<GOAL>(M.mapEquiv f).Dep D ↔ M.Dep (⇑f.symm '' D)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Matroid α<VAR>f : α ≃ β<VAR>B : Set β<GOAL>(M.mapEquiv f).Base B ↔ M.Base (⇑f.symm '' B)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>M : Matroid α<VAR>f : α ≃ β<VAR>I X : Set β<GOAL>(M.mapEquiv f).Basis I X ↔ M.Basis (⇑f.symm '' I) (⇑f.symm '' X)
<VAR>α : Type u_1<VAR>X : Set α<VAR>M : Matroid α<GOAL>(M.restrictSubtype X).E = Set.univ
<VAR>α : Type u_1<VAR>X : Set α<VAR>M : Matroid α<VAR>I : Set ↑X<GOAL>(M.restrictSubtype X).Indep I ↔ M.Indep ↑I
<VAR>α : Type u_1<VAR>X I : Set α<VAR>M : Matroid α<VAR>hIX : I ⊆ X<GOAL>(M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I
<VAR>α : Type u_1<VAR>X I : Set α<VAR>M : Matroid α<GOAL>(M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep (X ∩ I)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Y : Set α<VAR>I X : Set ↑Y<GOAL>(M.restrictSubtype Y).Basis I X ↔ M.Basis' ↑I ↑X
<VAR>α : Type u_1<VAR>X : Set α<VAR>M : Matroid α<VAR>B : Set ↑X<GOAL>(M.restrictSubtype X).Base B ↔ M.Basis' (↑B) X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set ↑M.E<GOAL>(M.restrictSubtype M.E).Base B ↔ M.Base ↑B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I X : Set ↑M.E<GOAL>(M.restrictSubtype M.E).Basis I X ↔ M.Basis ↑I ↑X
<VAR>α : Type u_1<VAR>E : Set α<VAR>M N : Matroid α<VAR>hM : M.E = E<VAR>hN : N.E = E<VAR>h : M.restrictSubtype E = N.restrictSubtype E<GOAL>M = N
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>(M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E
<VAR>α : Type u_1<VAR>E : Set α<VAR>M : Matroid α<VAR>hM : M.E = E<GOAL>(M.restrictSubtype E)✶ = M✶.restrictSubtype E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<GOAL>(M.restrictSubtype X).map Subtype.val ⋯ = M.restrict X
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>(M.restrictSubtype M.E).map Subtype.val ⋯ = M
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F : Set α<VAR>self : M.Flat F<VAR>I X : Set α<GOAL>M.Basis I F → M.Basis I X → X ⊆ F
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F : Set α<GOAL>M.Flat F ↔ (∀ ⦃I X : Set α⦄, M.Basis I F → M.Basis I X → X ⊆ F) ∧ F ⊆ M.E
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F : Set α<VAR>self : M.Flat F<GOAL>F ⊆ M.E
<VAR>α : Type u_2<VAR>M : Matroid α<GOAL>M.Flat M.E
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>ι : Type u_3<VAR>Nonempty ι<VAR>Fs : ι → Set α<VAR>hFs : ∀ (i : ι), M.Flat (Fs i)<GOAL>M.Flat (⋂ i, Fs i)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F : Set α<GOAL>M.Flat F ↔ ∃ (h : F ⊆ M.E), M.subtypeClosure.IsClosed ⟨F, h⟩
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F : ↑(Set.Iic M.E)<GOAL>M.subtypeClosure.IsClosed F ↔ M.Flat ↑F
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure X = ⋂₀ {F | M.Flat F ∧ X ∩ M.E ⊆ F}
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.closure X = ⋂₀ {F | M.Flat F ∧ X ⊆ F}
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure X ⊆ M.E
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.E ⊆ M.closure X ↔ M.closure X = M.E
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure (X ∩ M.E) = M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>X ∩ M.E ⊆ M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>e ∈ M.closure X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → e ∈ F
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>Y : Set α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>Y ⊆ M.closure X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → Y ⊆ F
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>X ⊆ M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F : Set α<VAR>hF : M.Flat F<GOAL>M.closure F = F
<VAR>α : Type u_2<VAR>M : Matroid α<GOAL>M.closure M.E = M.E
<VAR>α : Type u_2<VAR>M : Matroid α<GOAL>M.closure Set.univ = M.E
<VAR>α : Type u_2<VAR>X Y : Set α<VAR>M : Matroid α<VAR>h : X ⊆ Y<GOAL>M.closure X ⊆ M.closure Y
<VAR>α : Type u_2<VAR>M : Matroid α<GOAL>Monotone M.closure
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure (M.closure X) = M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : X ⊆ M.closure Y<GOAL>M.closure X ⊆ M.closure Y
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.closure X ⊆ M.closure Y ↔ X ⊆ M.closure Y
<VAR>α : Type u_2<VAR>X Y : Set α<VAR>M : Matroid α<VAR>hXY : X ⊆ Y<VAR>hY : Y ⊆ M.E := by aesop_mat<GOAL>X ⊆ M.closure Y
<VAR>α : Type u_2<VAR>X Y : Set α<VAR>M : Matroid α<VAR>hXY : X ⊆ Y<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>X ⊆ M.closure Y
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X Y : Set α<VAR>hXY : M.closure X ⊂ M.closure Y<GOAL>∃ e ∈ Y, e ∉ M.closure X
<VAR>α : Type u_2<VAR>X : Set α<VAR>e : α<VAR>M : Matroid α<VAR>h : e ∈ X<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>e ∈ M.closure X
<VAR>α : Type u_2<VAR>X : Set α<VAR>e : α<VAR>M : Matroid α<VAR>heX : e ∈ X<VAR>h : e ∈ M.E := by aesop_mat<GOAL>e ∈ M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<VAR>e : α<VAR>he : e ∈ M.E \ M.closure X<GOAL>e ∉ X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<VAR>e : α<VAR>he : e ∈ M.closure X<GOAL>e ∈ M.E
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>Xs : ι → Set α<GOAL>M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>Xs Ys : ι → Set α<VAR>h : ∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)<GOAL>M.closure (⋃ i, Xs i) = M.closure (⋃ i, Ys i)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>Xs : Set (Set α)<GOAL>M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>Xs : ι → Set α<VAR>A : Set ι<GOAL>M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>Xs Ys : ι → Set α<VAR>A : Set ι<VAR>h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)<GOAL>M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X Y : Set α<GOAL>M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X Y : Set α<GOAL>M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X Y : Set α<GOAL>M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>X : Set α<GOAL>M.closure (insert e (M.closure X)) = M.closure (insert e X)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure X ∪ M.closure ∅ = M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.closure ∅ ∪ M.closure X = M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<VAR>e : α<VAR>he : e ∈ M.closure X<GOAL>M.closure (insert e X) = M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>he : e ∈ M.E := by aesop_mat<GOAL>e ∈ M.closure {e}
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.closure I = {x | M.Basis I (insert x I)}
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.Basis I (insert e I) ↔ e ∈ M.closure I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.Basis I (M.closure I)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>h : M.Basis I X<GOAL>M.closure I = M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>h : M.Basis I (M.closure X)<GOAL>M.closure I = M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>h : M.Basis' I X<GOAL>M.closure I = M.closure X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>h : M.Basis I X<GOAL>X ⊆ M.closure I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>h : M.Basis' I X<GOAL>M.Basis I (M.closure X)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>h : M.Basis I X<GOAL>M.Basis I (M.closure X)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I : Set α<VAR>x : α<VAR>hI : M.Indep I<GOAL>x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I : Set α<VAR>x : α<VAR>hI : M.Indep I<GOAL>x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.Dep (insert e I) ↔ e ∈ M.closure I \ I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>heI : e ∉ I<GOAL>e ∈ M.closure I ↔ M.Dep (insert e I)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>he : e ∈ M.E := by aesop_mat<GOAL>e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>heI : e ∉ I<VAR>he : e ∈ M.E := by aesop_mat<GOAL>e ∉ M.closure I ↔ M.Indep (insert e I)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>heI : e ∉ I<GOAL>M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<GOAL>M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>e : α<VAR>I : Set α<VAR>f : α<VAR>hI : M.Indep (I \ {e})<VAR>heI : e ∈ I<GOAL>M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hXI : X ⊆ M.closure I<GOAL>M.Basis I X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<GOAL>M.Basis I X ↔ M.Indep I ∧ I ⊆ X ∧ X ⊆ M.closure I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<VAR>h : M.E ⊆ M.closure I<GOAL>M.Base I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : M.Base B<GOAL>M.closure B = M.E
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X B : Set α<VAR>hB : M.Base B<VAR>hBX : B ⊆ X<GOAL>M.closure X = M.E
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>B : Set α<GOAL>M.Base B ↔ M.Indep B ∧ M.closure B = M.E
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.Base I ↔ M.E ⊆ M.closure I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I J : Set α<VAR>hI : M.Indep I<VAR>hJI : J ⊆ I<GOAL>M.closure J ∩ I = J
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I : Set α<VAR>Js : Set (Set α)<VAR>hI : M.Indep I<VAR>hne : Js.Nonempty<VAR>hIs : ∀ J ∈ Js, J ⊆ I<GOAL>M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>ι : Sort u_3<VAR>hι : Nonempty ι<VAR>Is : ι → Set α<VAR>h : M.Indep (⋃ i, Is i)<GOAL>M.closure (⋂ i, Is i) = ⋂ i, M.closure (Is i)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>Is : Set (Set α)<VAR>hIs : Is.Nonempty<VAR>h : M.Indep (⋃₀ Is)<GOAL>M.closure (⋂₀ Is) = ⋂ I ∈ Is, M.closure I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>ι : Type u_4<VAR>A : Set ι<VAR>hA : A.Nonempty<VAR>I : ι → Set α<VAR>h : M.Indep (⋃ i ∈ A, I i)<GOAL>M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>ι : Sort u_3<VAR>I : Set α<VAR>hι : Nonempty ι<VAR>Js : ι → Set α<VAR>hI : M.Indep I<VAR>hJs : ∀ (i : ι), Js i ⊆ I<GOAL>M.closure (⋂ i, Js i) = ⋂ i, M.closure (Js i)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>I J : Set α<VAR>h : M.Indep (I ∪ J)<GOAL>M.closure (I ∩ J) = M.closure I ∩ M.closure J
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>hIX : I ⊆ X<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Basis I X ↔ M.Basis I (M.closure X)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<VAR>hIX : I ⊆ X<GOAL>M.Basis I X ↔ M.Basis I (M.closure X) ∧ X ⊆ M.E
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<GOAL>M.Basis' I X ↔ M.Basis I (M.closure X) ∧ I ⊆ X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>∃ I, M.Basis I (X ∩ M.E) ∧ M.Basis I (M.closure X)
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X Y I : Set α<VAR>hI : M.Basis I X<VAR>hY : I ⊆ Y<VAR>h : M.closure X = M.closure Y<VAR>hYE : Y ⊆ M.E := by aesop_mat<GOAL>M.Basis I Y
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<GOAL>M.Basis I (I ∪ X) ↔ M.Indep I ∧ X ⊆ M.closure I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I : Set α<GOAL>M.Basis I X ↔ M.Indep I ∧ X ⊆ M.closure I ∧ I ⊆ X
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X I J : Set α<VAR>hI : M.Basis I X<VAR>hJI : J ⊆ I<VAR>hJ : X ⊆ M.closure J<GOAL>J = I
<VAR>α : Type u_2<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.Basis ∅ X ↔ X ⊆ M.closure ∅
<VAR>α : Type u_1<VAR>f : Bool → α<GOAL>Set.range f = {f false, f true}
<VAR>b : Bool<GOAL>{b}ᶜ = {!b}
<VAR>a : Bool<GOAL>((!a) = true) = (a = false)
<VAR>a b : Bool<GOAL>((a && b) = false) = (a = false ∨ b = false)
<VAR>a b : Bool<GOAL>((a || b) = false) = (a = false ∧ b = false)
<VAR>a : Bool<GOAL>((!a) = false) = (a = true)
<VAR>p : Prop<VAR>d : Decidable p<GOAL>decide p = true ↔ p
<VAR>p : Prop<VAR>Decidable p<GOAL>p → decide p = true
<VAR>p : Prop<VAR>Decidable p<GOAL>decide p = true → p
<VAR>b : Bool<GOAL>¬b = true ↔ b = false
<VAR>p : Prop<VAR>Decidable p<GOAL>¬p → decide p = false
<VAR>p : Prop<VAR>Decidable p<GOAL>decide p = false → ¬p
<VAR>p q : Prop<VAR>Decidable p<VAR>Decidable q<VAR>h : p ↔ q<GOAL>decide p = decide q
<VAR>a b : Bool<GOAL>xor a b = true ↔ Xor' (a = true) (b = true)
<VAR>b : Bool<GOAL>b = false ∨ b = true
<VAR>p : Bool → Prop<VAR>b : Bool<GOAL>(∀ (x : Bool), p x) ↔ p b ∧ p !b
<VAR>p : Bool → Prop<GOAL>(∀ (b : Bool), p b) ↔ p false ∧ p true
<VAR>p : Bool → Prop<VAR>b : Bool<GOAL>(∃ x, p x) ↔ p b ∨ p !b
<VAR>p : Bool → Prop<GOAL>(∃ b, p b) ↔ p false ∨ p true
<VAR>a b : Bool<VAR>H : a = true<GOAL>(a || b) = true
<VAR>a b : Bool<VAR>H : b = true<GOAL>(a || b) = true
<VAR>a b : Bool<GOAL>(a && b) = true → a = true
<VAR>a b : Bool<GOAL>a = true → b = true → (a && b) = true
<VAR>a b : Bool<GOAL>(a && b) = true → b = true
<VAR>a b : Bool<GOAL>a = !b ↔ a ≠ b
<VAR>a b : Bool<GOAL>(!decide (a = b)) = true ↔ a ≠ b
<VAR>a b : Bool<GOAL>a ≠ !b ↔ a = b
<VAR>a b : Bool<GOAL>a = b ∨ a = !b
<VAR>b : Bool<GOAL>(!b) = true ↔ ¬b = true
<VAR>a : Bool<GOAL>(!decide (a = false)) = true → a = true
<VAR>a : Bool<GOAL>(!decide (a = true)) = true → a = false
<VAR>x y : Bool<GOAL>xor x y = true ↔ x ≠ y
<VAR>x y : Bool<GOAL>x < y ↔ x = false ∧ y = true
<VAR>x y : Bool<GOAL>x ≤ y ↔ x = true → y = true
<VAR>x y : Bool<GOAL>(x && y) ≤ x
<VAR>x y : Bool<GOAL>(x && y) ≤ y
<VAR>x y z : Bool<GOAL>x ≤ y → x ≤ z → x ≤ (y && z)
<VAR>x y : Bool<GOAL>x ≤ (x || y)
<VAR>x y : Bool<GOAL>y ≤ (x || y)
<VAR>x y z : Bool<GOAL>x ≤ z → y ≤ z → (x || y) ≤ z
<VAR>b : Bool<GOAL>(b.toNat == 0) = !b
<VAR>b : Bool<GOAL>(b.toNat != 0) = b
<VAR>b : Bool<GOAL>(b.toNat == 1) = b
<VAR>b : Bool<GOAL>(b.toNat != 1) = !b
<VAR>n m : Nat<VAR>h : n ≤ m<GOAL>Bool.ofNat n ≤ Bool.ofNat m
<VAR>b₀ b₁ : Bool<VAR>h : b₀ ≤ b₁<GOAL>b₀.toNat ≤ b₁.toNat
<VAR>b : Bool<GOAL>Bool.ofNat b.toNat = b
<VAR>α : Sort u_1<VAR>f : Bool → α<GOAL>Function.Injective f ↔ f false ≠ f true
<VAR>f : Bool → Bool<VAR>x : Bool<GOAL>f (f (f x)) = f x
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<GOAL>l.all p = true ↔ ∀ (a : α), a ∈ l → p a = true
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<GOAL>(l.all fun a => decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a
<VAR>α : Type u_1<VAR>l : List α<VAR>p : α → Bool<GOAL>l.any p = true ↔ ∃ a, a ∈ l ∧ p a = true
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<GOAL>(l.any fun a => decide (p a)) = true ↔ ∃ a, a ∈ l ∧ p a
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<VAR>p : α → Bool<VAR>h₁ : a ∈ l<VAR>h₂ : p a = true<GOAL>l.any p = true
<VAR>ub i : Nat<VAR>h : i < ub<GOAL>ub.Up (i + 1) i
<VAR>ub : Nat<GOAL>WellFounded ub.Up
<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>StrongRankCondition R<VAR>DecidableEq n<GOAL>Matrix.rank 1 = Fintype.card n
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>Nontrivial R<GOAL>Matrix.rank 0 = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>StrongRankCondition R<VAR>A : Matrix m n R<GOAL>A.rank ≤ Fintype.card n
<VAR>R : Type u_5<VAR>CommRing R<VAR>StrongRankCondition R<VAR>m n : ℕ<VAR>A : Matrix (Fin m) (Fin n) R<GOAL>A.rank ≤ n
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype o<VAR>CommRing R<VAR>StrongRankCondition R<VAR>A : Matrix m n R<VAR>B : Matrix n o R<GOAL>(A * B).rank ≤ A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype o<VAR>CommRing R<VAR>StrongRankCondition R<VAR>A : Matrix m n R<VAR>B : Matrix n o R<GOAL>(A * B).rank ≤ B.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype o<VAR>CommRing R<VAR>StrongRankCondition R<VAR>A : Matrix m n R<VAR>B : Matrix n o R<GOAL>(A * B).rank ≤ min A.rank B.rank
<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>StrongRankCondition R<VAR>DecidableEq n<VAR>A : (Matrix n n R)ˣ<GOAL>(↑A).rank = Fintype.card n
<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>StrongRankCondition R<VAR>DecidableEq n<VAR>A : Matrix n n R<VAR>h : IsUnit A<GOAL>A.rank = Fintype.card n
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>DecidableEq n<VAR>A : Matrix n n R<VAR>B : Matrix m n R<VAR>hA : IsUnit A.det<GOAL>(B * A).rank = B.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>Fintype m<VAR>DecidableEq m<VAR>A : Matrix m m R<VAR>B : Matrix m n R<VAR>hA : IsUnit A.det<GOAL>(A * B).rank = B.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>StrongRankCondition R<VAR>Fintype m<VAR>f : n → m<VAR>e : n ≃ m<VAR>A : Matrix m m R<GOAL>(A.submatrix f ⇑e).rank ≤ A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>Fintype m<VAR>e₁ e₂ : m ≃ n<VAR>A : Matrix m m R<GOAL>((Matrix.reindex e₁ e₂) A).rank = A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>Fintype m<VAR>A : Matrix m m R<VAR>e₁ e₂ : n ≃ m<GOAL>(A.submatrix ⇑e₁ ⇑e₂).rank = A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>Finite m<VAR>DecidableEq n<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>A : Matrix m n R<VAR>v₁ : Basis m R M₁<VAR>v₂ : Basis n R M₂<GOAL>A.rank = FiniteDimensional.finrank R ↥(LinearMap.range ((Matrix.toLin v₂ v₁) A))
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>Fintype m<VAR>StrongRankCondition R<VAR>A : Matrix m n R<GOAL>A.rank ≤ Fintype.card m
<VAR>R : Type u_5<VAR>CommRing R<VAR>StrongRankCondition R<VAR>m n : ℕ<VAR>A : Matrix (Fin m) (Fin n) R<GOAL>A.rank ≤ m