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

State before:
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ∞
hk : k ≠ ⊤
⊢ unifOn E k ／ C = unifOn (E \ C) (k - (E ∩ C).encard)
Tactic:
lift k to ℕ using hk
State after:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
⊢ unifOn E ↑k ／ C = unifOn (E \ C) (↑k - (E ∩ C).encard)

State before:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
⊢ unifOn E ↑k ／ C = unifOn (E \ C) (↑k - (E ∩ C).encard)
Tactic:
refine' eq_of_spanning_iff_spanning_forall (by simp) (fun S hS ↦ _)
State after:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ (unifOn E ↑k ／ C).E
⊢ (unifOn E ↑k ／ C).Spanning S ↔ (unifOn (E \ C) (↑k - (E ∩ C).encard)).Spanning S

State before:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ (unifOn E ↑k ／ C).E
⊢ (unifOn E ↑k ／ C).Spanning S ↔ (unifOn (E \ C) (↑k - (E ∩ C).encard)).Spanning S
Tactic:
simp only [ge_iff_le, contract_ground, unifOn_ground_eq, diff_self_inter, subset_diff] at hS
State after:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ (unifOn E ↑k ／ C).Spanning S ↔ (unifOn (E \ C) (↑k - (E ∩ C).encard)).Spanning S

State before:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ (unifOn E ↑k ／ C).Spanning S ↔ (unifOn (E \ C) (↑k - (E ∩ C).encard)).Spanning S
Tactic:
rw [← contract_inter_ground_eq, unifOn_ground_eq, inter_comm,
  contract_spanning_iff, unifOn_spanning_iff', unifOn_spanning_iff', tsub_le_iff_right,
  iff_true_intro (disjoint_of_subset_right inter_subset_right hS.2), and_true,
   ← encard_union_eq (disjoint_of_subset_right inter_subset_right hS.2), union_subset_iff,
  and_iff_left inter_subset_left, and_iff_left hS.1, subset_diff, union_inter_distrib_left,
  and_iff_left hS, union_eq_self_of_subset_left hS.1, inter_eq_left,
  subset_antisymm_iff, subset_diff, and_iff_right hS, diff_subset_iff, union_comm C]
State after:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ ↑k - (E ∩ C).encard ≠ ⊤

case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ ↑k ≠ ⊤

State before:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ ↑k ≠ ⊤
Tactic:
exact WithTop.coe_ne_top
State after:
no goals

State before:
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
⊢ (unifOn E ↑k ／ C).E = (unifOn (E \ C) (↑k - (E ∩ C).encard)).E
Tactic:
simp
State after:
no goals

State before:
case intro
α✝ : Type u_1
M : Matroid α✝
E✝ I B X C✝ : Set α✝
k✝ : ℕ∞
α : Type u_2
E C : Set α
k : ℕ
S : Set α
hS : S ⊆ E ∧ Disjoint S C
⊢ ↑k - (E ∩ C).encard ≠ ⊤
Tactic:
exact ((tsub_le_self).trans_lt (WithTop.coe_lt_top k)).ne
State after:
no goals