Theorem: Matroid.truncate_indep_iff (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.truncate.Indep I ↔ M.Indep I ∧ ¬M.Base I
Tactic:
simp only [truncate_indep_iff', and_congr_right_iff]
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.Indep I → (M.Base I → I = ∅ ↔ ¬M.Base I)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
⊢ M.Indep I → (M.Base I → I = ∅ ↔ ¬M.Base I)
Tactic:
exact fun _ ↦ ⟨fun h hB ↦ hB.nonempty.ne_empty (h hB), fun h hB ↦ by contradiction⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
inst✝ : M.RkPos
x✝ : M.Indep I
h : ¬M.Base I
hB : M.Base I
⊢ I = ∅
Tactic:
contradiction
State after:
no goals