internlm/Lean-Github huggingface dataset:
Theorem: Matroid.unifOn_dual_eq
Proof state before:
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B
Tactic:
rw [dual_base_iff', unifOn_base_iff' ((tsub_le_self.trans_lt hE.encard_lt_top).ne) (by simp) hBE,
  unifOn_ground_eq, and_iff_left hBE, unifOn_base_iff hlt.le diff_subset,
  ← WithTop.add_right_cancel_iff (hE.subset hBE).encard_lt_top.ne,
  encard_diff_add_encard_of_subset hBE, Iff.comm, eq_comm, add_comm,
  ← WithTop.add_right_cancel_iff (hlt.trans_le le_top).ne, tsub_add_cancel_of_le hlt.le]
Proof state after:
no goals
Theorem: Matroid.unifOn_dual_eq
Proof state before:
case inr.intro.inl
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hle : E.encard ≤ ↑k
⊢ (unifOn E ↑k)✶ = unifOn E (E.encard - ↑k)
Tactic:
rw [unifOn_eq_of_le hle, freeOn_dual_eq, tsub_eq_zero_of_le hle, unifOn_zero]
Proof state after:
no goals
Theorem: Matroid.unifOn_dual_eq
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
⊢ (unifOn E ↑k)✶.E = (unifOn E (E.encard - ↑k)).E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.unifOn_dual_eq
Proof state before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ E
⊢ E.encard - ↑k ≤ E.encard
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.unifOn_spanning_iff'
Proof 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
Proof 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
Theorem: Matroid.unifOn_spanning_iff'
Proof 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]
Proof 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
Theorem: Matroid.unifOn_spanning_iff'
Proof 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⟩ ) _⟩
Proof 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
Theorem: Matroid.unifOn_spanning_iff'
Proof 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
Proof 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
Theorem: Matroid.unifOn_spanning_iff'
Proof 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]
Proof 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
Theorem: Matroid.unifOn_spanning_iff'
Proof 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⟩
Proof state after:
no goals
Theorem: Matroid.unifOn_spanning_iff'
Proof 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]
Proof state after:
no goals
Theorem: Matroid.unifOn_spanning_iff'
Proof 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⟩)
Proof 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
Theorem: Matroid.unifOn_spanning_iff'
Proof 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]
Proof 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 ≤ ⊤
Theorem: Matroid.unifOn_spanning_iff'
Proof 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
Proof state after:
no goals
Theorem: Matroid.unifOn_spanning_iff'
Proof 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]
Proof state after:
no goals
Theorem: Matroid.unifOn_spanning_iff'
Proof 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)
Proof state after:
no goals
Theorem: Matroid.unifOn_spanning_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ (unifOn E ↑k).Spanning X ↔ ↑k ≤ X.encard
Tactic:
rw [← ENat.some_eq_coe, unifOn_spanning_iff' (WithTop.coe_lt_top k).ne, and_iff_left hX,
  or_iff_left_iff_imp]
Proof state after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ X = E → ↑k ≤ X.encard
Theorem: Matroid.unifOn_spanning_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ X = E → ↑k ≤ X.encard
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ X.encard
hX : X ⊆ X
⊢ ↑k ≤ X.encard
Theorem: Matroid.unifOn_spanning_iff
Proof state before:
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ X.encard
hX : X ⊆ X
⊢ ↑k ≤ X.encard
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.eq_unifOn_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E k → M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
Tactic:
rintro rfl
Proof state after:
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E k).E = E ∧ ∀ (I : Set α), (unifOn E k).Indep I ↔ I.encard ≤ k ∧ I ⊆ E
Theorem: Matroid.eq_unifOn_iff
Proof state before:
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E k).E = E ∧ ∀ (I : Set α), (unifOn E k).Indep I ↔ I.encard ≤ k ∧ I ⊆ E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.eq_unifOn_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
x✝ : M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
hE : M.E = E
h : ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
⊢ M.E = (unifOn E k).E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.eq_unifOn_iff
Proof state before:
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
x✝¹ : M.E = E ∧ ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
hE : M.E = E
h : ∀ (I : Set α), M.Indep I ↔ I.encard ≤ k ∧ I ⊆ E
I : Set α
x✝ : I ⊆ M.E
⊢ M.Indep I ↔ (unifOn E k).Indep I
Tactic:
simpa using h I
Proof state after:
no goals
Theorem: Matroid.unifOn_delete_eq
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B X C : Set α
k✝ : ℕ∞
E D : Set α
k : ℕ∞
⊢ unifOn E k ＼ D = unifOn (E \ D) k
Tactic:
simp_rw [eq_unifOn_iff, delete_ground, unifOn_ground_eq, true_and, delete_indep_iff,
  unifOn_indep_iff, subset_diff, and_assoc, imp_true_iff]
Proof state after:
no goals
Theorem: Matroid.unifOn_contract_eq'
Proof 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
Proof 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)
Theorem: Matroid.unifOn_contract_eq'
Proof 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 ↦ _)
Proof 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
Theorem: Matroid.unifOn_contract_eq'
Proof 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
Proof 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
Theorem: Matroid.unifOn_contract_eq'
Proof 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]
Proof 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 ≠ ⊤
Theorem: Matroid.unifOn_contract_eq'
Proof 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
Proof state after:
no goals
Theorem: Matroid.unifOn_contract_eq'
Proof 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
Proof state after:
no goals
Theorem: Matroid.unifOn_contract_eq'
Proof 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
Proof state after:
no goals
Theorem: Matroid.eq_unifOn_two_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E 2 ↔ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E 2 → M.E = E ∧ M.erk ≤ 2 ∧ M.Simple

case mpr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple → M = unifOn E 2
Theorem: Matroid.eq_unifOn_two_iff
Proof state before:
case mpr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M.E = E ∧ M.erk ≤ 2 ∧ M.Simple → M = unifOn E 2
Tactic:
rintro ⟨rfl, hr, hM⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ M = unifOn M.E 2
Theorem: Matroid.eq_unifOn_two_iff
Proof state before:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ M = unifOn M.E 2
Tactic:
simp only [eq_iff_indep_iff_indep_forall, unifOn_ground_eq, unifOn_indep_iff, true_and]
Proof state after:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ ∀ I ⊆ M.E, M.Indep I ↔ I.encard ≤ 2 ∧ I ⊆ M.E
Theorem: Matroid.eq_unifOn_two_iff
Proof state before:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I B X C : Set α
k : ℕ∞
hr : M.erk ≤ 2
hM : M.Simple
⊢ ∀ I ⊆ M.E, M.Indep I ↔ I.encard ≤ 2 ∧ I ⊆ M.E
Tactic:
exact fun I hIE ↦ ⟨fun hI ↦ ⟨hI.encard_le_erk.trans hr, hIE⟩,
  fun ⟨hcard, _⟩ ↦ indep_of_encard_le_two hcard⟩
Proof state after:
no goals
Theorem: Matroid.eq_unifOn_two_iff
Proof state before:
case mp
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ M = unifOn E 2 → M.E = E ∧ M.erk ≤ 2 ∧ M.Simple
Tactic:
rintro rfl
Proof state after:
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E 2).E = E ∧ (unifOn E 2).erk ≤ 2 ∧ (unifOn E 2).Simple
Theorem: Matroid.eq_unifOn_two_iff
Proof state before:
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E 2).E = E ∧ (unifOn E 2).erk ≤ 2 ∧ (unifOn E 2).Simple
Tactic:
simp_rw [unifOn_ground_eq, unifOn_erk_eq, min_le_iff, iff_true_intro rfl.le,
  or_true, true_and, simple_iff_forall_pair_indep, unifOn_ground_eq, unifOn_indep_iff,
  and_iff_right (encard_pair_le _ _)]
Proof state after:
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ ∀ ⦃e f : α⦄, e ∈ E → f ∈ E → {e, f} ⊆ E
Theorem: Matroid.eq_unifOn_two_iff
Proof state before:
case mp
α : Type u_1
E I B X C : Set α
k : ℕ∞
⊢ ∀ ⦃e f : α⦄, e ∈ E → f ∈ E → {e, f} ⊆ E
Tactic:
exact fun e f ↦ pair_subset
Proof state after:
no goals
Theorem: Matroid.unif_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
E I✝ B X C : Set α
k : ℕ∞
a b a' b' : ℕ
I : Set (Fin b)
⊢ (unif a b).Indep I ↔ I.encard ≤ ↑a
Tactic:
rw [unif, unifOn_indep_iff, and_iff_left (subset_univ _)]
Proof state after:
no goals
Theorem: Matroid.unif_er_eq
Proof state before:
α : Type u_1
M : Matroid α
E I B X✝ C : Set α
k : ℕ∞
a b a' b' : ℕ
X : Set (Fin b)
⊢ (unif a b).er X = min X.encard ↑a
Tactic:
rw [unif, unifOn_er_eq _ _ (subset_univ _)]
Proof state after:
no goals
Theorem: Matroid.unif_erk_eq
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ (unif a b).erk = ↑(min a b)
Tactic:
rw [erk_eq_er_ground, unif_er_eq]
Proof state after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min (unif a b).E.encard ↑a = ↑(min a b)
Theorem: Matroid.unif_erk_eq
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min (unif a b).E.encard ↑a = ↑(min a b)
Tactic:
simp only [unif_ground_eq, ge_iff_le, min_comm, encard_univ_fin]
Proof state after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min ↑a ↑b = ↑(min a b)
Theorem: Matroid.unif_erk_eq
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ min ↑a ↑b = ↑(min a b)
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.unif_rk_eq
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ (unif a b).rk = min a b
Tactic:
rw [rk, unif_erk_eq, ENat.toNat_coe]
Proof state after:
no goals
Theorem: Matroid.unif_erk_eq_of_le
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
⊢ (unif a b).erk = ↑a
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.unif_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
B : Set (Fin b)
⊢ (unif a b).Base B ↔ B.encard = ↑a
Tactic:
rw [unif, unifOn, truncateTo_base_iff, freeOn_indep_iff, and_iff_right (subset_univ _)]
Proof state after:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
B : Set (Fin b)
⊢ ↑a ≤ (freeOn univ).erk
Theorem: Matroid.unif_base_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
hab : a ≤ b
B : Set (Fin b)
⊢ ↑a ≤ (freeOn univ).erk
Tactic:
rwa [freeOn_erk_eq, encard_univ, PartENat.card_eq_coe_fintype_card, Fintype.card_fin,
  PartENat.withTopEquiv_natCast, Nat.cast_le]
Proof state after:
no goals
Theorem: Matroid.unif_base_iff'
Proof state before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
⊢ (unif a (a + b)).Base B ↔ B.encard = ↑a
Tactic:
rw [unif_base_iff (Nat.le_add_right _ _)]
Proof state after:
no goals
Theorem: Matroid.unif_dual'
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' n : ℕ
h : a + b = n
⊢ (unif a n)✶ = unif b n
Tactic:
subst h
Proof state after:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (unif a (a + b))✶ = unif b (a + b)
Theorem: Matroid.unif_dual'
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (unif a (a + b))✶ = unif b (a + b)
Tactic:
refine eq_of_base_iff_base_forall rfl (fun B _ ↦ ?_)
Proof state after:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ (unif a (a + b))✶.Base B ↔ (unif b (a + b)).Base B
Theorem: Matroid.unif_dual'
Proof state before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ (unif a (a + b))✶.Base B ↔ (unif b (a + b)).Base B
Tactic:
rw [dual_base_iff, unif_ground_eq, unif_base_iff (Nat.le_add_right _ _),
  unif_base_iff (Nat.le_add_left _ _),
  ← WithTop.add_right_cancel_iff (encard_ne_top_iff.2 B.toFinite),
  encard_diff_add_encard_of_subset (subset_univ _), Iff.comm,
  ← WithTop.add_left_cancel_iff (WithTop.coe_ne_top (a := a)), eq_comm]
Proof state after:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ ↑a + ↑b = ↑a + B.encard ↔ univ.encard = ↑a + B.encard
Theorem: Matroid.unif_dual'
Proof state before:
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ ↑a + ↑b = ↑a + B.encard ↔ univ.encard = ↑a + B.encard
Tactic:
convert Iff.rfl
Proof state after:
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ univ.encard = ↑a + ↑b
Theorem: Matroid.unif_dual'
Proof state before:
case h.e'_2.h.e'_2
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ univ.encard = ↑a + ↑b
Tactic:
rw [encard_univ, PartENat.card_eq_coe_fintype_card, Fintype.card_fin,
  PartENat.withTopEquiv_natCast, ENat.some_eq_coe, eq_comm, Nat.cast_add]
Proof state after:
no goals
Theorem: Matroid.unif_zero
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b✝ a' b' b : ℕ
⊢ unif 0 b = loopyOn univ
Tactic:
simp [eq_loopyOn_iff]
Proof state after:
no goals
Theorem: Matroid.unif_eq_freeOn
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
h : b ≤ a
⊢ unif a b = freeOn univ
Tactic:
simpa [eq_freeOn_iff]
Proof state after:
no goals
Theorem: Matroid.unif_dual
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ (unif a b)✶ = unif (b - a) b
Tactic:
obtain (hab | hba) := le_or_lt a b
Proof state after:
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
hab : a ≤ b
⊢ (unif a b)✶ = unif (b - a) b

case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
hba : b < a
⊢ (unif a b)✶ = unif (b - a) b
Theorem: Matroid.unif_dual
Proof state before:
case inr
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
hba : b < a
⊢ (unif a b)✶ = unif (b - a) b
Tactic:
simp [unif_eq_freeOn hba.le, Nat.sub_eq_zero_of_le hba.le]
Proof state after:
no goals
Theorem: Matroid.unif_dual
Proof state before:
case inl
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
hab : a ≤ b
⊢ (unif a b)✶ = unif (b - a) b
Tactic:
exact unif_dual' (Nat.add_sub_of_le hab)
Proof state after:
no goals
Theorem: Matroid.unif_sub_dual
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a✝ b✝ a' b' a b : ℕ
⊢ (unif (b - a) b)✶ = unif a b
Tactic:
rw [eq_comm, eq_dual_comm, unif_dual]
Proof state after:
no goals
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ Nonempty (M ≂ unif a b) ↔ ∃ E, M = unifOn E ↑a ∧ E.encard = ↑b
Tactic:
refine ⟨fun ⟨e⟩ ↦ ⟨M.E, ?_⟩, ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
x✝ : Nonempty (M ≂ unif a b)
e : M ≂ unif a b
⊢ M = unifOn M.E ↑a ∧ M.E.encard = ↑b

case refine_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) → Nonempty (M ≂ unif a b)
Theorem: Matroid.nonempty_iso_unif_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
⊢ (∃ E, M = unifOn E ↑a ∧ E.encard = ↑b) → Nonempty (M ≂ unif a b)
Tactic:
rintro ⟨E, rfl, hE⟩
Proof state after:
case refine_2.intro.intro
α : Type u_1
E✝ I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
E : Set α
hE : E.encard = ↑b
⊢ Nonempty (unifOn E ↑a ≂ unif a b)