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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E k → M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
Tactic:
rintro rfl
State after:
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E k).E = E ∧ ∀ (I : Set α), (unifOn E k).Indep I ↔ I.encard ≤ k ∧ I ⊆ E

State before:
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E k).E = E ∧ ∀ (I : Set α), (unifOn E k).Indep I ↔ I.encard ≤ k ∧ I ⊆ E
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
x✝ : M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
hE : M.E = E
h : ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
⊢ M.E = (unifOn E k).E
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
x✝¹ : M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
hE : M.E = E
h : ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
I : Set α
x✝ : I ⊆ M.E
⊢ M.Indep I ↔ (unifOn E k).Indep I
Tactic:
simpa using h I
State after:
no goals