Theorem: Matroid.unifOn_spanning_iff (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ (unifOn E ↑k).Spanning X ↔ ↑k ≤ X.encard
Tactic:
rw [← ENat.some_eq_coe, unifOn_spanning_iff' (WithTop.coe_lt_top k).ne, and_iff_left hX,
  or_iff_left_iff_imp]
State after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ X = E → ↑k ≤ X.encard

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ X = E → ↑k ≤ X.encard
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ X.encard
hX : X ⊆ X
⊢ ↑k ≤ X.encard

State before:
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ X.encard
hX : X ⊆ X
⊢ ↑k ≤ X.encard
Tactic:
assumption
State after:
no goals