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

State before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ (loopyOn E).truncateTo k = loopyOn E
Tactic:
apply eq_of_indep_iff_indep_forall (by simp)
State after:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ ((loopyOn E).truncateTo k).E, ((loopyOn E).truncateTo k).Indep I ↔ (loopyOn E).Indep I

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

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

State before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∅.encard ≤ k
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ((loopyOn E).truncateTo k).E = (loopyOn E).E
Tactic:
simp
State after:
no goals

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