internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
heCl : e ∈ M.cl I
⊢ False
Tactic:
simp only [heCl, insert_eq_of_mem, cl_flat, not_true_eq_false, imp_false] at h
Proof state after:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
heCl : e ∈ M.cl I
h : e ∉ M.cl (M.cl I \ {e})
⊢ False
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
heCl : e ∈ M.cl I
h : e ∉ M.cl (M.cl I \ {e})
⊢ False
Tactic:
exact h <| (M.cl_subset_cl <| subset_diff_singleton (M.subset_cl I hIi.subset_ground) heI') heCl
Proof state after:
no goals
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
⊢ M.E = ((M ＼ e).extendBy e (ofDeleteElem M e)).E
Tactic:
simp [he]
Proof state after:
no goals
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ I = insert e (I \ {e})
Tactic:
simp [heI]
Proof state after:
no goals
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ e ∉ I \ {e}
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
this : M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
⊢ M.Indep (insert e I) ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep (insert e I)
Tactic:
simpa [extIndep_iff_of_mem heI, heI']
Proof state after:
no goals
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ False
Tactic:
suffices e ∈ M.cl (M.cl I) from h.not_mem_cl_diff_of_mem (.inl rfl) <| by simpa [heI']
Proof state after:
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ e ∈ M.cl (M.cl I)
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ e ∈ M.cl (M.cl I)
Tactic:
exact (M.cl_subset_cl diff_subset) he
Proof state after:
no goals
Theorem: Matroid.ModularCut.deleteElem_extendBy
Proof state before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
this : e ∈ M.cl (M.cl I)
⊢ e ∈ M.cl (insert e I \ {e})
Tactic:
simpa [heI']
Proof state after:
no goals
Theorem: Matroid.ModularCut.extendBy_deleteElem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
⊢ M.extendBy e U ＼ e = M
Tactic:
refine eq_of_indep_iff_indep_forall (by simpa) fun I hI ↦ ?_
Proof state after:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I
Theorem: Matroid.ModularCut.extendBy_deleteElem
Proof state before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I
Tactic:
obtain ⟨-, heI⟩ := show I ⊆ M.E ∧ e ∉ I by simpa [subset_diff] using hI
Proof state after:
case intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
heI : e ∉ I
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I
Theorem: Matroid.ModularCut.extendBy_deleteElem
Proof state before:
case intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
heI : e ∉ I
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I
Tactic:
simp [deleteElem, extIndep_iff_of_not_mem heI, heI]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extendBy_deleteElem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
⊢ (M.extendBy e U ＼ e).E = M.E
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.ModularCut.extendBy_deleteElem
Proof state before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
⊢ I ⊆ M.E ∧ e ∉ I
Tactic:
simpa [subset_diff] using hI
Proof state after:
no goals
Theorem: Matroid.extendBy_injective
Proof state before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
⊢ Injective (M.extendBy e)
Tactic:
refine fun U U' h_eq ↦ SetLike.coe_set_eq.1 (Set.ext fun F ↦ ?_)
Proof state after:
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Theorem: Matroid.extendBy_injective
Proof state before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
obtain (hF | hF) := em' (M.Flat F)
Proof state after:
case inl
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : ¬M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'

case inr
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Theorem: Matroid.extendBy_injective
Proof state before:
case inr
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis F
Proof state after:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Theorem: Matroid.extendBy_injective
Proof state before:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
have heI : e ∉ I := not_mem_subset hI.indep.subset_ground he
Proof state after:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
heI : e ∉ I
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Theorem: Matroid.extendBy_injective
Proof state before:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
heI : e ∉ I
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
apply_fun (fun M ↦ M.Indep (insert e I)) at h_eq
Proof state after:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
heI : e ∉ I
h_eq : (M.extendBy e U).Indep (insert e I) = (M.extendBy e U').Indep (insert e I)
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Theorem: Matroid.extendBy_injective
Proof state before:
case inr.intro
α : Type u_1
M✝ : Matroid α
I✝ J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
F : Set α
hF : M.Flat F
I : Set α
hI : M.Basis I F
heI : e ∉ I
h_eq : (M.extendBy e U).Indep (insert e I) = (M.extendBy e U').Indep (insert e I)
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
simpa [extendBy_Indep, ModularCut.extIndep_iff_of_mem (mem_insert e I), heI, hI.indep,
  not_iff_not, ← hF.eq_cl_of_basis hI] using h_eq
Proof state after:
no goals
Theorem: Matroid.extendBy_injective
Proof state before:
case inl
α : Type u_1
M✝ : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ : M✝.ModularCut
M : Matroid α
he : e ∉ M.E
U U' : M.ModularCut
h_eq : M.extendBy e U = M.extendBy e U'
F : Set α
hF : ¬M.Flat F
⊢ F ∈ ↑U ↔ F ∈ ↑U'
Tactic:
exact iff_of_false (hF ∘ U.flat_of_mem) (hF ∘ U'.flat_of_mem)
Proof state after:
no goals
Theorem: Matroid.projectBy_indep_iff_of_ne_top
Proof state before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
I : Set α
hU : U ≠ ⊤
⊢ (M.projectBy U).Indep I ↔ M.Indep I ∧ M.cl I ∉ U
Tactic:
simp [hU]
Proof state after:
no goals
Theorem: Matroid.projectBy_top
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ M.projectBy ⊤ = M
Tactic:
simp [eq_iff_indep_iff_indep_forall]
Proof state after:
no goals
Theorem: Matroid.addLoop_eq_self
Proof state before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∈ M.E
⊢ M.addLoop e = M
Tactic:
rw [addLoop, insert_eq_of_mem he, restrict_ground_eq_self]
Proof state after:
no goals
Theorem: Matroid.addLoop_indep_iff
Proof state before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
⊢ (M.addLoop f).Indep I ↔ M.Indep I
Tactic:
simp only [addLoop, restrict_indep_iff, and_iff_left_iff_imp]
Proof state after:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
⊢ M.Indep I → I ⊆ insert f M.E
Theorem: Matroid.addLoop_indep_iff
Proof state before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
⊢ M.Indep I → I ⊆ insert f M.E
Tactic:
exact fun hI ↦ hI.subset_ground.trans (subset_insert _ _)
Proof state after:
no goals
Theorem: Matroid.eq_addLoop_iff
Proof state before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
Tactic:
obtain (he' | he') := em' (e ∈ M'.E)
Proof state after:
case inl
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M

case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
Tactic:
simp_rw [deleteElem, eq_iff_indep_iff_indep_forall, addLoop_ground, addLoop_indep_iff,
  delete_ground, delete_indep_iff, disjoint_singleton_right, ← singleton_dep, dep_iff,
  singleton_subset_iff, and_iff_left he', subset_diff, disjoint_singleton_right, and_imp]
Proof state after:
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ (M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I) ↔
    ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
⊢ (M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I) ↔
    ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
Tactic:
refine ⟨fun ⟨hE, hi⟩ ↦ ⟨?_, ?_, ?_⟩, fun ⟨hi, hE, h⟩ ↦ ⟨?_, fun I hIss ↦ ?_⟩⟩
Proof state after:
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M'.Indep {e}

case inr.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ M'.E \ {e} = M.E

case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)

case inr.refine_4
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.E = insert e M.E

case inr.refine_5
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
⊢ M'.Indep I ↔ M.Indep I
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_5
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
⊢ M'.Indep I ↔ M.Indep I
Tactic:
obtain (heI | heI) := em (e ∈ I)
Proof state after:
case inr.refine_5.inl
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
heI : e ∈ I
⊢ M'.Indep I ↔ M.Indep I

case inr.refine_5.inr
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
⊢ M'.Indep I ↔ M.Indep I
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_5.inr
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
⊢ M'.Indep I ↔ M.Indep I
Tactic:
specialize h I hIss
Proof state after:
case inr.refine_5.inr
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
h : e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.Indep I ↔ M.Indep I
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_5.inr
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
h : e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.Indep I ↔ M.Indep I
Tactic:
simpa [heI] using h
Proof state after:
no goals
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inl
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ M' = M.addLoop e ↔ M'.Loop e ∧ M' ＼ e = M
Tactic:
refine iff_of_false ?_ ?_
Proof state after:
case inl.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬M' = M.addLoop e

case inl.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬(M'.Loop e ∧ M' ＼ e = M)
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inl.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬(M'.Loop e ∧ M' ＼ e = M)
Tactic:
rintro ⟨h, rfl⟩
Proof state after:
case inl.refine_2.intro
α : Type u_1
M' : Matroid α
e f : α
I : Set α
he' : e ∉ M'.E
h : M'.Loop e
he : e ∉ (M' ＼ e).E
⊢ False
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inl.refine_2.intro
α : Type u_1
M' : Matroid α
e f : α
I : Set α
he' : e ∉ M'.E
h : M'.Loop e
he : e ∉ (M' ＼ e).E
⊢ False
Tactic:
exact he' h.mem_ground
Proof state after:
no goals
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inl.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ M'.E
⊢ ¬M' = M.addLoop e
Tactic:
rintro rfl
Proof state after:
case inl.refine_1
α : Type u_1
M : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ (M.addLoop e).E
⊢ False
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inl.refine_1
α : Type u_1
M : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∉ (M.addLoop e).E
⊢ False
Tactic:
simp at he'
Proof state after:
no goals
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M'.Indep {e}
Tactic:
rw [hi _ (singleton_subset_iff.2 he')]
Proof state after:
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M.Indep {e}
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_1
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ¬M.Indep {e}
Tactic:
exact fun hei ↦ he (singleton_subset_iff.1 hei.subset_ground)
Proof state after:
no goals
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_2
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ M'.E \ {e} = M.E
Tactic:
simp [hE, he]
Proof state after:
no goals
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
⊢ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
Tactic:
rintro I hIss heI
Proof state after:
case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
⊢ M'.Indep I ∧ e ∉ I ↔ M.Indep I
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_3
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : M'.E = insert e M.E ∧ ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
hE : M'.E = insert e M.E
hi : ∀ I ⊆ M'.E, M'.Indep I ↔ M.Indep I
I : Set α
hIss : I ⊆ M'.E
heI : e ∉ I
⊢ M'.Indep I ∧ e ∉ I ↔ M.Indep I
Tactic:
rw [and_iff_left heI, hi _ hIss]
Proof state after:
no goals
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_4
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
⊢ M'.E = insert e M.E
Tactic:
rw [← hE, insert_diff_singleton, insert_eq_of_mem he']
Proof state after:
no goals
Theorem: Matroid.eq_addLoop_iff
Proof state before:
case inr.refine_5.inl
α : Type u_1
M M' : Matroid α
e f : α
I✝ : Set α
he : e ∉ M.E
he' : e ∈ M'.E
x✝ : ¬M'.Indep {e} ∧ M'.E \ {e} = M.E ∧ ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
hi : ¬M'.Indep {e}
hE : M'.E \ {e} = M.E
h : ∀ I ⊆ M'.E, e ∉ I → (M'.Indep I ∧ e ∉ I ↔ M.Indep I)
I : Set α
hIss : I ⊆ M'.E
heI : e ∈ I
⊢ M'.Indep I ↔ M.Indep I
Tactic:
exact iff_of_false (fun hI ↦ hi <| hI.subset (singleton_subset_iff.2 heI))
  (fun hI ↦ he <| hI.subset_ground heI)
Proof state after:
no goals
Theorem: Matroid.addLoop_loop
Proof state before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ (M.addLoop e).Loop e
Tactic:
rw [addLoop, ← singleton_dep, Dep, singleton_subset_iff, restrict_indep_iff,
  singleton_subset_iff, restrict_ground_eq, and_iff_left (mem_insert _ _),
  and_iff_left (mem_insert _ _)]
Proof state after:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ ¬M.Indep {e}
Theorem: Matroid.addLoop_loop
Proof state before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ ¬M.Indep {e}
Tactic:
exact fun hi ↦ he (singleton_subset_iff.1 hi.subset_ground)
Proof state after:
no goals
Theorem: Matroid.addColoop_eq_self
Proof state before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∈ M.E
⊢ M.addColoop e = M
Tactic:
rwa [addColoop, addLoop_eq_self, dual_dual]
Proof state after:
no goals
Theorem: Matroid.eq_addColoop_iff
Proof state before:
α : Type u_1
M M' : Matroid α
e f : α
I : Set α
he : e ∉ M.E
⊢ M' = M.addColoop e ↔ M'.Coloop e ∧ M' ／ e = M
Tactic:
rw [addColoop, eq_dual_comm, eq_comm, eq_addLoop_iff (show e ∉ M✶.E from he),
  dual_loop_iff_coloop, eq_dual_comm, deleteElem, dual_delete_dual_eq_contract, contract_elem,
  eq_comm]
Proof state after:
no goals
Theorem: Matroid.parallelExtend_self
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f x : α
I C : Set α
M : Matroid α
e : α
⊢ M.parallelExtend e e = M.addLoop e
Tactic:
change comap _ (update id e (id e)) ↾ _ = _
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f x : α
I C : Set α
M : Matroid α
e : α
⊢ M.comap (update id e (id e)) ↾ insert e M.E = M.addLoop e
Theorem: Matroid.parallelExtend_self
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
M✝ M' : Matroid α
e✝ f x : α
I C : Set α
M : Matroid α
e : α
⊢ M.comap (update id e (id e)) ↾ insert e M.E = M.addLoop e
Tactic:
rw [update_eq_self, comap_id, addLoop]
Proof state after:
no goals