Theorem: Matroid.le_r_iff (Matroid/Rank.lean)

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
⊢ n ≤ M.r X ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
Tactic:
simp_rw [← coe_le_er_iff, le_er_iff,]
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
⊢ (∃ I ⊆ X, M.Indep I ∧ I.encard = ↑n) ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
⊢ (∃ I ⊆ X, M.Indep I ∧ I.encard = ↑n) ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
Tactic:
refine ⟨fun ⟨I, hIX, hI, hc⟩ ↦ ⟨I, hIX, hI, by rw [ncard_def, hc, toNat_coe]⟩,
  fun ⟨I, hIX, hI, hc⟩ ↦ ⟨I, hIX, hI, ?_⟩⟩
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ I.encard = ↑n

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ I.encard = ↑n
Tactic:
rw [hI.finite.encard_eq_coe, ← hc]
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ ↑(toNat I.encard) = ↑I.ncard

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.ncard = n
⊢ ↑(toNat I.encard) = ↑I.ncard
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n✝ : ℕ∞
e f : α
inst✝ : M.FiniteRk
n : ℕ
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = ↑n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hc : I.encard = ↑n
⊢ I.ncard = n
Tactic:
rw [ncard_def, hc, toNat_coe]
State after:
no goals