Theorem: Matroid.indep_of_encard_le_two (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I
Tactic:
have hne : I.encard ≠ ⊤ := (h.trans_lt (by exact (cmp_eq_lt_iff 2 ⊤).mp rfl : (2 : ℕ∞) < ⊤ )).ne
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I
Tactic:
rw [le_iff_lt_or_eq, encard_eq_two, ← ENat.add_one_le_iff hne, (by norm_num : (2 : ℕ∞) = 1 + 1),
  WithTop.add_le_add_iff_right, encard_le_one_iff_eq] at h
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : (I = ∅ ∨ ∃ x, I = {x}) ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I

α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard + 1 ≤ 1 + 1 ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ 1 ≠ ⊤

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard + 1 ≤ 1 + 1 ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ 1 ≠ ⊤
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard ≤ 2
hI : autoParam (I ⊆ M.E) _auto✝
⊢ 2 < ⊤
Tactic:
exact (cmp_eq_lt_iff 2 ⊤).mp rfl
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : I.encard + 1 ≤ 2 ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ 2 = 1 + 1
Tactic:
norm_num
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
inst✝ : M.Simple
h : (I = ∅ ∨ ∃ x, I = {x}) ∨ ∃ x y, x ≠ y ∧ I = {x, y}
hI : autoParam (I ⊆ M.E) _auto✝
hne : I.encard ≠ ⊤
⊢ M.Indep I
Tactic:
obtain (rfl | ⟨x, rfl⟩) | ⟨x, y, -, rfl⟩ := h
State after:
case inl.inl
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
hI : autoParam (∅ ⊆ M.E) _auto✝
hne : ∅.encard ≠ ⊤
⊢ M.Indep ∅

case inl.inr.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x : α
hI : autoParam ({x} ⊆ M.E) _auto✝
hne : {x}.encard ≠ ⊤
⊢ M.Indep {x}

case inr.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x y : α
hI : autoParam ({x, y} ⊆ M.E) _auto✝
hne : {x, y}.encard ≠ ⊤
⊢ M.Indep {x, y}

State before:
case inr.intro.intro.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x y : α
hI : autoParam ({x, y} ⊆ M.E) _auto✝
hne : {x, y}.encard ≠ ⊤
⊢ M.Indep {x, y}
Tactic:
exact pair_indep
State after:
no goals

State before:
case inl.inl
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
hI : autoParam (∅ ⊆ M.E) _auto✝
hne : ∅.encard ≠ ⊤
⊢ M.Indep ∅
Tactic:
exact M.empty_indep
State after:
no goals

State before:
case inl.inr.intro
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x : α
hI : autoParam ({x} ⊆ M.E) _auto✝
hne : {x}.encard ≠ ⊤
⊢ M.Indep {x}
Tactic:
refine indep_singleton.2 (toNonloop (by aesop_mat))
State after:
no goals

State before:
α : Type u_1
M N : Matroid α
e f g : α
X P D : Set α
inst✝ : M.Simple
x : α
hI : autoParam ({x} ⊆ M.E) _auto✝
hne : {x}.encard ≠ ⊤
⊢ x ∈ M.E
Tactic:
aesop_mat
State after:
no goals