Theorem: Matroid.spanning_iff_er' (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 : α
inst✝ : M.FiniteRk
⊢ M.Spanning X ↔ M.erk ≤ M.er X ∧ X ⊆ M.E
Tactic:
refine' ⟨fun h ↦ _, fun ⟨hr, hX⟩ ↦ _⟩
State after:
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.erk ≤ M.er X ∧ X ⊆ M.E

case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
⊢ M.Spanning X

State before:
case refine'_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
⊢ M.Spanning X
Tactic:
obtain ⟨J, hJ⟩ := M.exists_basis X
State after:
case refine'_2.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
⊢ M.Spanning X

State before:
case refine'_2.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
⊢ M.Spanning X
Tactic:
obtain ⟨B, hB, hJB⟩ := hJ.indep.exists_base_superset
State after:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
B : Set α
hB : M.Base B
hJB : J ⊆ B
⊢ M.Spanning X

State before:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hr : M.erk ≤ M.er X
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
B : Set α
hB : M.Base B
hJB : J ⊆ B
⊢ M.Spanning X
Tactic:
rw [← hJ.encard, ← hB.encard] at hr
State after:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
B : Set α
hr : B.encard ≤ J.encard
hB : M.Base B
hJB : J ⊆ B
⊢ M.Spanning X

State before:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
B : Set α
hr : B.encard ≤ J.encard
hB : M.Base B
hJB : J ⊆ B
⊢ M.Spanning X
Tactic:
obtain rfl := hB.finite.eq_of_subset_of_encard_le hJB hr
State after:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
hr : J.encard ≤ J.encard
hB : M.Base J
hJB : J ⊆ J
⊢ M.Spanning X

State before:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
hr : J.encard ≤ J.encard
hB : M.Base J
hJB : J ⊆ J
⊢ M.Spanning X
Tactic:
rw [spanning_iff_superset_base]
State after:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
hr : J.encard ≤ J.encard
hB : M.Base J
hJB : J ⊆ J
⊢ ∃ B, M.Base B ∧ B ⊆ X

State before:
case refine'_2.intro.intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
x✝ : M.erk ≤ M.er X ∧ X ⊆ M.E
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J X
hr : J.encard ≤ J.encard
hB : M.Base J
hJB : J ⊆ J
⊢ ∃ B, M.Base B ∧ B ⊆ X
Tactic:
exact ⟨J, hB, hJ.subset⟩
State after:
no goals

State before:
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.erk ≤ M.er X ∧ X ⊆ M.E
Tactic:
rw [erk_eq_er_ground, ← er_cl_eq _ X, h.cl_eq]
State after:
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.er M.E ≤ M.er M.E ∧ X ⊆ M.E

State before:
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.er M.E ≤ M.er M.E ∧ X ⊆ M.E
Tactic:
exact ⟨rfl.le, h.subset_ground⟩
State after:
no goals