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

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ (M.truncateTo ↑k).Base B ↔ M.Indep B ∧ B.encard = ↑k
Tactic:
simp_rw [base_iff_maximal_indep, truncateTo_indep_iff, and_imp]
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ ((M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I) ↔ M.Indep B ∧ B.encard = ↑k

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ ((M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I) ↔ M.Indep B ∧ B.encard = ↑k
Tactic:
refine ⟨fun ⟨⟨hB, hBk⟩, h⟩ ↦ ⟨hB, hBk.antisymm (le_of_not_lt fun hlt ↦ ?_)⟩,
  fun ⟨hB, hBk⟩ ↦ ⟨⟨ hB, hBk.le⟩,
    fun I _ hIk hBI ↦ ?_⟩ ⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
⊢ False

case refine_2
α : Type u_1
M : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝¹ : M.Indep B ∧ B.encard = ↑k
hB : M.Indep B
hBk : B.encard = ↑k
I : Set α
x✝ : M.Indep I
hIk : I.encard ≤ ↑k
hBI : B ⊆ I
⊢ B = I

State before:
case refine_2
α : Type u_1
M : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝¹ : M.Indep B ∧ B.encard = ↑k
hB : M.Indep B
hBk : B.encard = ↑k
I : Set α
x✝ : M.Indep I
hIk : I.encard ≤ ↑k
hBI : B ⊆ I
⊢ B = I
Tactic:
exact (finite_of_encard_eq_coe hBk).eq_of_subset_of_encard_le' hBI (hIk.trans_eq hBk.symm)
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
⊢ False
Tactic:
obtain ⟨B', hB', hJB'⟩ := hB.exists_base_superset
State after:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB' : B ⊆ B'
⊢ False

State before:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB' : B ⊆ B'
⊢ False
Tactic:
obtain ⟨J, hBJ, hJB', h'⟩ :=
  exists_superset_subset_encard_eq hJB' hBk (h_rk.trans_eq hB'.encard.symm)
State after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False

State before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False
Tactic:
rw [h _ (hB'.indep.subset hJB') h'.le hBJ] at hlt
State after:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hlt : J.encard < ↑k
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False

State before:
case refine_1.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hlt : J.encard < ↑k
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False
Tactic:
exact hlt.ne h'
State after:
no goals