internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Circuit.basis_iff_eq_diff_singleton
Proof state before:
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit I
h : M.Basis I I
⊢ False
Tactic:
exact hC.dep.not_indep h.indep
Proof state after:
no goals
Theorem: Matroid.Circuit.basis_iff_insert_eq
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ M.Basis I C ↔ ∃ e ∈ C \ I, C = insert e I
Tactic:
rw [hC.basis_iff_eq_diff_singleton]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I
Theorem: Matroid.Circuit.basis_iff_insert_eq
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I
Tactic:
refine' ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, _⟩,
  fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, _⟩⟩
Proof state after:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I

case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC✝ : M.Circuit C
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}
Theorem: Matroid.Circuit.basis_iff_insert_eq
Proof state before:
case refine'_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC✝ : M.Circuit C
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}
Tactic:
rw [hC, insert_diff_self_of_not_mem he.2]
Proof state after:
no goals
Theorem: Matroid.Circuit.basis_iff_insert_eq
Proof state before:
case refine'_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I
Tactic:
rw [hI, insert_diff_singleton, insert_eq_of_mem he]
Proof state after:
no goals
Theorem: Matroid.Circuit.cl_diff_singleton_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ M.cl (C \ {e}) = M.cl C
Tactic:
rw [(hC.diff_singleton_basis he).cl_eq_cl]
Proof state after:
no goals
Theorem: Matroid.Circuit.cl_diff_singleton_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ M.cl (C \ {e}) = M.cl C
Tactic:
rw [diff_singleton_eq_self he]
Proof state after:
no goals
Theorem: Matroid.Circuit.subset_cl_diff_singleton
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
⊢ C ⊆ M.cl (C \ {e})
Tactic:
by_cases he : e ∈ C
Proof state after:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ M.cl (C \ {e})

case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ C ⊆ M.cl (C \ {e})
Theorem: Matroid.Circuit.subset_cl_diff_singleton
Proof state before:
case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ C ⊆ M.cl (C \ {e})
Tactic:
rw [diff_singleton_eq_self he]
Proof state after:
case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ C ⊆ M.cl C
Theorem: Matroid.Circuit.subset_cl_diff_singleton
Proof state before:
case neg
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∉ C
⊢ C ⊆ M.cl C
Tactic:
exact M.subset_cl _
Proof state after:
no goals
Theorem: Matroid.Circuit.subset_cl_diff_singleton
Proof state before:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ M.cl (C \ {e})
Tactic:
rw [(hC.diff_singleton_basis he).cl_eq_cl]
Proof state after:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ M.cl C
Theorem: Matroid.Circuit.subset_cl_diff_singleton
Proof state before:
case pos
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
hC : M.Circuit C
e : α
he : e ∈ C
⊢ C ⊆ M.cl C
Tactic:
exact M.subset_cl _
Proof state after:
no goals
Theorem: Matroid.Circuit.subset_cl_diff_subsingleton
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
Z : Set α
hZ : Z.encard ≤ 1
⊢ C ⊆ M.cl (C \ Z)
Tactic:
obtain (rfl | ⟨x, rfl⟩) := encard_le_one_iff_eq.1 hZ
Proof state after:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl (C \ ∅)

case inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
hC : M.Circuit C
x : α
hZ : {x}.encard ≤ 1
⊢ C ⊆ M.cl (C \ {x})
Theorem: Matroid.Circuit.subset_cl_diff_subsingleton
Proof state before:
case inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
hC : M.Circuit C
x : α
hZ : {x}.encard ≤ 1
⊢ C ⊆ M.cl (C \ {x})
Tactic:
exact hC.subset_cl_diff_singleton _
Proof state after:
no goals
Theorem: Matroid.Circuit.subset_cl_diff_subsingleton
Proof state before:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl (C \ ∅)
Tactic:
rw [diff_empty]
Proof state after:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl C
Theorem: Matroid.Circuit.subset_cl_diff_subsingleton
Proof state before:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hZ : ∅.encard ≤ 1
⊢ C ⊆ M.cl C
Tactic:
apply M.subset_cl _
Proof state after:
no goals
Theorem: Matroid.Circuit.cl_diff_subsingleton_eq_cl
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
Z : Set α
hZ : Z.encard ≤ 1
⊢ M.cl (C \ Z) = M.cl C
Tactic:
obtain (rfl | ⟨x, rfl⟩) := encard_le_one_iff_eq.1 hZ
Proof state after:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hZ : ∅.encard ≤ 1
⊢ M.cl (C \ ∅) = M.cl C

case inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
hC : M.Circuit C
x : α
hZ : {x}.encard ≤ 1
⊢ M.cl (C \ {x}) = M.cl C
Theorem: Matroid.Circuit.cl_diff_subsingleton_eq_cl
Proof state before:
case inr.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x✝ y : α
hC : M.Circuit C
x : α
hZ : {x}.encard ≤ 1
⊢ M.cl (C \ {x}) = M.cl C
Tactic:
rw [hC.cl_diff_singleton_eq_cl]
Proof state after:
no goals
Theorem: Matroid.Circuit.cl_diff_subsingleton_eq_cl
Proof state before:
case inl
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hZ : ∅.encard ≤ 1
⊢ M.cl (C \ ∅) = M.cl C
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.empty_not_circuit
Proof state before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
M : Matroid α
h : M.Circuit ∅
⊢ False
Tactic:
simpa using h.nonempty
Proof state after:
no goals
Theorem: Matroid.Circuit.circuit_restrict_of_subset
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hCR : C ⊆ R
⊢ (M ↾ R).Circuit C
Tactic:
simp_rw [circuit_iff, restrict_dep_iff, dep_iff, and_imp] at *
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ R → I ⊆ C → I = C
Theorem: Matroid.Circuit.circuit_restrict_of_subset
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ R → I ⊆ C → I = C
Tactic:
refine' ⟨⟨hC.1.1, hCR⟩, fun I hI _ hIC ↦ hC.2 hI (hIC.trans hC.1.2) hIC⟩
Proof state after:
no goals
Theorem: Matroid.restrict_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).Circuit C ↔ M.Circuit C ∧ C ⊆ R
Tactic:
refine' ⟨_, fun h ↦ h.1.circuit_restrict_of_subset h.2⟩
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).Circuit C → M.Circuit C ∧ C ⊆ R
Theorem: Matroid.restrict_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).Circuit C → M.Circuit C ∧ C ⊆ R
Tactic:
simp_rw [circuit_iff, restrict_dep_iff, and_imp, dep_iff]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ R → I ⊆ C → I = C) →
        ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I ∧ I ⊆ M.E → I ⊆ C → I = C) ∧ C ⊆ R
Theorem: Matroid.restrict_circuit_iff
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ R → I ⊆ C → I = C) →
        ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I ∧ I ⊆ M.E → I ⊆ C → I = C) ∧ C ⊆ R
Tactic:
exact fun hC hCR h ↦ ⟨⟨⟨hC,hCR.trans hR⟩,fun I hI hIC ↦ h hI.1 (hIC.trans hCR) hIC⟩,hCR⟩
Proof state after:
no goals
Theorem: Matroid.circuit_iff_dep_forall_diff_singleton_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Circuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
Tactic:
rw [circuit_iff_forall_ssubset, and_congr_right_iff]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Dep C → ((∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I) ↔ ∀ e ∈ C, M.Indep (C \ {e}))
Theorem: Matroid.circuit_iff_dep_forall_diff_singleton_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Dep C → ((∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I) ↔ ∀ e ∈ C, M.Indep (C \ {e}))
Tactic:
refine' fun _ ↦ ⟨fun h e heC ↦ h (Iff.mpr diff_singleton_sSubset heC),
  fun h I hIC ↦ _⟩
Proof state after:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
x✝ : M.Dep C
h : ∀ e ∈ C, M.Indep (C \ {e})
I : Set α
hIC : I ⊂ C
⊢ M.Indep I
Theorem: Matroid.circuit_iff_dep_forall_diff_singleton_indep
Proof state before:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
x✝ : M.Dep C
h : ∀ e ∈ C, M.Indep (C \ {e})
I : Set α
hIC : I ⊂ C
⊢ M.Indep I
Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset hIC
Proof state after:
case intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
x✝ : M.Dep C
h : ∀ e ∈ C, M.Indep (C \ {e})
I : Set α
hIC : I ⊂ C
e : α
he : e ∈ C ∧ e ∉ I
⊢ M.Indep I
Theorem: Matroid.circuit_iff_dep_forall_diff_singleton_indep
Proof state before:
case intro
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
x✝ : M.Dep C
h : ∀ e ∈ C, M.Indep (C \ {e})
I : Set α
hIC : I ⊂ C
e : α
he : e ∈ C ∧ e ∉ I
⊢ M.Indep I
Tactic:
exact (h e he.1).subset (subset_diff_singleton hIC.subset he.2)
Proof state after:
no goals
Theorem: Matroid.fundCct_eq_sInter
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∈ M.cl I
⊢ M.fundCct e I = insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
Tactic:
rw [fundCct, inter_eq_self_of_subset_right]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∈ M.cl I
⊢ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ I
Theorem: Matroid.fundCct_eq_sInter
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∈ M.cl I
⊢ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ I
Tactic:
exact sInter_subset_of_mem ⟨Subset.rfl, he⟩
Proof state after:
no goals
Theorem: Matroid.Indep.fundCct_eq_of_mem
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ M.fundCct e I = {e}
Tactic:
rw [fundCct, ← union_singleton, union_eq_right]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ I ∩ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ {e}
Theorem: Matroid.Indep.fundCct_eq_of_mem
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ I ∩ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} ⊆ {e}
Tactic:
refine inter_subset_right.trans (sInter_subset_of_mem ?_)
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ {e} ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
Theorem: Matroid.Indep.fundCct_eq_of_mem
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ {e} ∈ {J | J ⊆ I ∧ e ∈ M.cl J}
Tactic:
simp only [mem_setOf, singleton_subset_iff, and_iff_right he]
Proof state after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ e ∈ M.cl {e}
Theorem: Matroid.Indep.fundCct_eq_of_mem
Proof state before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hI : M.Indep I
he : e ∈ I
⊢ e ∈ M.cl {e}
Tactic:
exact M.mem_cl_self _ (hI.subset_ground he)
Proof state after:
no goals
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
α : 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
⊢ M.Circuit (M.fundCct e I)
Tactic:
rw [circuit_iff_dep_forall_diff_singleton_indep,
  ← not_indep_iff (fundCct_subset_ground (M.cl_subset_ground I he.1)), fundCct_eq_sInter he.1]
Proof state after:
α : 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
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
α : 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
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Tactic:
have hu : M.Indep (⋃₀ {J : Set α | J ⊆ I ∧ e ∈ M.cl J}) :=
  hI.subset (sUnion_subset fun J ↦ And.left)
Proof state after:
α : 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})
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
α : 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})
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Tactic:
have hI' : I ∈ {J : Set α | J ⊆ I ∧ e ∈ M.cl J} := ⟨rfl.subset, he.1⟩
Proof state after:
α : 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}
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Theorem: Matroid.Indep.fundCct_circuit
Proof state before:
α : 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}
⊢ ¬M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})) ∧
    ∀ e_1 ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}), M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e_1})
Tactic:
refine' ⟨fun hi ↦ _, fun f hf ↦ _⟩
Proof state after:
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 : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ False

case refine'_2
α : 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 : f ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Theorem: Matroid.Indep.fundCct_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 : α
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 : f ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Tactic:
obtain rfl | hne := em (e = f)
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})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {e})

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 : f ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hne : ¬e = f
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
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 : f ∈ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
hne : ¬e = f
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Tactic:
rw [mem_insert_iff, mem_sInter, eq_comm, iff_false_intro hne, false_or_iff] at hf
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
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
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
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Tactic:
have hi : M.Indep (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.cl J} \ {f}) :=
  hI.subset (diff_subset.trans (sInter_subset_of_mem hI'))
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})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
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})
⊢ M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}) \ {f})
Tactic:
rw [← insert_diff_singleton_comm hne, hi.insert_indep_iff_of_not_mem, mem_diff,
  and_iff_right ((M.cl_subset_ground _) he.1)]
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})
⊢ e ∉ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f})

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 ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f}
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 ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J} \ {f}
Tactic:
exact fun h'e ↦ he.2 (diff_subset.trans (sInter_subset_of_mem hI') h'e)
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 : M.Indep (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J}))
⊢ False
Tactic:
rw [Indep.insert_indep_iff_of_not_mem] at hi
Proof state after:
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 \ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ False

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})

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}
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 \ M.cl (⋂₀ {J | J ⊆ I ∧ e ∈ M.cl J})
⊢ False

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})

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:
rw [cl_sInter_eq_biInter_cl_of_sUnion_indep _  ⟨_, hI'⟩ hu] at hi
Proof state after:
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

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})

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}