Theorem: Matroid.unifOn_spanning_iff' (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ k : ℕ∞
hk : k ≠ ⊤
⊢ (unifOn E k).Spanning X ↔ k ≤ X.encard ∧ X ⊆ E ∨ X = E
Tactic:
lift k to ℕ using hk
State after:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
⊢ (unifOn E ↑k).Spanning X ↔ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E

State before:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
⊢ (unifOn E ↑k).Spanning X ↔ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E
Tactic:
rw [spanning_iff_er', erk_eq_er_ground, unifOn_ground_eq, unifOn_er_eq', unifOn_er_eq',
  le_min_iff, min_le_iff, min_le_iff, iff_true_intro (le_refl _), or_true, and_true, inter_self]
State after:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
⊢ (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E ↔ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E

State before:
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
⊢ (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E ↔ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E
Tactic:
refine' ⟨fun ⟨h, hXE⟩ ↦ h.elim (fun h ↦ _) (fun h ↦ Or.inl ⟨_,hXE⟩),
  fun h ↦ h.elim (fun ⟨hle, hXE⟩ ↦ ⟨Or.inr (by rwa [inter_eq_self_of_subset_left hXE]), hXE⟩ ) _⟩
State after:
case intro.refine'_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
⊢ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E

case intro.refine'_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : ↑k ≤ (X ∩ E).encard
⊢ ↑k ≤ X.encard

case intro.refine'_3
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
h : ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E
⊢ X = E → (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E

State before:
case intro.refine'_3
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
h : ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E
⊢ X = E → (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
Tactic:
rintro rfl
State after:
case intro.refine'_3
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
h : ↑k ≤ X.encard ∧ X ⊆ X ∨ X = X
⊢ (X.encard ≤ (X ∩ X).encard ∨ ↑k ≤ (X ∩ X).encard) ∧ X ⊆ X

State before:
case intro.refine'_3
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
h : ↑k ≤ X.encard ∧ X ⊆ X ∨ X = X
⊢ (X.encard ≤ (X ∩ X).encard ∨ ↑k ≤ (X ∩ X).encard) ∧ X ⊆ X
Tactic:
rw [inter_self]
State after:
case intro.refine'_3
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
h : ↑k ≤ X.encard ∧ X ⊆ X ∨ X = X
⊢ (X.encard ≤ X.encard ∨ ↑k ≤ X.encard) ∧ X ⊆ X

State before:
case intro.refine'_3
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
h : ↑k ≤ X.encard ∧ X ⊆ X ∨ X = X
⊢ (X.encard ≤ X.encard ∨ ↑k ≤ X.encard) ∧ X ⊆ X
Tactic:
exact ⟨Or.inl rfl.le, Subset.rfl⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
h : ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E
x✝ : ↑k ≤ X.encard ∧ X ⊆ E
hle : ↑k ≤ X.encard
hXE : X ⊆ E
⊢ ↑k ≤ (X ∩ E).encard
Tactic:
rwa [inter_eq_self_of_subset_left hXE]
State after:
no goals

State before:
case intro.refine'_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
⊢ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E
Tactic:
refine' X.finite_or_infinite.elim (fun hfin ↦ Or.inr _) (fun hinf ↦ Or.inl ⟨_, hXE⟩)
State after:
case intro.refine'_1.refine'_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
hfin : X.Finite
⊢ X = E

case intro.refine'_1.refine'_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
hinf : X.Infinite
⊢ ↑k ≤ X.encard

State before:
case intro.refine'_1.refine'_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
hinf : X.Infinite
⊢ ↑k ≤ X.encard
Tactic:
rw [hinf.encard_eq]
State after:
case intro.refine'_1.refine'_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
hinf : X.Infinite
⊢ ↑k ≤ ⊤

State before:
case intro.refine'_1.refine'_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
hinf : X.Infinite
⊢ ↑k ≤ ⊤
Tactic:
apply le_top
State after:
no goals

State before:
case intro.refine'_1.refine'_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
hfin : X.Finite
⊢ X = E
Tactic:
rw [← (hfin.inter_of_left E).eq_of_subset_of_encard_le' inter_subset_right h,
  inter_eq_self_of_subset_left hXE]
State after:
no goals

State before:
case intro.refine'_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : ↑k ≤ (X ∩ E).encard
⊢ ↑k ≤ X.encard
Tactic:
exact h.trans (encard_mono inter_subset_left)
State after:
no goals