internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
case refine'_1.heI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
exact fun heIs ↦ he.2 (sInter_subset_of_mem hI' heIs)
Proof state after:
no goals
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : e ∈ M.E \ ⋂ I_1 ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, M.cl I_1
⊢ False
Tactic:
simp at hi
Proof state after:
no goals
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
case refine'_1.hI
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hi : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
Tactic:
exact hI.subset (sInter_subset_of_mem hI')
Proof state after:
no goals
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e})
Tactic:
refine' hu.subset _
Proof state after:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e} ⊆ ⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e} ⊆ ⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
simp only [insert_diff_of_mem, mem_singleton]
Proof state after:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {e} ⊆ ⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
case refine'_2.inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
hf : e ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {e} ⊆ ⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
exact
  subset_trans diff_subset ((sInter_subset_of_mem hI').trans (subset_sUnion_of_mem hI'))
Proof state after:
no goals
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ e ∉ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
Tactic:
intro hcl
Proof state after:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
hcl : e ∈ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ False
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
case refine'_2.inr
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
hI : M.Indep I
he : e ∈ M.cl I \ I
hu : M.Indep (⋃₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hI' : I ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
f : α
hf : ∀ t ∈ {J | J ⊆ I ∧ e ∈ M.cl J}, f ∈ t
hne : ¬e = f
hi : M.Indep (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
hcl : e ∈ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})
⊢ False
Tactic:
exact (hf _ ⟨diff_subset.trans (sInter_subset_of_mem hI'), hcl⟩).2 rfl
Proof state after:
no goals
Theorem: Matroid.Base.fundCct_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hB : M.Base B
hx : x ∈ M.E \ B
⊢ M.Circuit (M.fundCct x B)
Tactic:
apply hB.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 α
hB : M.Base B
hx : x ∈ M.E \ B
⊢ x ∈ M.cl B \ B
Theorem: Matroid.Base.fundCct_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hB : M.Base B
hx : x ∈ M.E \ B
⊢ x ∈ M.cl B \ B
Tactic:
rwa [hB.cl_eq]
Proof state after:
no goals
Theorem: Matroid.Dep.exists_circuit_subset
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : M.Dep X
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
rw [dep_iff, indep_iff_not_mem_cl_diff_forall] at hX
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (¬∀ e ∈ X, e ∉ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C
Theorem: Matroid.Dep.exists_circuit_subset
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (¬∀ e ∈ X, e ∉ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
push_neg at hX
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (∃ e ∈ X, e ∈ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C
Theorem: Matroid.Dep.exists_circuit_subset
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : (∃ e ∈ X, e ∈ M.cl (X \ {e})) ∧ X ⊆ M.E
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
obtain ⟨⟨e, he, heX⟩, hXE⟩ := hX
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 : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Theorem: Matroid.Dep.exists_circuit_subset
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 : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (X \ {e}) (diff_subset.trans hXE)
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
I : Set α
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Theorem: Matroid.Dep.exists_circuit_subset
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
heX : e ∈ M.cl (X \ {e})
I : Set α
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
rw [← hI.cl_eq_cl] at heX
Proof state after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Theorem: Matroid.Dep.exists_circuit_subset
Proof state before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
hXE : X ⊆ M.E
e : α
he : e ∈ X
I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X \ {e})
⊢ ∃ C ⊆ X, M.Circuit C
Tactic:
exact ⟨_, (fundCct_subset_insert e I).trans
  (insert_subset he (hI.subset.trans diff_subset)),
  hI.indep.fundCct_circuit ⟨heX, not_mem_subset hI.subset (not_mem_diff_of_mem rfl)⟩⟩
Proof state after:
no goals
Theorem: Matroid.indep_iff_forall_subset_not_circuit'
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Indep I ↔ (∀ C ⊆ I, ¬M.Circuit C) ∧ I ⊆ M.E
Tactic:
simp_rw [indep_iff_not_dep, dep_iff_superset_circuit', not_and, imp_not_comm (b := _ ⊆ _)]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ (I ⊆ M.E → ¬∃ C ⊆ I, M.Circuit C) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.Circuit C) ∧ I ⊆ M.E
Theorem: Matroid.indep_iff_forall_subset_not_circuit'
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ (I ⊆ M.E → ¬∃ C ⊆ I, M.Circuit C) ∧ I ⊆ M.E ↔ (∀ C ⊆ I, ¬M.Circuit C) ∧ I ⊆ M.E
Tactic:
aesop
Proof state after:
no goals
Theorem: Matroid.indep_iff_forall_subset_not_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Indep I ↔ ∀ C ⊆ I, ¬M.Circuit C
Tactic:
rw [indep_iff_forall_subset_not_circuit', and_iff_left hI]
Proof state after:
no goals
Theorem: Matroid.mem_cl_iff_mem_or_exists_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ e ∈ M.cl X ↔ e ∈ X ∨ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
refine' (em (e ∈ X)).elim (fun he ↦ iff_of_true (M.mem_cl_of_mem he) (Or.inl he)) (fun he ↦ _)
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
⊢ e ∈ M.cl X ↔ e ∈ X ∨ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Theorem: Matroid.mem_cl_iff_mem_or_exists_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
⊢ e ∈ M.cl X ↔ e ∈ X ∨ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
rw [or_iff_right he]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
⊢ e ∈ M.cl X ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Theorem: Matroid.mem_cl_iff_mem_or_exists_circuit
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
⊢ e ∈ M.cl X ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
refine' ⟨fun h ↦ _, fun ⟨C, hC, heC, hCX⟩ ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X

case refine'_2
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ e ∈ M.cl X
Theorem: Matroid.mem_cl_iff_mem_or_exists_circuit
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ e ∈ M.cl X
Tactic:
refine' ((hC.subset_cl_diff_singleton e).trans (M.cl_subset_cl _)) heC
Proof state after:
case refine'_2
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ C \ {e} ⊆ X
Theorem: Matroid.mem_cl_iff_mem_or_exists_circuit
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCX : C ⊆ insert e X
⊢ C \ {e} ⊆ X
Tactic:
rwa [diff_subset_iff, singleton_union]
Proof state after:
no goals
Theorem: Matroid.mem_cl_iff_mem_or_exists_circuit
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis X
Proof state after:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
I : Set α
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Theorem: Matroid.mem_cl_iff_mem_or_exists_circuit
Proof state before:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
h : e ∈ M.cl X
I : Set α
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
rw [← hI.cl_eq_cl] at h
Proof state after:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
I : Set α
h : e ∈ M.cl I
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Theorem: Matroid.mem_cl_iff_mem_or_exists_circuit
Proof state before:
case refine'_1.intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
hX : autoParam (X ⊆ M.E) _auto✝
he : e ∉ X
I : Set α
h : e ∈ M.cl I
hI : M.Basis I X
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
exact ⟨M.fundCct e I, hI.indep.fundCct_circuit ⟨h, not_mem_subset hI.subset he⟩,
  M.mem_fundCct e I, (fundCct_subset_insert _ _).trans (insert_subset_insert hI.subset)⟩
Proof state after:
no goals
Theorem: Matroid.mem_cl_iff_exists_circuit_of_not_mem
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
⊢ e ∈ M.cl X ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
rw [← cl_inter_ground, mem_cl_iff_mem_or_exists_circuit, mem_inter_iff, iff_false_intro he,
  false_and_iff, false_or_iff]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
⊢ (∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e (X ∩ M.E)) ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Theorem: Matroid.mem_cl_iff_exists_circuit_of_not_mem
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
⊢ (∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e (X ∩ M.E)) ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
refine' ⟨
  fun ⟨C, hC, heC, h⟩ ↦ ⟨C, hC, heC, h.trans ((insert_subset_insert inter_subset_left))⟩,
  fun ⟨C, hC, heC, h⟩ ↦ ⟨C, hC, heC, (subset_inter h hC.subset_ground).trans _⟩⟩
Proof state after:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
h : C ⊆ insert e X
⊢ insert e X ∩ M.E ⊆ insert e (X ∩ M.E)
Theorem: Matroid.mem_cl_iff_exists_circuit_of_not_mem
Proof state before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
h : C ⊆ insert e X
⊢ insert e X ∩ M.E ⊆ insert e (X ∩ M.E)
Tactic:
rw [insert_inter_of_mem (hC.subset_ground heC)]
Proof state after:
no goals
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
set Y := (C ∪ ⋃ x, Cs x) \ insert z (range x) with hY
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
have hYE : Y ⊆ M.E := by
  refine' diff_subset.trans (union_subset hC.subset_ground _)
  exact iUnion_subset fun i ↦ (hCs i).subset_ground
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
have h₂ : range x ⊆ M.cl Y := by
  refine' h₁.trans (M.cl_subset_cl (iUnion_subset fun x ↦ _))
  refine' diff_subset_diff_left (subset_union_of_subset_right _ _)
  exact subset_iUnion_of_subset x diff_subset
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
have h₃ : C \ {z} ⊆ M.cl Y := by
  suffices C \ {z} ⊆ C \ insert z (range x) ∪ range x by
    rw [union_diff_distrib] at hY
    convert this.trans (union_subset_union (subset_union_left.trans_eq hY.symm) h₂) using 1
    rw [union_eq_right.mpr]
    exact M.subset_cl Y
  rw [← union_singleton, ← diff_diff, diff_subset_iff, singleton_union, ← insert_union,
    insert_diff_singleton, ← singleton_union, union_assoc, diff_union_self]
  exact subset_union_of_subset_right subset_union_left _
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : C \ {z} ⊆ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : C \ {z} ⊆ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
rw [← M.cl_subset_cl_iff_subset_cl (diff_subset.trans hC.subset_ground)] at h₃
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
have h₄ := h₃ (hC.subset_cl_diff_singleton z hz.1)
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Theorem: Matroid.Circuit.strong_multi_elimination
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x
Tactic:
obtain (hzY | ⟨C', hC', hzC', hCzY⟩) := (mem_cl_iff_mem_or_exists_circuit hYE).mp h₄
Proof state after:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
hzY : z ∈ Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x

case inr.intro.intro.intro
α : Type u_1
M : Matroid α
C C'✝ I X K C₁ C₂ R : Set α
e f x✝ y : α
ι : Type u_2
hC : M.Circuit C
x : ι → α
Cs : ι → Set α
hCs : ∀ (i : ι), M.Circuit (Cs i)
h_mem : ∀ (i : ι), x i ∈ C ∩ Cs i
h_unique : ∀ (i i' : ι), x i ∈ Cs i' → i = i'
z : α
hz : z ∈ C \ ⋃ i, Cs i
Y : Set α := (C ∪ ⋃ x, Cs x) \ insert z (range x)
hY : Y = (C ∪ ⋃ x, Cs x) \ insert z (range x)
hYE : Y ⊆ M.E
h₁ : range x ⊆ M.cl (⋃ i, (Cs i \ {x i}) \ insert z (range x))
h₂ : range x ⊆ M.cl Y
h₃ : M.cl (C \ {z}) ⊆ M.cl Y
h₄ : z ∈ M.cl Y
C' : Set α
hC' : M.Circuit C'
hzC' : z ∈ C'
hCzY : C' ⊆ insert z Y
⊢ ∃ C', M.Circuit C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ ⋃ i, Cs i) \ range x