have hle : M.relRank B' B <= 1 := by
  have := M.relRank_le_encard_diff (B \ {x}) B
  rw [Set.diff_diff_cancel_left (Set.singleton_subset_iff.mpr hxB)] at this
  simp only [Set.encard_singleton] at this; exact 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✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
⊢ M.relRank B' B = 1
α : 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✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this✝ : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
hxB : x ∈ B
hB'B : B' ⊆ B
hAB' : A ⊆ B'
hB'_indep : M.Indep B'
hB'dA : B' \ A = (B \ A) \ {x}
this : (B' \ A).encard = ↑n
hrAB' : M.relRank A B' = ↑n
hle : M.relRank B' B ≤ 1
⊢ M.relRank B' B = 1