Theorem: Matroid.unifOn_er_eq' (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ (unifOn E k).er X = min (X ∩ E).encard k
Tactic:
rw [← er_inter_ground_eq, unifOn_er_eq _ _ (by rw [unifOn_ground_eq]; apply inter_subset_right),
  unifOn_ground_eq]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ X ∩ (unifOn E k).E ⊆ E
Tactic:
rw [unifOn_ground_eq]
State after:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ X ∩ E ⊆ E

State before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ X ∩ E ⊆ E
Tactic:
apply inter_subset_right
State after:
no goals