refine (@ENat.nat_induction P n ?_ ?_ ?_)
α : 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 : ℕ∞
⊢ P n
case refine_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 : ℕ∞
⊢ P 0

case refine_2
α : 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 : ℕ), P ↑n → P ↑n.succ

case refine_3
α : 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 : ℕ), P ↑n) → P ⊤