awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : M.IsColoop e
rw rw₁ : e ∈ X ↔ e ∈ X
⊢ e ∈ M.closure X ↔ e ∈ X

Tactic:
rw [he.mem_closure_iff_mem]

Premises used: Matroid.IsColoop.mem_closure_iff_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
nth_rw : M.closure X ∩ (M.coloops ∩ K) = X ∩ K
⊢ M.closure X ∩ K = X ∩ K

Tactic:
nth_rw 1 [← inter_eq_self_of_subset_right hK]

Premises used: Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
rw : M.closure X ∩ M.coloops ∩ K = X ∩ K
rw₁ : X ∩ M.coloops ∩ K = X ∩ K
rw₂ : X ∩ (M.coloops ∩ K) = X ∩ K
rw₃ rw₄ : X ∩ K = X ∩ K
⊢ M.closure X ∩ (M.coloops ∩ K) = X ∩ K

Tactic:
rw [← inter_assoc, closure_inter_coloops_eq, inter_assoc, inter_eq_self_of_subset_right hK]

Premises used: Set.inter_eq_self_of_subset_right, Matroid.closure_inter_coloops_eq, Set.inter_assoc
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
rw : ∀ (x : α), x ∉ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
⊢ M.closure (X ∪ K) = M.closure X ∪ K

Tactic:
rw [← closure_union_closure_left_eq, subset_antisymm_iff, and_iff_left (M.subset_closure _),
    ← diff_eq_empty, eq_empty_iff_forall_notMem]

Premises used: and_iff_left, Matroid.closure_union_closure_left_eq, Matroid.subset_closure, Set.eq_empty_iff_forall_notMem, subset_antisymm_iff, Set.diff_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ ∀ (x : α), x ∉ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)

Tactic:
fun e ⟨hecl, he⟩ ↦ he (.inl ?_)

Premises used: False, _private.0.Matroid.closure_union_eq_of_subset_coloops.match_2, Or.inl, Not
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
refine :
  ∀ e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K),
    ∀ (hecl : e ∈ M.closure (M.closure X ∪ K)) (he : e ∉ M.closure X ∪ K), e ∈ M.closure X
⊢ ∀ (x : α), x ∉ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)

Tactic:
refine fun e ⟨hecl, he⟩ ↦ he (.inl ?_)
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
h : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
obtain : ∀ (C : Set α) (hCss : C ⊆ insert e (M.closure X ∪ K)) (hC : M.IsCircuit C) (heC : e ∈ C), e ∈ M.closure X
⊢ e ∈ M.closure X

Tactic:
obtain ⟨C, hCss, hC, heC⟩ := (mem_closure_iff_exists_isCircuit he).1 hecl

Premises used: Iff.mp, Matroid.mem_closure_iff_exists_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
h : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X ∪ K)
hC : M.IsCircuit C
heC : e ∈ C
⊢ C ⊆ insert e (M.closure X)

Tactic:
rw [← singleton_union, ← union_assoc, union_comm, ← diff_subset_iff,
    (hC.disjoint_coloops.mono_right hK).sdiff_eq_left, singleton_union] at hCss

Premises used: Set.diff_subset_iff, Set.singleton_union, Set.union_comm, Matroid.IsCircuit.disjoint_coloops, Disjoint.sdiff_eq_left, Set.union_assoc, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
h : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X ∪ K)
hC : M.IsCircuit C
heC : e ∈ C
hCss₁ : C ⊆ insert e (M.closure X)
⊢ M.IsCircuit C

Tactic:
rw [← singleton_union, ← union_assoc, union_comm, ← diff_subset_iff,
    (hC.disjoint_coloops.mono_right hK).sdiff_eq_left, singleton_union] at hCss

Premises used: Set.diff_subset_iff, Set.singleton_union, Set.union_comm, Matroid.IsCircuit.disjoint_coloops, Disjoint.sdiff_eq_left, Set.union_assoc, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
h : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X ∪ K)
hC : M.IsCircuit C
heC : e ∈ C
hCss₁ : C ⊆ insert e (M.closure X)
hC₁ : M.IsCircuit C
⊢ e ∈ C

Tactic:
rw [← singleton_union, ← union_assoc, union_comm, ← diff_subset_iff,
    (hC.disjoint_coloops.mono_right hK).sdiff_eq_left, singleton_union] at hCss

Premises used: Set.diff_subset_iff, Set.singleton_union, Set.union_comm, Matroid.IsCircuit.disjoint_coloops, Disjoint.sdiff_eq_left, Set.union_assoc, Disjoint.mono_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
h : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X)
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ M.closure X

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
h : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X)
hC : M.IsCircuit C
heC : e ∈ C
⊢ e ∈ M.closure X

Tactic:
exact M.closure_subset_closure_of_subset_closure (by simpa) <|
    hC.mem_closure_diff_singleton_of_mem heC

Premises used: Matroid.IsCircuit.mem_closure_diff_singleton_of_mem, Matroid.closure_subset_closure_of_subset_closure
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ {e} ⊆ M.coloops

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
rw : M.closure (X ∪ {e}) = insert e (M.closure X)
rw₁ : M.closure X ∪ {e} = insert e (M.closure X)
rw₂ rw₃ : insert e (M.closure X) = insert e (M.closure X)
⊢ M.closure (insert e X) = insert e (M.closure X)

Tactic:
rw [← union_singleton, closure_union_eq_of_subset_coloops _ (by simpa), union_singleton]

Premises used: Matroid.closure_union_eq_of_subset_coloops, Set.union_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K : Set α
hK : K ⊆ M.coloops
rw : M.closure (∅ ∪ K) = ∅ ∪ K ∪ M.loops
rw₁ : M.closure ∅ ∪ K = ∅ ∪ K ∪ M.loops
rw₂ : M.closure ∅ ∪ K = K ∪ M.loops
rw₃ : K ∪ M.closure ∅ = K ∪ M.loops
rw₄ rw₅ : K ∪ M.loops = K ∪ M.loops
⊢ M.closure K = K ∪ M.loops

Tactic:
rw [← empty_union K, closure_union_eq_of_subset_coloops _ hK, empty_union, union_comm,
    closure_empty]

Premises used: Matroid.closure_empty, Set.empty_union, Matroid.closure_union_eq_of_subset_coloops, Set.union_comm
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
nth_rw : M.closure (X \ K) = M.closure (X ∩ K ∪ X \ K) \ K
⊢ M.closure (X \ K) = M.closure X \ K

Tactic:
nth_rw 2 [← inter_union_diff X K]

Premises used: Set.inter_union_diff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
rw : ∀ ⦃a : α⦄, a ∈ K → ∀ ⦃b : α⦄, b ∈ M.closure (X \ K) → a ≠ b
⊢ M.closure (X \ K) = M.closure (X ∩ K ∪ X \ K) \ K

Tactic:
rw [union_comm, closure_union_eq_of_subset_coloops _ (inter_subset_right.trans hK),
    union_diff_distrib, diff_eq_empty.mpr inter_subset_right, union_empty, eq_comm,
    sdiff_eq_self_iff_disjoint, disjoint_iff_forall_ne]

Premises used: Iff.mpr, Set.union_empty, HasSubset.Subset.trans, Matroid.closure_union_eq_of_subset_coloops, Set.union_comm, eq_comm, Set.union_diff_distrib, Set.disjoint_iff_forall_ne, sdiff_eq_self_iff_disjoint, Set.diff_eq_empty, Set.inter_subset_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
heK : e ∈ K
heX : e ∈ M.closure (X \ K)
⊢ e ∈ X \ K

Tactic:
rw [IsColoop.mem_closure_iff_mem (hK heK)] at heX

Premises used: Matroid.IsColoop.mem_closure_iff_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
heK : e ∈ K
heX : e ∈ X \ K
⊢ False

Tactic:
heX.2 heK

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
heK : e ∈ K
heX : e ∈ X \ K
⊢ False

Tactic:
exact heX.2 heK

Premises used: And.right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X K : Set α
hXK : Disjoint X K
hK : K ⊆ M.coloops
rwa : M.closure X ∩ K = ∅
rwa₁ : X ∩ K = ∅
rwa₂ rwa₃ rwa₄ rwa₅ : Disjoint X K
⊢ Disjoint (M.closure X) K

Tactic:
rwa [disjoint_iff_inter_eq_empty, closure_inter_eq_of_subset_coloops X hK,
    ← disjoint_iff_inter_eq_empty]

Premises used: Matroid.closure_inter_eq_of_subset_coloops, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
hX : Disjoint X M.coloops
⊢ Disjoint (M.closure X) M.coloops

Tactic:
closure_disjoint_of_disjoint_of_subset_coloops hX Subset.rfl

Premises used: Matroid.closure_disjoint_of_disjoint_of_subset_coloops, Set.Subset.rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∪ M.coloops) = M.closure X ∪ M.coloops

Tactic:
closure_union_eq_of_subset_coloops _ Subset.rfl

Premises used: Matroid.closure_union_eq_of_subset_coloops, Set.Subset.rfl
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
hX : e ∉ X
⊢ e ∉ M.closure X

Tactic:
mt he.mem_closure_iff_mem.mp hX

Premises used: mt, Iff.mp, Matroid.IsColoop.mem_closure_iff_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∈ I
rwa rwa₁ rwa₂ rwa₃ : M.Indep I
⊢ M.Indep (insert e I)

Tactic:
rwa [insert_eq_of_mem h]

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
⊢ e ∉ I

Tactic:
refine (em (e ∈ I)).elim (fun h ↦ by rwa [insert_eq_of_mem h]) fun h ↦ ?_

Premises used: Membership.mem, em, Or.elim
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∉ I
rw : e ∉ M.closure I
⊢ M.Indep (insert e I)

Tactic:
rw [← hI.notMem_closure_iff_of_notMem h]

Premises used: Matroid.Indep.notMem_closure_iff_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∉ I
⊢ e ∉ M.closure I

Tactic:
he.notMem_closure_of_notMem h

Premises used: Matroid.IsColoop.notMem_closure_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∉ I
⊢ e ∉ M.closure I

Tactic:
exact he.notMem_closure_of_notMem h

Premises used: Matroid.IsColoop.notMem_closure_of_notMem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
⊢ M.Indep (I ∪ K) ↔ M.Indep I

Tactic:
⟨fun h ↦ h.subset subset_union_left, fun h ↦ ?_⟩

Premises used: Matroid.Indep.subset, Set.subset_union_left, Iff.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
refine : ∀ (h : M.Indep I), M.Indep (I ∪ K)
⊢ M.Indep (I ∪ K) ↔ M.Indep I

Tactic:
refine ⟨fun h ↦ h.subset subset_union_left, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
h : M.Indep I
obtain : ∀ (B : Set α) (hB : M.IsBase B) (hIB : I ⊆ B), M.Indep (I ∪ K)
⊢ M.Indep (I ∪ K)

Tactic:
obtain ⟨B, hB, hIB⟩ := h.exists_isBase_superset

Premises used: Matroid.Indep.exists_isBase_superset
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
h : M.Indep I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.Indep (I ∪ K)

Tactic:
hB.indep.subset (union_subset hIB (hK.trans fun e he ↦ IsColoop.mem_of_isBase he hB))

Premises used: HasSubset.Subset.trans, Matroid.Indep.subset, Set.union_subset, Matroid.IsColoop.mem_of_isBase, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
h : M.Indep I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.Indep (I ∪ K)

Tactic:
exact hB.indep.subset (union_subset hIB (hK.trans fun e he ↦ IsColoop.mem_of_isBase he hB))

Premises used: HasSubset.Subset.trans, Matroid.Indep.subset, Set.union_subset, Matroid.IsColoop.mem_of_isBase, Matroid.IsBase.indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I K : Set α
hK : K ⊆ M.coloops
rw : M.Indep (I \ K ∪ K) ↔ M.Indep I
rw₁ : M.Indep (I ∪ K) ↔ M.Indep I
rw₂ rw₃ : M.Indep I ↔ M.Indep I
⊢ M.Indep (I \ K) ↔ M.Indep I

Tactic:
rw [← union_indep_iff_indep_of_subset_coloops hK, diff_union_self,
    union_indep_iff_indep_of_subset_coloops hK]

Premises used: Set.diff_union_self, Matroid.union_indep_iff_indep_of_subset_coloops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep (I ∪ M.coloops) ↔ M.Indep I

Tactic:
union_indep_iff_indep_of_subset_coloops Subset.rfl

Premises used: Set.Subset.rfl, Matroid.union_indep_iff_indep_of_subset_coloops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep (I \ M.coloops) ↔ M.Indep I

Tactic:
diff_indep_iff_indep_of_subset_coloops Subset.rfl

Premises used: Set.Subset.rfl, Matroid.diff_indep_iff_indep_of_subset_coloops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
rw : M.Indep ∅
⊢ M.Indep M.coloops

Tactic:
rw [← empty_union M.coloops, union_coloops_indep_iff]

Premises used: Matroid.coloops, Set.empty_union, Matroid.union_coloops_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.Indep ∅

Tactic:
M.empty_indep

Premises used: Matroid.empty_indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
⊢ M.Indep ∅

Tactic:
exact M.empty_indep

Premises used: Matroid.empty_indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
inr :
  ∀
    (this :
      ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) (heR : e ∈ R),
        (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R)
    (heR : e ∉ R), (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
wlog :
  ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) (heR : e ∈ R),
    (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

Tactic:
wlog heR : e ∈ R
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
this :
  ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) (heR : e ∈ R),
    (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
heR : e ∉ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

Tactic:
iff_of_false (fun h ↦ heR h.mem_ground) fun h ↦ heR h.2

Premises used: Matroid.IsColoop.mem_ground, iff_of_false, And.right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
this :
  ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) (heR : e ∈ R),
    (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
heR : e ∉ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

Tactic:
exact iff_of_false (fun h ↦ heR h.mem_ground) fun h ↦ heR h.2

Premises used: iff_of_false
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α_1 : Type u_1
M_1 : Matroid α_1
e_1 : α_1
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ e ∉ R \ {e}

Tactic:
simp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α_1 : Type u_1
M_1 : Matroid α_1
e_1 : α_1
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
rw : (∀ ⦃C : Set α⦄, (M ↾ R).IsCircuit C → e ∉ C) ↔ (¬∃ C ⊆ insert e (R \ {e}), M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R
⊢ (M ↾ R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R

Tactic:
rw [isColoop_iff_forall_notMem_isCircuit heR, mem_closure_iff_exists_isCircuit (by simp)]

Premises used: Matroid.mem_closure_iff_exists_isCircuit, Matroid.isColoop_iff_forall_notMem_isCircuit
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α_1 : Type u_1
M_1 : Matroid α_1
e_1 : α_1
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
simp : (∀ ⦃C : Set α⦄, M.IsCircuit C ∧ C ⊆ R → e ∉ C) ↔ (¬∃ C ⊆ insert e R, M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R
⊢ (∀ ⦃C : Set α⦄, (M ↾ R).IsCircuit C → e ∉ C) ↔ (¬∃ C ⊆ insert e (R \ {e}), M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R

Tactic:
simp only [restrict_isCircuit_iff hRE, insert_diff_singleton]

Premises used: Matroid.restrict_isCircuit_iff, Set.insert_diff_singleton
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α_1 : Type u_1
M_1 : Matroid α_1
e_1 : α_1
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C ∧ C ⊆ R → e ∉ C) ↔ (¬∃ C ⊆ insert e R, M.IsCircuit C ∧ e ∈ C) ∧ e ∈ R

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
⊢ M₁ = M₂

Tactic:
ext_indep hE fun I hI ↦ ?_

Premises used: Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
refine : ∀ (I : Set α) (hI : I ⊆ M₁.E), M₁.Indep I ↔ M₂.Indep I
⊢ M₁ = M₂

Tactic:
refine ext_indep hE fun I hI ↦ ?_

Premises used: Matroid.ext_indep
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
rw : M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
rw [← diff_coloops_indep_iff, ← @diff_coloops_indep_iff _ M₂, ← hc]

Premises used: Matroid.diff_coloops_indep_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
inl : ∀ (hdj : Disjoint I M₁.loops), M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
inr : ∀ (hndj : ¬Disjoint I M₁.loops), M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

Tactic:
obtain hdj | hndj := em (Disjoint I (M₁.loops))

Premises used: Disjoint, em, Matroid.loops
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
inl : Disjoint (I \ M₁.coloops) (M₁.loops ∪ M₁.coloops)
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

Tactic:
rw [h _ (diff_subset.trans hI)]

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
inl : Disjoint (I \ M₁.coloops) M₁.loops ∧ Disjoint (I \ M₁.coloops) M₁.coloops
⊢ Disjoint (I \ M₁.coloops) (M₁.loops ∪ M₁.coloops)

Tactic:
rw [disjoint_union_right]

Premises used: Set.disjoint_union_right
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ Disjoint (I \ M₁.coloops) M₁.loops ∧ Disjoint (I \ M₁.coloops) M₁.coloops

Tactic:
⟨disjoint_of_subset_left diff_subset hdj, disjoint_sdiff_left⟩

Premises used: Set.diff_subset, Set.disjoint_of_subset_left, Set.disjoint_sdiff_left, And.intro
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I M₁.loops
⊢ Disjoint (I \ M₁.coloops) M₁.loops ∧ Disjoint (I \ M₁.coloops) M₁.coloops

Tactic:
exact ⟨disjoint_of_subset_left diff_subset hdj, disjoint_sdiff_left⟩
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
inr : ∀ (e : α) (heI : e ∈ I) (hel : M₁.IsLoop e), M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

Tactic:
obtain ⟨e, heI, hel : M₁.IsLoop e⟩ := not_disjoint_iff_nonempty_inter.mp hndj

Premises used: Set.not_disjoint_iff_nonempty_inter, Iff.mp
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₁.IsLoop e
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

Tactic:
iff_of_false (hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩) ?_

Premises used: iff_of_false, And.intro, Matroid.IsLoop.not_isColoop, Matroid.IsLoop.not_indep_of_mem
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₁.IsLoop e
inr : ¬M₂.Indep (I \ M₁.coloops)
⊢ M₁.Indep (I \ M₁.coloops) ↔ M₂.Indep (I \ M₁.coloops)

Tactic:
refine iff_of_false (hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩) ?_
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₁.IsLoop e
⊢ M₂.IsLoop e

Tactic:
rw [isLoop_iff, hl, ← isLoop_iff] at hel

Premises used: Matroid.isLoop_iff
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
inr : ¬M₂.Indep (I \ M₂.coloops)
⊢ ¬M₂.Indep (I \ M₁.coloops)

Tactic:
rw [hc]
-- Module: Mathlib.Combinatorics.Matroid.Loop
Goal:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.loops = M₂.loops
hc : M₁.coloops = M₂.coloops
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I M₁.loops
e : α
heI : e ∈ I
hel : M₂.IsLoop e
⊢ ¬M₂.Indep (I \ M₂.coloops)

Tactic:
hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩

Premises used: And.intro, Matroid.IsLoop.not_isColoop, Matroid.IsLoop.not_indep_of_mem