internlm/Lean-Github huggingface dataset:
Theorem: Matroid.relRank_ground_left
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
M : Matroid α
X : Set α
⊢ M.relRank M.E X = 0
Tactic:
rw [← relRank_inter_ground_right, M.relRank_eq_zero_of_subset inter_subset_right]
Proof state after:
no goals
Theorem: Matroid.relRank_eq_relRank_union
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X✝ Y✝ Z : Set α
e f : α
M : Matroid α
X Y : Set α
⊢ M.relRank X Y = M.relRank X (Y ∪ X)
Tactic:
rw [relRank, ← er_cl_eq, contract_cl_eq, ← relRank_eq_er_diff_contract, relRank_cl_right]
Proof state after:
no goals
Theorem: Matroid.Basis'.relRank_eq_encard_diff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ M.relRank C X = (I \ C).encard
Tactic:
rw [relRank_eq_relRank_union, relRank, ← er_cl_eq, contract_cl_eq, union_assoc, union_self,
  ← hI.cl_eq_cl, ← relRank_eq_er_diff_contract, relRank_cl_right,
  relRank_eq_er_diff_contract, Indep.er]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ (M ／ C).Indep (I \ C)
Theorem: Matroid.Basis'.relRank_eq_encard_diff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ (M ／ C).Indep (I \ C)
Tactic:
rw [hIC.contract_eq_contract_delete, delete_indep_iff, hIC.indep.contract_indep_iff,
  diff_union_inter, and_iff_left hI.indep, ← disjoint_union_right, union_diff_self,
  union_eq_self_of_subset_left inter_subset_right]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ Disjoint (I \ C) C
Theorem: Matroid.Basis'.relRank_eq_encard_diff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ Disjoint (I \ C) C
Tactic:
exact disjoint_sdiff_left
Proof state after:
no goals
Theorem: Matroid.Basis'.relRank_eq_encard_diff_of_subset
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I X
hCX : C ⊆ X
hIC : M.Basis' (I ∩ C) C
⊢ M.relRank C X = (I \ C).encard
Tactic:
rw [← union_eq_self_of_subset_right hCX] at hI
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hCX : C ⊆ X
hIC : M.Basis' (I ∩ C) C
⊢ M.relRank C X = (I \ C).encard
Theorem: Matroid.Basis'.relRank_eq_encard_diff_of_subset
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hCX : C ⊆ X
hIC : M.Basis' (I ∩ C) C
⊢ M.relRank C X = (I \ C).encard
Tactic:
exact hI.relRank_eq_encard_diff hIC
Proof state after:
no goals
Theorem: Matroid.Indep.relRank_of_subset
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.relRank J I = (I \ J).encard
Tactic:
rw [hI.basis_self.relRank_eq_encard_diff_of_subset hJ]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis (I ∩ J) J
Theorem: Matroid.Indep.relRank_of_subset
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis (I ∩ J) J
Tactic:
rw [inter_eq_self_of_subset_right hJ]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis J J
Theorem: Matroid.Indep.relRank_of_subset
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
hJ : J ⊆ I
⊢ M.Basis J J
Tactic:
exact (hI.subset hJ).basis_self
Proof state after:
no goals
Theorem: Matroid.Basis.relRank_eq_encard_diff_of_subset_basis
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis I X
hJ : M.Basis J Y
hIJ : I ⊆ J
⊢ M.relRank X Y = (J \ I).encard
Tactic:
rw [← relRank_cl_left, ← hI.cl_eq_cl, relRank_cl_left, ← relRank_cl_right, ← hJ.cl_eq_cl,
  relRank_cl_right, hJ.indep.relRank_of_subset hIJ]
Proof state after:
no goals
Theorem: Matroid.relRank_add_er_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X : Set α
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
Tactic:
obtain ⟨I, D, hIC, hD, -, hM⟩ := M.exists_eq_contract_indep_delete C
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X I D : Set α
hIC : M.Basis I (C ∩ M.E)
hD : D ⊆ (M ／ I).E
hM : M ／ C = M ／ I ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
Theorem: Matroid.relRank_add_er_eq
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X I D : Set α
hIC : M.Basis I (C ∩ M.E)
hD : D ⊆ (M ／ I).E
hM : M ／ C = M ／ I ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
Tactic:
obtain ⟨J, hJ, rfl⟩ := hIC.exists_basis_inter_eq_of_superset
  (subset_union_right (s := X ∩ M.E)) (by simp)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J✝ C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X D J : Set α
hJ : M.Basis J (X ∩ M.E ∪ C ∩ M.E)
hIC : M.Basis (J ∩ (C ∩ M.E)) (C ∩ M.E)
hD : D ⊆ (M ／ (J ∩ (C ∩ M.E))).E
hM : M ／ C = M ／ (J ∩ (C ∩ M.E)) ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
Theorem: Matroid.relRank_add_er_eq
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J✝ C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X D J : Set α
hJ : M.Basis J (X ∩ M.E ∪ C ∩ M.E)
hIC : M.Basis (J ∩ (C ∩ M.E)) (C ∩ M.E)
hD : D ⊆ (M ／ (J ∩ (C ∩ M.E))).E
hM : M ／ C = M ／ (J ∩ (C ∩ M.E)) ＼ D
⊢ M.relRank C X + M.er C = M.er (X ∪ C)
Tactic:
rw [← relRank_inter_ground_left, ← relRank_inter_ground_right,
  hJ.basis'.relRank_eq_encard_diff hIC.basis', ← er_inter_ground_eq,
  ← hIC.encard, encard_diff_add_encard_inter, hJ.encard, ← union_inter_distrib_right,
  er_inter_ground_eq]
Proof state after:
no goals
Theorem: Matroid.relRank_add_er_eq
Proof state before:
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D✝ X✝ Y Z : Set α
e f : α
M : Matroid α
C X I D : Set α
hIC : M.Basis I (C ∩ M.E)
hD : D ⊆ (M ／ I).E
hM : M ／ C = M ／ I ＼ D
⊢ X ∩ M.E ∪ C ∩ M.E ⊆ M.E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.relRank_add_er_of_subset
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
⊢ M.relRank X Y + M.er X = M.er Y
Tactic:
rw [relRank_add_er_eq, union_eq_self_of_subset_right hXY]
Proof state after:
no goals
Theorem: Matroid.rFin.relRank_eq_sub
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y = M.er Y - M.er X
Tactic:
rw [← relRank_add_er_of_subset _ hXY]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y = M.relRank X Y + M.er X - M.er X
Theorem: Matroid.rFin.relRank_eq_sub
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y = M.relRank X Y + M.er X - M.er X
Tactic:
apply WithTop.add_right_cancel <| ne_top_of_lt hY
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y + M.er X = M.relRank X Y + M.er X - M.er X + M.er X
Theorem: Matroid.rFin.relRank_eq_sub
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.relRank X Y + M.er X = M.relRank X Y + M.er X - M.er X + M.er X
Tactic:
rw [eq_comm, tsub_add_cancel_iff_le]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.er X ≤ M.relRank X Y + M.er X
Theorem: Matroid.rFin.relRank_eq_sub
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : M.rFin X
hXY : X ⊆ Y
⊢ M.er X ≤ M.relRank X Y + M.er X
Tactic:
exact le_add_self
Proof state after:
no goals
Theorem: Matroid.Nonloop.relRank_add_one_eq
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X + 1 = M.er (insert e X)
Tactic:
rw [← union_singleton, ← relRank_add_er_eq, he.er_eq]
Proof state after:
no goals
Theorem: Matroid.Nonloop.relRank_eq_sub_one
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X = M.er (insert e X) - 1
Tactic:
apply WithTop.add_right_cancel (show (1 : ℕ∞) ≠ ⊤ from ENat.coe_toNat_eq_self.mp rfl)
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X + 1 = M.er (insert e X) - 1 + 1
Theorem: Matroid.Nonloop.relRank_eq_sub_one
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ M.relRank {e} X + 1 = M.er (insert e X) - 1 + 1
Tactic:
rw [← he.relRank_add_one_eq, eq_comm, tsub_add_cancel_iff_le]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ 1 ≤ M.relRank {e} X + 1
Theorem: Matroid.Nonloop.relRank_eq_sub_one
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X✝ Y Z : Set α
e f : α
he : M.Nonloop e
X : Set α
⊢ 1 ≤ M.relRank {e} X + 1
Tactic:
exact le_add_self
Proof state after:
no goals
Theorem: Matroid.relRank_add_of_subset_of_subset
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
Proof state after:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Theorem: Matroid.relRank_add_of_subset_of_subset
Proof state before:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans hXY)
Proof state after:
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J✝ C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Theorem: Matroid.relRank_add_of_subset_of_subset
Proof state before:
case intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J✝ C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain ⟨K, hK, hJK⟩ := hJ.indep.subset_basis'_of_subset (hJ.subset.trans hYZ)
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J✝ C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
K : Set α
hK : M.Basis' K Z
hJK : J ⊆ K
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Theorem: Matroid.relRank_add_of_subset_of_subset
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I✝ J✝ C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J Y
hIJ : I ⊆ J
K : Set α
hK : M.Basis' K Z
hJK : J ⊆ K
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain rfl := hI.inter_eq_of_subset_indep hIJ hJ.indep
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J✝ C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
J : Set α
hJ : M.Basis' J Y
K : Set α
hK : M.Basis' K Z
hJK : J ⊆ K
hI : M.Basis' (J ∩ X) X
hIJ : J ∩ X ⊆ J
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Theorem: Matroid.relRank_add_of_subset_of_subset
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J✝ C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
J : Set α
hJ : M.Basis' J Y
K : Set α
hK : M.Basis' K Z
hJK : J ⊆ K
hI : M.Basis' (J ∩ X) X
hIJ : J ∩ X ⊆ J
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
obtain rfl := hJ.inter_eq_of_subset_indep hJK hK.indep
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Theorem: Matroid.relRank_add_of_subset_of_subset
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ M.relRank X Y + M.relRank Y Z = M.relRank X Z
Tactic:
rw [hJ.relRank_eq_encard_diff_of_subset hXY hI, hK.relRank_eq_encard_diff_of_subset hYZ hJ,
  hK.relRank_eq_encard_diff_of_subset (hXY.trans hYZ)
  (by rwa [inter_assoc, inter_eq_self_of_subset_right hXY] at hI),
  ← encard_union_eq, diff_eq, diff_eq, inter_assoc, ← inter_union_distrib_left,
  inter_union_distrib_right, union_compl_self, univ_inter, ← compl_inter,
  inter_eq_self_of_subset_left hXY, diff_eq]
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ Disjoint ((K ∩ Y) \ X) (K \ Y)
Theorem: Matroid.relRank_add_of_subset_of_subset
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ Disjoint ((K ∩ Y) \ X) (K \ Y)
Tactic:
exact disjoint_of_subset_left (diff_subset.trans inter_subset_right)
  disjoint_sdiff_right
Proof state after:
no goals
Theorem: Matroid.relRank_add_of_subset_of_subset
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C D X Y Z : Set α
e f : α
M : Matroid α
hXY : X ⊆ Y
hYZ : Y ⊆ Z
K : Set α
hK : M.Basis' K Z
hJ : M.Basis' (K ∩ Y) Y
hJK : K ∩ Y ⊆ K
hI : M.Basis' (K ∩ Y ∩ X) X
hIJ : K ∩ Y ∩ X ⊆ K ∩ Y
⊢ M.Basis' (K ∩ X) X
Tactic:
rwa [inter_assoc, inter_eq_self_of_subset_right hXY] at hI
Proof state after:
no goals
Theorem: Matroid.relRank_eq_zero_iff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.relRank X Y = 0 ↔ Y ⊆ M.cl X
Tactic:
rw [← relRank_cl_left, relRank, er_eq_zero_iff', contract_loops_eq, cl_cl, diff_self,
  subset_empty_iff, contract_ground, ← inter_diff_assoc, inter_eq_self_of_subset_left hY,
  diff_eq_empty]
Proof state after:
no goals
Theorem: Matroid.relRank_eq_zero_iff'
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
⊢ M.relRank X Y = 0 ↔ Y ∩ M.E ⊆ M.cl X
Tactic:
rw [← relRank_inter_ground_right, ← relRank_inter_ground_left, relRank_eq_zero_iff,
  cl_inter_ground]
Proof state after:
no goals
Theorem: Matroid.relRank_eq_one_iff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.relRank X Y = 1 ↔ ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
Tactic:
rw [← relRank_cl_left, relRank_eq_er_diff_contract, er_eq_one_iff
  (show Y \ (M.cl X) ⊆ (M ／ (M.cl X)).E from diff_subset_diff_left hY)]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, (M ／ M.cl X).Nonloop e ∧ Y \ M.cl X ⊆ (M ／ M.cl X).cl {e}) ↔
    ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
Theorem: Matroid.relRank_eq_one_iff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, (M ／ M.cl X).Nonloop e ∧ Y \ M.cl X ⊆ (M ／ M.cl X).cl {e}) ↔
    ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
Tactic:
simp only [contract_cl_eq, singleton_union, diff_subset_iff, diff_union_self,
  cl_insert_cl_eq_cl_insert, union_diff_self, contract_nonloop_iff, cl_cl,
  union_eq_self_of_subset_left (M.cl_subset_cl (subset_insert _ X))]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, e ∈ M.E \ M.cl X ∧ Y ⊆ M.cl (insert e X)) ↔ ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
Theorem: Matroid.relRank_eq_one_iff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, e ∈ M.E \ M.cl X ∧ Y ⊆ M.cl (insert e X)) ↔ ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
Tactic:
exact ⟨fun ⟨e,he,_,hY'⟩ ↦ ⟨e,he,hY'⟩, fun ⟨e, he, hY'⟩ ↦ ⟨e, he, ⟨hY he.1, he.2⟩, hY'⟩⟩
Proof state after:
no goals
Theorem: Matroid.relRank_le_one_iff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.relRank X Y ≤ 1 ↔ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
rw [le_iff_eq_or_lt, lt_iff_not_le, ENat.one_le_iff_ne_zero, not_not, relRank_eq_one_iff,
  relRank_eq_zero_iff]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X ↔ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Theorem: Matroid.relRank_le_one_iff
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X ↔ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
refine ⟨?_, fun ⟨e, hY'⟩ ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X → ∃ e ∈ Y, Y ⊆ M.cl (insert e X)

case refine_2
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Theorem: Matroid.relRank_le_one_iff
Proof state before:
case refine_2
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Tactic:
by_cases he : e ∈ M.cl X
Proof state after:
case pos
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
he : e ∈ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X

case neg
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
he : e ∉ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Theorem: Matroid.relRank_le_one_iff
Proof state before:
case neg
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
he : e ∉ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Tactic:
exact Or.inl ⟨_, ⟨hY'.1, he⟩, hY'.2⟩
Proof state after:
no goals
Theorem: Matroid.relRank_le_one_iff
Proof state before:
case refine_1
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X → ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
rintro (⟨e, he, hY'⟩ | hY')
Proof state after:
case refine_1.inl.intro.intro
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
e : α
he : e ∈ Y \ M.cl X
hY' : Y ⊆ M.cl (insert e X)
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)

case refine_1.inr
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
hY' : Y ⊆ M.cl X
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Theorem: Matroid.relRank_le_one_iff
Proof state before:
case refine_1.inr
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
hY' : Y ⊆ M.cl X
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
exact ⟨_, hYne.some_mem, hY'.trans (M.cl_subset_cl (subset_insert _ _))⟩
Proof state after:
no goals
Theorem: Matroid.relRank_le_one_iff
Proof state before:
case refine_1.inl.intro.intro
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
e : α
he : e ∈ Y \ M.cl X
hY' : Y ⊆ M.cl (insert e X)
⊢ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
Tactic:
exact ⟨e, he.1, hY'⟩
Proof state after:
no goals
Theorem: Matroid.relRank_le_one_iff
Proof state before:
case pos
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl (insert e X)
he : e ∈ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Tactic:
rw [← cl_insert_cl_eq_cl_insert, insert_eq_of_mem he, cl_cl] at hY'
Proof state after:
case pos
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl X
he : e ∈ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Theorem: Matroid.relRank_le_one_iff
Proof state before:
case pos
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e✝ f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
x✝ : ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
e : α
hY' : e ∈ Y ∧ Y ⊆ M.cl X
he : e ∈ M.cl X
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X
Tactic:
exact Or.inr hY'.2
Proof state after:
no goals
Theorem: Matroid.er_contract_le_er
Proof state before:
α : Type u_1
M✝ N : Matroid α
I J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X : Set α
⊢ (M ／ C).er X ≤ M.er X
Tactic:
obtain ⟨I, hI⟩ := (M ／ C).exists_basis (X ∩ (M ／ C).E)
Proof state after:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ (M ／ C).er X ≤ M.er X
Theorem: Matroid.er_contract_le_er
Proof state before:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ (M ／ C).er X ≤ M.er X
Tactic:
rw [← er_inter_ground_eq, ← hI.encard, ← hI.indep.of_contract.er]
Proof state after:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ M.er I ≤ M.er X
Theorem: Matroid.er_contract_le_er
Proof state before:
case intro
α : Type u_1
M✝ N : Matroid α
I✝ J C✝ D X✝ Y Z : Set α
e f : α
M : Matroid α
C X I : Set α
hI : (M ／ C).Basis I (X ∩ (M ／ C).E)
⊢ M.er I ≤ M.er X
Tactic:
exact M.er_mono (hI.subset.trans inter_subset_left)
Proof state after:
no goals
Theorem: Matroid.rFin.contract_rFin
Proof state before:
α : Type u_1
M N : Matroid α
I J C✝ D X Y Z : Set α
e f : α
h : M.rFin X
C : Set α
⊢ (M ／ C).rFin X
Tactic:
rw [← er_lt_top_iff] at *
Proof state after:
α : Type u_1
M N : Matroid α
I J C✝ D X Y Z : Set α
e f : α
h : M.er X < ⊤
C : Set α
⊢ (M ／ C).er X < ⊤
Theorem: Matroid.rFin.contract_rFin
Proof state before:
α : Type u_1
M N : Matroid α
I J C✝ D X Y Z : Set α
e f : α
h : M.er X < ⊤
C : Set α
⊢ (M ／ C).er X < ⊤
Tactic:
exact (er_contract_le_er _ _ _).trans_lt h
Proof state after:
no goals
Theorem: Matroid.rFin.union_of_contract
Proof state before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).rFin X
hC : M.rFin C
⊢ M.rFin (X ∪ C)
Tactic:
rw [← er_lt_top_iff, ← M.relRank_add_er_eq, relRank]
Proof state after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).rFin X
hC : M.rFin C
⊢ (M ／ C).er X + M.er C < ⊤