Theorem: Matroid.relRank_le_one_iff (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.relRank X Y ≤ 1 ↔ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
rw [le_iff_eq_or_lt, lt_iff_not_le, ENat.one_le_iff_ne_zero, not_not, relRank_eq_one_iff,
  relRank_eq_zero_iff]
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X ↔ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X ↔ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
refine ⟨?_, fun ⟨e, hY'⟩ ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X → ∃ e ∈ Y, Y ⊆ M.cl (insert e X)

case refine_2
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X

State before:
case refine_2
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Tactic:
by_cases he : e ∈ M.cl X
State after:
case pos
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
he : e ∈ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X

case neg
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
he : e ∉ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X

State before:
case neg
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
he : e ∉ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Tactic:
exact Or.inl ⟨_, ⟨hY'.1, he⟩, hY'.2⟩
State after:
no goals

State before:
case refine_1
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X → ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
rintro (⟨e, he, hY'⟩ | hY')
State after:
case refine_1.inl.intro.intro
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
e : α
he : e ∈ Y \ M.cl X
hY' : Y ⊆ M.cl (insert e X)
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)

case refine_1.inr
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
hY' : Y ⊆ M.cl X
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)

State before:
case refine_1.inr
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
hY' : Y ⊆ M.cl X
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
exact ⟨_, hYne.some_mem, hY'.trans (M.cl_subset_cl (subset_insert _ _))⟩
State after:
no goals

State before:
case refine_1.inl.intro.intro
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
e : α
he : e ∈ Y \ M.cl X
hY' : Y ⊆ M.cl (insert e X)
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
exact ⟨e, he.1, hY'⟩
State after:
no goals

State before:
case pos
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
he : e ∈ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Tactic:
rw [← cl_insert_cl_eq_cl_insert, insert_eq_of_mem he, cl_cl] at hY'
State after:
case pos
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl X
he : e ∈ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X

State before:
case pos
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl X
he : e ∈ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Tactic:
exact Or.inr hY'.2
State after:
no goals