internlm/Lean-Github huggingface dataset:
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case M_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
ground_eq : M.E = (C.extension e).E \ {e}
⊢ (C.extension e).delete {e} = M
Tactic:
exact C.extension_delete he
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case ground_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
⊢ M.E = (C.extension e).E \ {e}
Tactic:
rw [(C.extension_ground), insert_diff_self_of_not_mem he]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
have Fsub : F ⊆ M.E
Proof state after:
case Fsub
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
⊢ F ⊆ M.E

case refine'_1.inr.inl
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
obtain ⟨I, hI⟩ := (C.extension e).exists_basis F (Fsub.trans (subset_insert _ _))
Proof state after:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
have hI' : M.Basis I F
Proof state after:
case hI'
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
⊢ M.Basis I F

case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
have F_flat : M.Flat F
Proof state after:
case F_flat
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
⊢ M.Flat F

case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
⊢ M.Flat F ∧ F ∉ C ∨ e ∈ F ∧ F \ {e} ∈ C
Tactic:
refine' Or.inl ⟨F_flat, fun F_mem ↦ e_not_mem _⟩
Proof state after:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
⊢ e ∈ F
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
⊢ e ∈ F
Tactic:
have e_nI := not_mem_subset hI.subset e_not_mem
Proof state after:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ e ∈ F
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ e ∈ F
Tactic:
rw [←(Flat.cl_eq_iff_basis_of_indep _ hI.indep).2 hI, hI.indep.mem_cl_iff, dep_iff,
(C.extension_indep e), not_or, insert_diff_self_of_not_mem e_nI, hI'.cl_eq_cl,
C.extension_ground, insert_subset_insert_iff e_nI, not_and_or]
Proof state after:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ (¬M.Indep (insert e I) ∧ (e ∉ insert e I \ M.E ∨ ¬(M.Indep I ∧ M.cl F ∉ C))) ∧ I ⊆ M.E ∨ e ∈ I

α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ (C.extension e).Flat F
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ (C.extension e).Flat F
Tactic:
rwa [flat_iff_cl_self]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case Fsub
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
⊢ F ⊆ M.E
Tactic:
rw [←diff_singleton_eq_self e_not_mem, diff_singleton_subset_iff, ←cl_eq_self, ←(C.extension_ground)]
Proof state after:
case Fsub
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
⊢ (C.extension e).cl F ⊆ (C.extension e).E
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case Fsub
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
⊢ (C.extension e).cl F ⊆ (C.extension e).E
Tactic:
exact cl_subset_ground _ _
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case hI'
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
⊢ M.Basis I F
Tactic:
sorry
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case F_flat
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
⊢ M.Flat F
Tactic:
rw [flat_iff_cl_self, ←M_eq, restrict_cl_eq _ Fsub (by simp)]
Proof state after:
case F_flat
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
⊢ (C.extension e).cl F ∩ M.E = F
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
⊢ M.E ⊆ (C.extension e).E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case F_flat
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
⊢ (C.extension e).cl F ∩ M.E = F
Tactic:
rw [cl_eq_self, inter_eq_self_of_subset_left Fsub]
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ (¬M.Indep (insert e I) ∧ (e ∉ insert e I \ M.E ∨ ¬(M.Indep I ∧ M.cl F ∉ C))) ∧ I ⊆ M.E ∨ e ∈ I
Tactic:
refine' Or.inl ⟨⟨fun eI_ind ↦ he (eI_ind.subset_ground (mem_insert _ _)), _⟩,
hI'.left_subset_ground⟩
Proof state after:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ e ∉ insert e I \ M.E ∨ ¬(M.Indep I ∧ M.cl F ∉ C)
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ e ∉ insert e I \ M.E ∨ ¬(M.Indep I ∧ M.cl F ∉ C)
Tactic:
rw [flat_iff_cl_self.1 F_flat, not_and_or, not_not]
Proof state after:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ e ∉ insert e I \ M.E ∨ ¬M.Indep I ∨ F ∈ C
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case refine'_1.inr.inl.intro
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem✝ : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
e_not_mem : e ∉ F
Fsub : F ⊆ M.E
I : Set α
hI : (C.extension e).Basis I F
hI' : M.Basis I F
F_flat : M.Flat F
F_mem : F ∈ C
e_nI : e ∉ I
⊢ e ∉ insert e I \ M.E ∨ ¬M.Indep I ∨ F ∈ C
Tactic:
exact Or.inr (Or.inr F_mem)
Proof state after:
no goals
Theorem: Matroid.ModularCut.extension_flat_iff
Proof state before:
case e_nF
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
f_not_mem : F \ {e} ∉ C
⊢ e ∉ F
Tactic:
intro e_F
Proof state after:
case e_nF
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
M_eq : C.extension e ↾ M.E = M
f_not_mem : F \ {e} ∉ C
e_F : e ∈ F
⊢ False
Theorem: Matroid.parallel_iff
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Parallel e f ↔ M.Nonloop e ∧ M.Nonloop f ∧ M.cl {e} = M.cl {f}
Tactic:
simp [Parallel, parallelClasses, and_comm (a := _ ∈ M.E), nonloop_iff_mem_compl_loops]
Proof state after:
no goals
Theorem: Matroid.Nonloop.parallel_iff_cl_eq_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
⊢ M.Parallel e f ↔ M.cl {e} = M.cl {f}
Tactic:
rw [Parallel, parallelClasses, Partition.rel_congr,
  (M.cl_flat ∅).rel_covByPartition_iff' ⟨he.mem_ground, he.not_loop⟩]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
⊢ M.cl (insert e (M.cl ∅)) = M.cl (insert f (M.cl ∅)) ↔ M.cl {e} = M.cl {f}
Theorem: Matroid.Nonloop.parallel_iff_cl_eq_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
⊢ M.cl (insert e (M.cl ∅)) = M.cl (insert f (M.cl ∅)) ↔ M.cl {e} = M.cl {f}
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Parallel.mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
⊢ e ∈ M.cl {f}
Tactic:
rw [← h.cl_eq_cl]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
⊢ e ∈ M.cl {e}
Theorem: Matroid.Parallel.mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
⊢ e ∈ M.cl {e}
Tactic:
exact mem_cl_of_mem' _ rfl
Proof state after:
no goals
Theorem: Matroid.setOf_parallel_eq_cl_diff_loops
Proof state before:
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅
Tactic:
by_cases he : M.Nonloop e
Proof state after:
case pos
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅

case neg
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : ¬M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅
Theorem: Matroid.setOf_parallel_eq_cl_diff_loops
Proof state before:
case neg
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : ¬M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅
Tactic:
rw [not_nonloop_iff_cl.1 he, diff_self, eq_empty_iff_forall_not_mem]
Proof state after:
case neg
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : ¬M.Nonloop e
⊢ ∀ (x : α), x ∉ {f | M.Parallel e f}
Theorem: Matroid.setOf_parallel_eq_cl_diff_loops
Proof state before:
case neg
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : ¬M.Nonloop e
⊢ ∀ (x : α), x ∉ {f | M.Parallel e f}
Tactic:
exact fun f hf ↦ he (Parallel.nonloop_left hf)
Proof state after:
no goals
Theorem: Matroid.setOf_parallel_eq_cl_diff_loops
Proof state before:
case pos
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅
Tactic:
rw [Parallel, parallelClasses, Partition.rel_congr,
  Partition.setOf_rel_eq_partOf, (M.cl_flat ∅).partOf_covByPartition_eq,
  cl_insert_cl_eq_cl_insert, insert_emptyc_eq]
Proof state after:
no goals
Theorem: Matroid.cl_eq_parallel_class_union_loops
Proof state before:
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
⊢ M.cl {e} = {f | M.Parallel e f} ∪ M.cl ∅
Tactic:
rw [setOf_parallel_eq_cl_diff_loops, diff_union_self,
  union_eq_self_of_subset_right (M.cl_mono (empty_subset _))]
Proof state after:
no goals
Theorem: Matroid.Nonloop.parallel_iff_mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
⊢ M.Parallel e f ↔ e ∈ M.cl {f}
Tactic:
refine ⟨Parallel.mem_cl, fun h ↦ ?_⟩
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
h : e ∈ M.cl {f}
⊢ M.Parallel e f
Theorem: Matroid.Nonloop.parallel_iff_mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
h : e ∈ M.cl {f}
⊢ M.Parallel e f
Tactic:
rw [cl_eq_parallel_class_union_loops, mem_union,  mem_setOf_eq, parallel_comm] at h
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
h : M.Parallel e f ∨ e ∈ M.cl ∅
⊢ M.Parallel e f
Theorem: Matroid.Nonloop.parallel_iff_mem_cl
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
h : M.Parallel e f ∨ e ∈ M.cl ∅
⊢ M.Parallel e f
Tactic:
exact h.elim id (fun h' ↦ (he.not_loop h').elim)
Proof state after:
no goals
Theorem: Matroid.Loopless.parallel_class_eq_cl
Proof state before:
α : Type u_1
M N : Matroid α
e✝ f g : α
I X P D : Set α
h : M.Loopless
e : α
⊢ {f | M.Parallel e f} = M.cl {e}
Tactic:
rw [setOf_parallel_eq_cl_diff_loops, h.cl_empty, diff_empty]
Proof state after:
no goals
Theorem: Matroid.Parallel.dep_of_ne
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hne : e ≠ f
⊢ M.Dep {e, f}
Tactic:
rw [pair_comm, ← h.nonloop_left.indep.mem_cl_iff_of_not_mem hne.symm]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hne : e ≠ f
⊢ f ∈ M.cl {e}
Theorem: Matroid.Parallel.dep_of_ne
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hne : e ≠ f
⊢ f ∈ M.cl {e}
Tactic:
exact h.symm.mem_cl
Proof state after:
no goals
Theorem: Matroid.parallel_iff_circuit
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
⊢ M.Parallel e f ↔ M.Circuit {e, f}
Tactic:
refine' ⟨fun h ↦ circuit_iff_dep_forall_diff_singleton_indep.2 ⟨h.dep_of_ne hef,_⟩, fun h ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Parallel e f
⊢ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})

case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.Parallel e f
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.Parallel e f
Tactic:
rw [Nonloop.parallel_iff_mem_cl]
Proof state after:
case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ e ∈ M.cl {f}

case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.Nonloop e
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case refine'_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.Nonloop e
Tactic:
apply h.nonloop_of_mem_of_one_lt_card _ (mem_insert _ _)
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ 1 < {e, f}.encard
Theorem: Matroid.parallel_iff_circuit
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ 1 < {e, f}.encard
Tactic:
rw [encard_pair hef]
Proof state after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ 1 < 2
Theorem: Matroid.parallel_iff_circuit
Proof state before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Circuit {e, f}
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case refine'_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : e ≠ f
h : M.Parallel e f
⊢ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Tactic:
rintro x (rfl | rfl)
Proof state after:
case refine'_1.inl
α : Type u_1
M N : Matroid α
f g : α
I X P D : Set α
x : α
hef : x ≠ f
h : M.Parallel x f
⊢ M.Indep ({x, f} \ {x})

case refine'_1.inr
α : Type u_1
M N : Matroid α
e g : α
I X P D : Set α
x : α
hef : e ≠ x
h : M.Parallel e x
⊢ M.Indep ({e, x} \ {x})
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case refine'_1.inl
α : Type u_1
M N : Matroid α
f g : α
I X P D : Set α
x : α
hef : x ≠ f
h : M.Parallel x f
⊢ M.Indep ({x, f} \ {x})
Tactic:
rw [pair_diff_left hef]
Proof state after:
case refine'_1.inl
α : Type u_1
M N : Matroid α
f g : α
I X P D : Set α
x : α
hef : x ≠ f
h : M.Parallel x f
⊢ M.Indep {f}
Theorem: Matroid.parallel_iff_circuit
Proof state before:
case refine'_1.inl
α : Type u_1
M N : Matroid α
f g : α
I X P D : Set α
x : α
hef : x ≠ f
h : M.Parallel x f
⊢ M.Indep {f}
Tactic:
exact h.nonloop_right.indep
Proof state after:
no goals