Theorem: Matroid.basis'_iff_indep_encard_eq_of_finite (Matroid/Rank.lean)

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
⊢ M.Basis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
Tactic:
refine' ⟨fun h ↦ ⟨h.subset,h.indep, h.er_eq_encard.symm⟩, fun ⟨hIX, hI, hcard⟩  ↦ _⟩
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis' I X

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis' I X
Tactic:
rw [basis'_iff_basis_inter_ground]
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis I (X ∩ M.E)

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
⊢ M.Basis I (X ∩ M.E)
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.subset_basis_of_subset (subset_inter hIX hI.subset_ground)
State after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ M.Basis I (X ∩ M.E)

State before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ M.Basis I (X ∩ M.E)
Tactic:
apply hI.basis_of_subset_of_subset_cl (subset_inter hIX hI.subset_ground)
State after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ X ∩ M.E ⊆ M.cl I

State before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ X ∩ M.E ⊆ M.cl I
Tactic:
obtain rfl := hIfin.eq_of_subset_of_encard_le' hIJ
  (by rw [hcard, ← hJ.er_eq_encard, er_inter_ground_eq ])
State after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
hJ : M.Basis I (X ∩ M.E)
hIJ : I ⊆ I
⊢ X ∩ M.E ⊆ M.cl I

State before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
hJ : M.Basis I (X ∩ M.E)
hIJ : I ⊆ I
⊢ X ∩ M.E ⊆ M.cl I
Tactic:
exact hJ.subset_cl
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.er X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.er X
J : Set α
hJ : M.Basis J (X ∩ M.E)
hIJ : I ⊆ J
⊢ J.encard ≤ I.encard
Tactic:
rw [hcard, ← hJ.er_eq_encard, er_inter_ground_eq ]
State after:
no goals