Theorem: Matroid.uniqueBaseOn_dep_iff (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
Tactic:
by_cases hD : D ⊆ E
State after:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E

case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : ¬D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E

State before:
case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : ¬D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
Tactic:
exact iff_of_false (fun h ↦ hD h.subset_ground) (by simp [hD])
State after:
no goals

State before:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : D ⊆ E
⊢ (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E
Tactic:
simp (config := {contextual := true}) [← not_indep_iff (M := uniqueBaseOn I E) hD, hD,
  nonempty_iff_ne_empty, not_imp_not]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hD : ¬D ⊆ E
⊢ ¬(D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E)
Tactic:
simp [hD]
State after:
no goals