Theorem: Matroid.rFin.basis_of_subset_cl_of_subset_of_encard_le (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 : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
⊢ M.Basis I X
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis (I ∩ M.E)
State after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
⊢ M.Basis I X

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
⊢ M.Basis I X
Tactic:
have hIJ := hJ.subset.trans inter_subset_left
State after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hXI : X ⊆ M.cl I
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X
Tactic:
rw [← cl_inter_ground] at hXI
State after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hXI : X ⊆ M.cl (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hXI : X ⊆ M.cl (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.Basis I X
Tactic:
replace hXI := hXI.trans <| M.cl_subset_cl_of_subset_cl hJ.subset_cl
State after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
⊢ M.Basis I X

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
⊢ M.Basis I X
Tactic:
have hJX := hJ.indep.basis_of_subset_of_subset_cl (hIJ.trans hIX) hXI
State after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hIX : I ⊆ X
hI : I.encard ≤ M.er X
J : Set α
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X
Tactic:
rw [← hJX.encard] at hI
State after:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X

State before:
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.Basis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.cl J
hJX : M.Basis J X
⊢ M.Basis I X
Tactic:
rwa [← Finite.eq_of_subset_of_encard_le' (hX.finite_of_basis hJX) hIJ hI]
State after:
no goals