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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ Nonempty (M ≂ unif a b) ↔ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
rw [nonempty_iso_unif_iff]
State after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) ↔ M = unifOn M.E ↑a ∧ M.E.encard = ↑b

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) ↔ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
exact ⟨by rintro ⟨E, rfl, h⟩; simp [h], fun h ↦ ⟨M.E, by simpa⟩⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) → M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
rintro ⟨E, rfl, h⟩
State after:
case intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
h : E.encard = ↑b
⊢ unifOn E ↑a = unifOn (unifOn E ↑a).E ↑a ∧ (unifOn E ↑a).E.encard = ↑b

State before:
case intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
h : E.encard = ↑b
⊢ unifOn E ↑a = unifOn (unifOn E ↑a).E ↑a ∧ (unifOn E ↑a).E.encard = ↑b
Tactic:
simp [h]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
h : M = unifOn M.E ↑a ∧ M.E.encard = ↑b
⊢ M = unifOn M.E ↑a ∧ M.E.encard = ↑b
Tactic:
simpa
State after:
no goals