internlm/Lean-Github huggingface dataset:
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
case intro.refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M.Skew X Y
J : Set α
hJ : J ⊆ Y
⊢ M.Indep (J ∪ I) ∧ Disjoint X J ↔ M.Indep J
Tactic:
refine ⟨fun h ↦ h.1.subset subset_union_left,
  fun hJi ↦ ⟨?_, h.disjoint_of_indep_subset_right hJi hJ⟩⟩
Proof state after:
case intro.refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M.Skew X Y
J : Set α
hJ : J ⊆ Y
hJi : M.Indep J
⊢ M.Indep (J ∪ I)
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
case intro.refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M.Skew X Y
J : Set α
hJ : J ⊆ Y
hJi : M.Indep J
⊢ M.Indep (J ∪ I)
Tactic:
exact h.symm.union_indep_of_indep_subsets hJi hJ hI.indep hI.subset
Proof state after:
no goals
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
⊢ (M ↾ Y).Indep J
Tactic:
exact restrict_indep_iff.2 ⟨hJ.indep, hJ.subset⟩
Proof state after:
no goals
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
case intro.refine_2.intro.refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : (M ↾ Y).Indep J
⊢ M.Indep (I ∪ J)
Tactic:
rw [← h, restrict_indep_iff, hI.contract_eq_contract_delete, delete_indep_iff,
  hI.indep.contract_indep_iff, union_comm] at hi
Proof state after:
case intro.refine_2.intro.refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : ((Disjoint J I ∧ M.Indep (I ∪ J)) ∧ Disjoint J (X \ I)) ∧ J ⊆ Y
⊢ M.Indep (I ∪ J)
Theorem: Matroid.skew_iff_contract_restrict_eq_restrict
Proof state before:
case intro.refine_2.intro.refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
h : M ／ X ↾ Y = M ↾ Y
J : Set α
hJ : M.Basis J Y
hi : ((Disjoint J I ∧ M.Indep (I ∪ J)) ∧ Disjoint J (X \ I)) ∧ J ⊆ Y
⊢ M.Indep (I ∪ J)
Tactic:
exact hi.1.1.2
Proof state after:
no goals
Theorem: Matroid.empty_skew
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hX : X ⊆ M.E
⊢ M.Skew ∅ X
Tactic:
rw [skew_iff_contract_restrict_eq_restrict, contract_empty]
Proof state after:
no goals
Theorem: Matroid.SkewFamily.skew_compl
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
A : Set ι
⊢ M.Skew (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i)
Tactic:
rw [skew_iff_modularPair_inter_subset_loops]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
A : Set ι
⊢ M.ModularPair (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i) ∧ (⋃ i ∈ A, Xs i) ∩ ⋃ i ∈ Aᶜ, Xs i ⊆ M.cl ∅
Theorem: Matroid.SkewFamily.skew_compl
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
A : Set ι
⊢ M.ModularPair (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i) ∧ (⋃ i ∈ A, Xs i) ∩ ⋃ i ∈ Aᶜ, Xs i ⊆ M.cl ∅
Tactic:
refine ⟨h.modularFamily.modularPair_compl_biUnion A, ?_⟩
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
A : Set ι
⊢ (⋃ i ∈ A, Xs i) ∩ ⋃ i ∈ Aᶜ, Xs i ⊆ M.cl ∅
Theorem: Matroid.SkewFamily.skew_compl
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
h : M.SkewFamily Xs
A : Set ι
⊢ (⋃ i ∈ A, Xs i) ∩ ⋃ i ∈ Aᶜ, Xs i ⊆ M.cl ∅
Tactic:
rintro e ⟨⟨_,⟨i,hi,rfl⟩,hi'⟩ ,⟨_,⟨j,hj,rfl⟩,hj'⟩⟩
Proof state after:
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e✝ f : α
h : M.SkewFamily Xs
A : Set ι
e : α
i : ι
hi' : e ∈ (fun i => ⋃ (_ : i ∈ A), Xs i) i
j : ι
hj' : e ∈ (fun i => ⋃ (_ : i ∈ Aᶜ), Xs i) j
⊢ e ∈ M.cl ∅
Theorem: Matroid.SkewFamily.skew_compl
Proof state before:
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e✝ f : α
h : M.SkewFamily Xs
A : Set ι
e : α
i : ι
hi' : e ∈ (fun i => ⋃ (_ : i ∈ A), Xs i) i
j : ι
hj' : e ∈ (fun i => ⋃ (_ : i ∈ Aᶜ), Xs i) j
⊢ e ∈ M.cl ∅
Tactic:
simp only [mem_iUnion, exists_prop] at hi' hj'
Proof state after:
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e✝ f : α
h : M.SkewFamily Xs
A : Set ι
e : α
i j : ι
hi' : i ∈ A ∧ e ∈ Xs i
hj' : j ∈ Aᶜ ∧ e ∈ Xs j
⊢ e ∈ M.cl ∅
Theorem: Matroid.SkewFamily.skew_compl
Proof state before:
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e✝ f : α
h : M.SkewFamily Xs
A : Set ι
e : α
i j : ι
hi' : i ∈ A ∧ e ∈ Xs i
hj' : j ∈ Aᶜ ∧ e ∈ Xs j
⊢ e ∈ M.cl ∅
Tactic:
exact h.loop_of_mem_inter (show i ≠ j from fun hij ↦ hj'.1 <| hij ▸ hi'.1) ⟨hi'.2, hj'.2⟩
Proof state after:
no goals
Theorem: Matroid.SkewFamily.skew_compl_singleton
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
h : M.SkewFamily Xs
i : ι
⊢ M.Skew (Xs i) (⋃ j ∈ {i}ᶜ, Xs j)
Tactic:
convert h.skew_compl {i}
Proof state after:
case h.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
h : M.SkewFamily Xs
i : ι
⊢ Xs i = ⋃ i_1 ∈ {i}, Xs i_1
Theorem: Matroid.SkewFamily.skew_compl_singleton
Proof state before:
case h.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j : ι
e f : α
h : M.SkewFamily Xs
i : ι
⊢ Xs i = ⋃ i_1 ∈ {i}, Xs i_1
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.skew_iff_forall_circuit
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hdj : Disjoint X Y
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.Skew X Y ↔ ∀ (C : Set α), M.Circuit C → C ⊆ X ∪ Y → C ⊆ X ∨ C ⊆ Y
Tactic:
rw [Skew, skewFamily_iff_forall_circuit]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hdj : Disjoint X Y
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∀ (C : Set α), M.Circuit C → (C ⊆ ⋃ i, bif i then X else Y) → ∃ i, C ⊆ bif i then X else Y) ↔
    ∀ (C : Set α), M.Circuit C → C ⊆ X ∪ Y → C ⊆ X ∨ C ⊆ Y

case hXs
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hdj : Disjoint X Y
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ ∀ (i : Bool), (bif i then X else Y) ⊆ M.E

case hdj
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hdj : Disjoint X Y
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ Pairwise (Disjoint on fun i => bif i then X else Y)
Theorem: Matroid.skew_iff_forall_circuit
Proof state before:
case hdj
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hdj : Disjoint X Y
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ Pairwise (Disjoint on fun i => bif i then X else Y)
Tactic:
rwa [pairwise_disjoint_on_bool]
Proof state after:
no goals
Theorem: Matroid.skew_iff_forall_circuit
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hdj : Disjoint X Y
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∀ (C : Set α), M.Circuit C → (C ⊆ ⋃ i, bif i then X else Y) → ∃ i, C ⊆ bif i then X else Y) ↔
    ∀ (C : Set α), M.Circuit C → C ⊆ X ∪ Y → C ⊆ X ∨ C ⊆ Y
Tactic:
simp [← union_eq_iUnion, or_comm]
Proof state after:
no goals
Theorem: Matroid.skew_iff_forall_circuit
Proof state before:
case hXs
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hdj : Disjoint X Y
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ ∀ (i : Bool), (bif i then X else Y) ⊆ M.E
Tactic:
simp [hX, hY]
Proof state after:
no goals
Theorem: Matroid.skew_of_subset_loops
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
L : Set α
hL : L ⊆ M.cl ∅
hX : X ⊆ M.E
⊢ M.Skew L X
Tactic:
rw [skew_iff_diff_loops_skew_left, diff_eq_empty.2 hL]
Proof state after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
L : Set α
hL : L ⊆ M.cl ∅
hX : X ⊆ M.E
⊢ M.Skew ∅ X
Theorem: Matroid.skew_of_subset_loops
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
L : Set α
hL : L ⊆ M.cl ∅
hX : X ⊆ M.E
⊢ M.Skew ∅ X
Tactic:
apply empty_skew hX
Proof state after:
no goals
Theorem: Matroid.Loop.skew
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : M.Loop e
hX : X ⊆ M.E
⊢ {e} ⊆ M.cl ∅
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.skew_of_subset_coloops
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
K : Set α
hK : K ⊆ M✶.cl ∅
hX : X ⊆ M.E
hdj : Disjoint K X
⊢ M.Skew K X
Tactic:
rw [skew_iff_contract_restrict_eq_restrict, contract_eq_delete_of_subset_coloops hK,
  delete_eq_restrict, restrict_restrict_eq]
Proof state after:
case hR
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
K : Set α
hK : K ⊆ M✶.cl ∅
hX : X ⊆ M.E
hdj : Disjoint K X
⊢ X ⊆ M.E \ K
Theorem: Matroid.skew_of_subset_coloops
Proof state before:
case hR
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
K : Set α
hK : K ⊆ M✶.cl ∅
hX : X ⊆ M.E
hdj : Disjoint K X
⊢ X ⊆ M.E \ K
Tactic:
rwa [subset_diff, and_iff_left hdj.symm]
Proof state after:
no goals
Theorem: Matroid.Coloop.skew
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : M.Coloop e
hX : X ⊆ M.E
heX : e ∉ X
⊢ {e} ⊆ M✶.cl ∅
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Coloop.skew
Proof state before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
he : M.Coloop e
hX : X ⊆ M.E
heX : e ∉ X
⊢ Disjoint {e} X
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.ModularCut.iInter_mem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ ⋂ i, Fs i ∈ U
Tactic:
have hwin := U.sInter_mem (Fs := range Fs) (range_nonempty Fs) ?_ ?_
Proof state after:
case refine_3
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
hwin : ⋂₀ range Fs ∈ U
⊢ ⋂ i, Fs i ∈ U

case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ range Fs ⊆ ↑U

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ M.ModularFamily fun F => ↑F
Theorem: Matroid.ModularCut.iInter_mem
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ M.ModularFamily fun F => ↑F
Tactic:
obtain ⟨B, hB, hB'⟩ := hFs_mod
Proof state after:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
B : Set α
hB : M.Base B
hB' : ∀ (i : ι), M.Basis (Fs i ∩ B) (Fs i)
⊢ M.ModularFamily fun F => ↑F
Theorem: Matroid.ModularCut.iInter_mem
Proof state before:
case refine_2.intro.intro
α : Type u_1
M : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
B : Set α
hB : M.Base B
hB' : ∀ (i : ι), M.Basis (Fs i ∩ B) (Fs i)
⊢ M.ModularFamily fun F => ↑F
Tactic:
exact ⟨B, hB, by simpa⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.iInter_mem
Proof state before:
case refine_3
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
hwin : ⋂₀ range Fs ∈ U
⊢ ⋂ i, Fs i ∈ U
Tactic:
simpa using hwin
Proof state after:
no goals
Theorem: Matroid.ModularCut.iInter_mem
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
⊢ range Fs ⊆ ↑U
Tactic:
rintro _ ⟨i, hi, rfl⟩
Proof state after:
case refine_1.intro.refl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
i : ι
⊢ Fs i ∈ ↑U
Theorem: Matroid.ModularCut.iInter_mem
Proof state before:
case refine_1.intro.refl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
hFs_mod : M.ModularFamily Fs
i : ι
⊢ Fs i ∈ ↑U
Tactic:
exact hFs i
Proof state after:
no goals
Theorem: Matroid.ModularCut.iInter_mem
Proof state before:
α : Type u_1
M : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
ι : Type u_2
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), Fs i ∈ U
B : Set α
hB : M.Base B
hB' : ∀ (i : ι), M.Basis (Fs i ∩ B) (Fs i)
⊢ ∀ (i : ↑(range Fs)), M.Basis ((fun F => ↑F) i ∩ B) ((fun F => ↑F) i)
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.ModularCut.inter_mem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ F ∩ F' ∈ U
Tactic:
rw [inter_eq_iInter]
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ (⋂ b, bif b then F else F') ∈ U
Theorem: Matroid.ModularCut.inter_mem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ (⋂ b, bif b then F else F') ∈ U
Tactic:
apply U.iInter_mem
Proof state after:
case hFs
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ ∀ (i : Bool), (bif i then F else F') ∈ U

case hFs_mod
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ M.ModularFamily fun i => bif i then F else F'
Theorem: Matroid.ModularCut.inter_mem
Proof state before:
case hFs_mod
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ M.ModularFamily fun i => bif i then F else F'
Tactic:
exact h
Proof state after:
no goals
Theorem: Matroid.ModularCut.inter_mem
Proof state before:
case hFs
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hF : F ∈ U
hF' : F' ∈ U
h : M.ModularPair F F'
⊢ ∀ (i : Bool), (bif i then F else F') ∈ U
Tactic:
simp [hF, hF']
Proof state after:
no goals
Theorem: Matroid.ModularCut.cl_mem_of_mem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hF : F ∈ U
⊢ M.cl F ∈ U
Tactic:
rwa [(U.flat_of_mem hF).cl]
Proof state after:
no goals
Theorem: Matroid.ModularCut.eq_bot_or_ground_mem
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
⊢ U = ⊥ ∨ M.E ∈ U
Tactic:
obtain (hU | ⟨F, hF⟩) := (U : Set (Set α)).eq_empty_or_nonempty
Proof state after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥ ∨ M.E ∈ U

case inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ U : M.ModularCut
F : Set α
hF : F ∈ ↑U
⊢ U = ⊥ ∨ M.E ∈ U
Theorem: Matroid.ModularCut.eq_bot_or_ground_mem
Proof state before:
case inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ U : M.ModularCut
F : Set α
hF : F ∈ ↑U
⊢ U = ⊥ ∨ M.E ∈ U
Tactic:
exact .inr <| U.superset_mem hF M.ground_flat (U.flat_of_mem hF).subset_ground
Proof state after:
no goals
Theorem: Matroid.ModularCut.eq_bot_or_ground_mem
Proof state before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥ ∨ M.E ∈ U
Tactic:
left
Proof state after:
case inl.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥
Theorem: Matroid.ModularCut.eq_bot_or_ground_mem
Proof state before:
case inl.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥
Tactic:
ext x
Proof state after:
case inl.h.carrier.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
x : Set α
⊢ x ∈ U.carrier ↔ x ∈ ⊥.carrier
Theorem: Matroid.ModularCut.eq_bot_or_ground_mem
Proof state before:
case inl.h.carrier.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
x : Set α
⊢ x ∈ U.carrier ↔ x ∈ ⊥.carrier
Tactic:
change x ∈ (U : Set (Set α)) ↔ x ∈ ∅
Proof state after:
case inl.h.carrier.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
x : Set α
⊢ x ∈ ↑U ↔ x ∈ ∅
Theorem: Matroid.ModularCut.eq_bot_or_ground_mem
Proof state before:
case inl.h.carrier.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
x : Set α
⊢ x ∈ ↑U ↔ x ∈ ∅
Tactic:
simp [hU]
Proof state after:
no goals
Theorem: Matroid.ModularCut.eq_top_iff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ U = ⊤ ↔ M.cl ∅ ∈ U
Tactic:
refine ⟨?_, fun h ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ U = ⊤ → M.cl ∅ ∈ U

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ U = ⊤
Theorem: Matroid.ModularCut.eq_top_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ U = ⊤
Tactic:
simp only [SetLike.ext_iff, mem_top_iff]
Proof state after:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ ∀ (x : Set α), x ∈ U ↔ M.Flat x
Theorem: Matroid.ModularCut.eq_top_iff
Proof state before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ ∀ (x : Set α), x ∈ U ↔ M.Flat x
Tactic:
refine fun F ↦ ⟨U.flat_of_mem, fun h' ↦ U.superset_mem h h' h'.loops_subset⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.eq_top_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ U = ⊤ → M.cl ∅ ∈ U
Tactic:
rintro rfl
Proof state after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
⊢ M.cl ∅ ∈ ⊤
Theorem: Matroid.ModularCut.eq_top_iff
Proof state before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
⊢ M.cl ∅ ∈ ⊤
Tactic:
exact ⟨M.cl_flat ∅, empty_subset _⟩
Proof state after:
no goals
Theorem: Matroid.top_ne_bot
Proof state before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
⊢ ⊤ ≠ ⊥
Tactic:
rw [Ne, eq_comm, ModularCut.eq_top_iff]
Proof state after:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
⊢ M.cl ∅ ∉ ⊥
Theorem: Matroid.top_ne_bot
Proof state before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
⊢ M.cl ∅ ∉ ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.principal_ground_ne_top
Proof state before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
⊢ ModularCut.principal M M.E ≠ ⊤
Tactic:
simp only [Ne, ModularCut.eq_top_iff, ModularCut.mem_principal_iff, cl_flat, true_and]
Proof state after:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
⊢ ¬M.E ⊆ M.cl ∅
Theorem: Matroid.principal_ground_ne_top
Proof state before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
⊢ ¬M.E ⊆ M.cl ∅
Tactic:
obtain ⟨B, hB⟩ := M.exists_base
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
⊢ ¬M.E ⊆ M.cl ∅
Theorem: Matroid.principal_ground_ne_top
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
⊢ ¬M.E ⊆ M.cl ∅
Tactic:
obtain ⟨e, heB⟩ := hB.nonempty
Proof state after:
case intro.intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e✝ f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
e : α
heB : e ∈ B
⊢ ¬M.E ⊆ M.cl ∅
Theorem: Matroid.principal_ground_ne_top
Proof state before:
case intro.intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e✝ f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
e : α
heB : e ∈ B
⊢ ¬M.E ⊆ M.cl ∅
Tactic:
exact fun h ↦ (hB.indep.nonloop_of_mem heB).not_loop <| h (hB.subset_ground heB)
Proof state after:
no goals
Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff
Proof state before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
⊢ M.cl J ∈ U
Tactic:
set Is : ↑(I \ J) → Set α := fun e ↦ I \ {e.1} with hIs
Proof state after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
⊢ M.cl J ∈ U