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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E 2 ↔ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple
Tactic:
constructor
State after:
case mp
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E 2 → M.E = E ∧ M.erk ≤ 2 ∧ M.Simple

case mpr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple → M = unifOn E 2

State before:
case mpr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple → M = unifOn E 2
Tactic:
rintro ⟨rfl, hr, hM⟩
State after:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ M = unifOn M.E 2

State before:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ M = unifOn M.E 2
Tactic:
simp only [eq_iff_indep_iff_indep_forall, unifOn_ground_eq, unifOn_indep_iff, true_and]
State after:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ ∀ I ⊆ M.E, M.Indep I ↔ I.encard ≤ 2 ∧ I ⊆ M.E

State before:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ ∀ I ⊆ M.E, M.Indep I ↔ I.encard ≤ 2 ∧ I ⊆ M.E
Tactic:
exact fun I hIE ↦ ⟨fun hI ↦ ⟨hI.encard_le_erk.trans hr, hIE⟩,
  fun ⟨hcard, _⟩ ↦ indep_of_encard_le_two hcard⟩
State after:
no goals

State before:
case mp
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E 2 → M.E = E ∧ M.erk ≤ 2 ∧ M.Simple
Tactic:
rintro rfl
State after:
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E 2).E = E ∧ (unifOn E 2).erk ≤ 2 ∧ (unifOn E 2).Simple

State before:
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E 2).E = E ∧ (unifOn E 2).erk ≤ 2 ∧ (unifOn E 2).Simple
Tactic:
simp_rw [unifOn_ground_eq, unifOn_erk_eq, min_le_iff, iff_true_intro rfl.le,
  or_true, true_and, simple_iff_forall_pair_indep, unifOn_ground_eq, unifOn_indep_iff,
  and_iff_right (encard_pair_le _ _)]
State after:
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ ∀ ⦃e f : α⦄, e ∈ E → f ∈ E → {e, f} ⊆ E

State before:
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ ∀ ⦃e f : α⦄, e ∈ E → f ∈ E → {e, f} ⊆ E
Tactic:
exact fun e f ↦ pair_subset
State after:
no goals