internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ {e} ⊆ M.E
Tactic:
rw [← he]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C ∩ K ⊆ M.E
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C ∩ K ⊆ M.E
Tactic:
exact inter_subset_left.trans hC.subset_ground
Proof state after:
no goals
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e}) ⊆ M.cl (M.E \ K)
Tactic:
refine (M.cl_subset_cl (subset_union_left (t := C))).trans ?_
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e} ∪ C) ⊆ M.cl (M.E \ K)
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.cl (M.E \ K ∪ {e} ∪ C) ⊆ M.cl (M.E \ K)
Tactic:
rw [union_assoc, singleton_union, insert_eq_of_mem heC, ← cl_union_cl_right_eq,
  ← hC.cl_diff_singleton_eq_cl e, cl_union_cl_right_eq, union_eq_self_of_subset_right]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ {e} ⊆ M.E \ K
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ {e} ⊆ M.E \ K
Tactic:
rw [← he, diff_self_inter]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ K ⊆ M.E \ K
Theorem: Matroid.Circuit.cocircuit_disjoint_or_nontrivial_inter
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
B : Set α
hC : M.Circuit C
e : α
heC : e ∈ C
heK : e ∈ K
he : C ∩ K = {e}
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃y : Set α⦄, y ⊂ K → M.Spanning (M.E \ y)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ C \ K ⊆ M.E \ K
Tactic:
exact diff_subset_diff_left hC.subset_ground
Proof state after:
no goals
Theorem: Matroid.Circuit.cocircuit_inter_nontrivial
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
hK : M.Cocircuit K
hCK : (C ∩ K).Nonempty
⊢ (C ∩ K).Nontrivial
Tactic:
simpa [or_iff_not_imp_left, not_disjoint_iff_nonempty_inter, imp_iff_right hCK] using
  hC.cocircuit_disjoint_or_nontrivial_inter hK
Proof state after:
no goals
Theorem: Matroid.dual_rkPos_iff_exists_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M✶.RkPos ↔ ∃ C, M.Circuit C
Tactic:
rw [rkPos_iff_empty_not_base, dual_base_iff, diff_empty, not_iff_comm, not_exists,
  ← ground_indep_iff_base, indep_iff_forall_subset_not_circuit]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ (∀ (x : Set α), ¬M.Circuit x) ↔ ∀ C ⊆ M.E, ¬M.Circuit C
Theorem: Matroid.dual_rkPos_iff_exists_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ (∀ (x : Set α), ¬M.Circuit x) ↔ ∀ C ⊆ M.E, ¬M.Circuit C
Tactic:
exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩
Proof state after:
no goals
Theorem: Matroid.exists_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
inst✝ : M✶.RkPos
⊢ M✶.RkPos
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.rk_Pos_iff_exists_cocircuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M.RkPos ↔ ∃ K, M.Cocircuit K
Tactic:
rw [← dual_dual M, dual_rkPos_iff_exists_circuit, dual_dual M]
Proof state after:
no goals
Theorem: Matroid.fundCocct_cocircuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ M.Cocircuit (fundCocct e B)
Tactic:
apply hB.compl_base_dual.indep.fundCct_circuit
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B) \ (M.E \ B)
Theorem: Matroid.fundCocct_cocircuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B) \ (M.E \ B)
Tactic:
simp only [mem_diff, he, not_true_eq_false, and_false, not_false_eq_true, and_true]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B)
Theorem: Matroid.fundCocct_cocircuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M✶.cl (M.E \ B)
Tactic:
rw [hB.compl_base_dual.cl_eq, dual_ground]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M.E
Theorem: Matroid.fundCocct_cocircuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
he : e ∈ B
hB : M.Base B
⊢ e ∈ M.E
Tactic:
exact hB.subset_ground he
Proof state after:
no goals
Theorem: Matroid.fundCocct_inter_eq
Proof state before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ fundCocct e B ∩ B = {e}
Tactic:
refine subset_antisymm ?_ (singleton_subset_iff.2 ⟨M.mem_fundCocct _ _, he⟩)
Proof state after:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ fundCocct e B ∩ B ⊆ {e}
Theorem: Matroid.fundCocct_inter_eq
Proof state before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ fundCocct e B ∩ B ⊆ {e}
Tactic:
refine (inter_subset_inter_left _ (M.fundCocct_subset_insert_compl _ _)).trans ?_
Proof state after:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ insert e (M.E \ B) ∩ B ⊆ {e}
Theorem: Matroid.fundCocct_inter_eq
Proof state before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
M : Matroid α
B : Set α
he : e ∈ B
⊢ insert e (M.E \ B) ∩ B ⊆ {e}
Tactic:
simp (config := {contextual := true})
Proof state after:
no goals
Theorem: Matroid.Indep.exists_cocircuit_inter_eq_mem
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ∃ K, M.Cocircuit K ∧ K ∩ I = {e}
Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_base_superset
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∃ K, M.Cocircuit K ∧ K ∩ I = {e}
Theorem: Matroid.Indep.exists_cocircuit_inter_eq_mem
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ ∃ K, M.Cocircuit K ∧ K ∩ I = {e}
Tactic:
refine ⟨M.fundCocct e B, fundCocct_cocircuit (hIB heI) hB, ?_⟩
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I = {e}
Theorem: Matroid.Indep.exists_cocircuit_inter_eq_mem
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I = {e}
Tactic:
rw [subset_antisymm_iff, subset_inter_iff, singleton_subset_iff, and_iff_right
  (mem_fundCocct _ _ _), singleton_subset_iff, and_iff_left heI, ← M.fundCocct_inter_eq (hIB heI)]
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I ⊆ fundCocct e B ∩ B
Theorem: Matroid.Indep.exists_cocircuit_inter_eq_mem
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B✝ : Set α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ fundCocct e B ∩ I ⊆ fundCocct e B ∩ B
Tactic:
exact inter_subset_inter_right _ hIB
Proof state after:
no goals
Theorem: Matroid.Circuit.finite
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
⊢ C.Finite
Tactic:
have hi := hC.dep.not_indep
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ¬M.Indep C
⊢ C.Finite
Theorem: Matroid.Circuit.finite
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ¬M.Indep C
⊢ C.Finite
Tactic:
rw [indep_iff_forall_finite_subset_indep] at hi
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite
Theorem: Matroid.Circuit.finite
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite
Tactic:
push_neg at hi
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
⊢ C.Finite
Theorem: Matroid.Circuit.finite
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
⊢ C.Finite
Tactic:
obtain ⟨J, hJC, hJfin, hJ⟩ := hi
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite
Theorem: Matroid.Circuit.finite
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite
Tactic:
rwa [← hC.eq_of_not_indep_subset hJ hJC]
Proof state after:
no goals
Theorem: Matroid.finitary_iff_forall_circuit_finite
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Finitary ↔ ∀ (C : Set α), M.Circuit C → C.Finite
Tactic:
refine ⟨fun _ _ ↦ Circuit.finite, fun h ↦
  ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩ ⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False

case refine_2
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x✝ y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E
Theorem: Matroid.finitary_iff_forall_circuit_finite
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x✝ y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E
Tactic:
simpa using (hI {x} (by simpa) (finite_singleton _)).subset_ground
Proof state after:
no goals
Theorem: Matroid.finitary_iff_forall_circuit_finite
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False
Tactic:
obtain ⟨C, hCI, hC⟩ := hd.exists_circuit_subset
Proof state after:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
C : Set α
hCI : C ⊆ I
hC : M.Circuit C
⊢ False
Theorem: Matroid.finitary_iff_forall_circuit_finite
Proof state before:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
C : Set α
hCI : C ⊆ I
hC : M.Circuit C
⊢ False
Tactic:
exact hC.dep.not_indep <| hI _ hCI (h C hC)
Proof state after:
no goals
Theorem: Matroid.finitary_iff_forall_circuit_finite
Proof state before:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x✝ y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ {x} ⊆ I
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.one_le_girth
Proof state before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ 1 ≤ M.girth
Tactic:
simp_rw [girth, le_iInf_iff, one_le_encard_iff_nonempty]
Proof state after:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ ∀ i ∈ {C | M.Circuit C}, i.Nonempty
Theorem: Matroid.one_le_girth
Proof state before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ ∀ i ∈ {C | M.Circuit C}, i.Nonempty
Tactic:
exact fun _ ↦ Circuit.nonempty
Proof state after:
no goals
Theorem: Matroid.Circuit.girth_le_card
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hC : M.Circuit C
⊢ M.girth ≤ C.encard
Tactic:
simp only [girth, mem_setOf_eq, iInf_le_iff, le_iInf_iff]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hC : M.Circuit C
⊢ ∀ (b : ℕ∞), (∀ (i : Set α), M.Circuit i → b ≤ i.encard) → b ≤ C.encard
Theorem: Matroid.Circuit.girth_le_card
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hC : M.Circuit C
⊢ ∀ (b : ℕ∞), (∀ (i : Set α), M.Circuit i → b ≤ i.encard) → b ≤ C.encard
Tactic:
exact fun b hb ↦ hb C hC
Proof state after:
no goals
Theorem: Matroid.girth_eq_top_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
⊢ M.girth = ⊤ ↔ ∀ (C : Set α), M.Circuit C → C.Infinite
Tactic:
simp [girth, sInf_eq_top]
Proof state after:
no goals
Theorem: Matroid.le_girth_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
⊢ k ≤ M.girth ↔ ∀ (C : Set α), M.Circuit C → k ≤ C.encard
Tactic:
simp [girth, le_sInf_iff]
Proof state after:
no goals
Theorem: Matroid.exists_circuit_girth
Proof state before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
inst✝ : M✶.RkPos
⊢ ∃ C, M.Circuit C ∧ C.encard = M.girth
Tactic:
obtain ⟨⟨C,hC⟩, (hC' : C.encard = _)⟩ :=
  @ciInf_mem ℕ∞ (setOf M.Circuit) _ _ (nonempty_coe_sort.mpr M.exists_circuit)
    (fun C ↦ (C : Set α).encard)
Proof state after:
case intro.mk
α : Type u_1
M✝ : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
inst✝ : M✶.RkPos
C : Set α
hC : C ∈ setOf M.Circuit
hC' : C.encard = ⨅ C, (↑C).encard
⊢ ∃ C, M.Circuit C ∧ C.encard = M.girth
Theorem: Matroid.exists_circuit_girth
Proof state before:
case intro.mk
α : Type u_1
M✝ : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
inst✝ : M✶.RkPos
C : Set α
hC : C ∈ setOf M.Circuit
hC' : C.encard = ⨅ C, (↑C).encard
⊢ ∃ C, M.Circuit C ∧ C.encard = M.girth
Tactic:
exact ⟨C, hC, by rw [hC', girth, iInf_subtype']⟩
Proof state after:
no goals
Theorem: Matroid.exists_circuit_girth
Proof state before:
α : Type u_1
M✝ : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
inst✝ : M✶.RkPos
C : Set α
hC : C ∈ setOf M.Circuit
hC' : C.encard = ⨅ C, (↑C).encard
⊢ C.encard = M.girth
Tactic:
rw [hC', girth, iInf_subtype']
Proof state after:
no goals
Theorem: Matroid.girth_lt_iff
Proof state before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
⊢ M.girth < k ↔ ∃ C, M.Circuit C ∧ C.encard < k
Tactic:
simp_rw [girth, iInf_lt_iff, mem_setOf_eq, bex_def]
Proof state after:
no goals
Theorem: Matroid.indep_of_card_lt_girth
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hI : I.encard < M.girth
hIE : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I
Tactic:
rw [indep_iff_forall_subset_not_circuit]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hI : I.encard < M.girth
hIE : autoParam (I ⊆ M.E) _auto✝
⊢ ∀ C ⊆ I, ¬M.Circuit C
Theorem: Matroid.indep_of_card_lt_girth
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
hI : I.encard < M.girth
hIE : autoParam (I ⊆ M.E) _auto✝
⊢ ∀ C ⊆ I, ¬M.Circuit C
Tactic:
exact fun C hCI hC ↦ ((hC.girth_le_card.trans (encard_mono hCI)).trans_lt hI).ne rfl
Proof state after:
no goals
Theorem: Matroid.girth_eq_top_iff_ground_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
inst✝ : M.Finitary
⊢ M.girth = ⊤ ↔ M.Indep M.E
Tactic:
rw [girth_eq_top_iff, indep_iff_forall_subset_not_circuit]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
inst✝ : M.Finitary
⊢ (∀ (C : Set α), M.Circuit C → C.Infinite) ↔ ∀ C ⊆ M.E, ¬M.Circuit C
Theorem: Matroid.girth_eq_top_iff_ground_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
inst✝ : M.Finitary
⊢ (∀ (C : Set α), M.Circuit C → C.Infinite) ↔ ∀ C ⊆ M.E, ¬M.Circuit C
Tactic:
exact ⟨fun h C _ hC ↦ h C hC hC.finite, fun h C hC _ ↦ h C hC.subset_ground hC⟩
Proof state after:
no goals
Theorem: Matroid.Indep.rev_exchange_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ M.Indep (insert e I \ {f}) ↔ f ∈ M.fundCct e I
Tactic:
simp_rw [indep_iff_forall_subset_not_circuit', and_iff_left (diff_subset.trans
  (insert_subset ((M.cl_subset_ground I) he.1) hI.subset_ground)), imp_not_comm, subset_diff,
  disjoint_singleton_right, not_and, not_not]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ (∀ (C : Set α), M.Circuit C → C ⊆ insert e I → f ∈ C) ↔ f ∈ M.fundCct e I
Theorem: Matroid.Indep.rev_exchange_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ (∀ (C : Set α), M.Circuit C → C ⊆ insert e I → f ∈ C) ↔ f ∈ M.fundCct e I
Tactic:
exact ⟨fun h ↦ h _ (hI.fundCct_circuit he) (fundCct_subset_insert _ _),
  fun h C hC hCeI ↦ by rwa [hC.eq_fundCct_of_subset_insert_indep hI hCeI]⟩
Proof state after:
no goals
Theorem: Matroid.Indep.rev_exchange_indep_iff
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
h : f ∈ M.fundCct e I
C : Set α
hC : M.Circuit C
hCeI : C ⊆ insert e I
⊢ f ∈ C
Tactic:
rwa [hC.eq_fundCct_of_subset_insert_indep hI hCeI]
Proof state after:
no goals
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
Tactic:
suffices h1 : (∃ f, f ∈ B₂ \ B₁ ∧  M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})) by
  obtain ⟨f, hf, h₁, h₂⟩ := h1;
  exact ⟨f, hf, hB₂.exchange_base_of_indep' hf.1 he.2 h₁,
    hB₁.exchange_base_of_indep' he.1 hf.2 h₂⟩
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
Tactic:
have he₁ : e ∈ M.cl B₂ \ B₂ := by
  rw [hB₂.cl_eq]; exact ⟨hB₁.subset_ground he.1, he.2⟩
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
Tactic:
simp_rw [hB₂.indep.rev_exchange_indep_iff he₁]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ ∧ M.Indep (insert f B₁ \ {e})
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ ∧ M.Indep (insert f B₁ \ {e})
Tactic:
by_contra! h
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
⊢ False
Theorem: Matroid.Base.strong_exchange
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
⊢ False
Tactic:
have hC := hB₂.indep.fundCct_circuit he₁
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ False