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

State before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ M.truncateTo 0 = loopyOn M.E
Tactic:
refine eq_of_indep_iff_indep_forall rfl ?_
State after:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ (M.truncateTo 0).E, (M.truncateTo 0).Indep I ↔ (loopyOn M.E).Indep I

State before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ (M.truncateTo 0).E, (M.truncateTo 0).Indep I ↔ (loopyOn M.E).Indep I
Tactic:
suffices ∀ I ⊆ M.E, I = ∅ → M.Indep I by simpa
State after:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ M.E, I = ∅ → M.Indep I

State before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ M.E, I = ∅ → M.Indep I
Tactic:
rintro I - rfl
State after:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ M.Indep ∅

State before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ M.Indep ∅
Tactic:
exact M.empty_indep
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
this : ∀ I ⊆ M.E, I = ∅ → M.Indep I
⊢ ∀ I ⊆ (M.truncateTo 0).E, (M.truncateTo 0).Indep I ↔ (loopyOn M.E).Indep I
Tactic:
simpa
State after:
no goals