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

State before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X : Set α
⊢ (M.truncateTo k).er X = min (M.er X) k
Tactic:
simp_rw [le_antisymm_iff, le_er_iff, er_le_iff, truncateTo_indep_iff]
State after:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X : Set α
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k

State before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X : Set α
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
State after:
case intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k

State before:
case intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Tactic:
refine ⟨?_, ?_⟩
State after:
case intro.refine_1
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k

case intro.refine_2
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k

State before:
case intro.refine_2
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Tactic:
obtain ⟨I₀, hI₀, hI₀ss⟩ := exists_subset_encard_eq (min_le_of_left_le (b := k) hI.encard.symm.le)
State after:
case intro.refine_2.intro.intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
I₀ : Set α
hI₀ : I₀ ⊆ I
hI₀ss : I₀.encard = min (M.er X) k
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k

State before:
case intro.refine_2.intro.intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
I₀ : Set α
hI₀ : I₀ ⊆ I
hI₀ss : I₀.encard = min (M.er X) k
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
Tactic:
exact ⟨_, hI₀.trans hI.subset, ⟨hI.indep.subset hI₀, hI₀ss.trans_le (min_le_right _ _)⟩, hI₀ss⟩
State after:
no goals

State before:
case intro.refine_1
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k
Tactic:
intro J hJX hJi
State after:
case intro.refine_1
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
J : Set α
hJX : J ⊆ X
hJi : M.Indep J ∧ J.encard ≤ k
⊢ J.encard ≤ min (M.er X) k

State before:
case intro.refine_1
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
J : Set α
hJX : J ⊆ X
hJi : M.Indep J ∧ J.encard ≤ k
⊢ J.encard ≤ min (M.er X) k
Tactic:
exact le_min (hJi.1.encard_le_er_of_subset hJX) hJi.2
State after:
no goals