exact Set.disjoint_of_subset (fun ⦃a⦄ a ↦ a) hD_subset this
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ : Set α
hA : A✝ ⊆ B✝
hB✝ : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
c : ℕ∞
hc : M.relRank A B = c
h : (B \ A).Infinite
D : Set α
hD_subset : D ⊆ B \ A
c_finite : c ≠ ⊤
hcc : c + 1 = ↑(ENat.toNat c + 1)
hD_encard : D.encard = c + 1
A' : Set α := A ∪ D
hD_subset_B : D ⊆ B
hA'_subset_B : A' ⊆ B
hA'_indep : M.Indep A'
this : Disjoint A (B \ A)
⊢ Disjoint A D
no goals