have : (B' \ A).encard = n := by
  rw [hB'dA]
  rw [<-Set.encard_diff_singleton_add_one hx] at h
  simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one] at h
  exact WithTop.add_right_cancel (ENat.coe_toNat_eq_self.mp (refl 1)) h
case refine_2.intro
α : 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}
⊢ M.relRank A B = ↑n.succ
case refine_2.intro
α : 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
⊢ M.relRank A B = ↑n.succ