internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Basis.exchange_base_of_indep
Proof state before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
⊢ M.Basis (insert f (B \ {e})) X
Tactic:
have X_sub := hB.subset_ground
Proof state after:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ M.Basis (insert f (B \ {e})) X
Theorem: Matroid.Basis.exchange_base_of_indep
Proof state before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : M.Basis B X
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ M.Basis (insert f (B \ {e})) X
Tactic:
rw [← base_restrict_iff] at hB ⊢
Proof state after:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : (M ↾ X).Base B
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ (M ↾ X).Base (insert f (B \ {e}))
Theorem: Matroid.Basis.exchange_base_of_indep
Proof state before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
f e : α
X : Set α
hB : (M ↾ X).Base B
hf : f ∈ X \ B
hI : M.Indep (insert f (B \ {e}))
X_sub : X ⊆ M.E
⊢ (M ↾ X).Base (insert f (B \ {e}))
Tactic:
apply hB.exchange_base_of_indep hf.2 (hI.indep_restrict_of_subset (insert_subset hf.1
(diff_subset.trans hB.subset_ground)))
Proof state after:
no goals
Theorem: Matroid.ModularFamily.subset
Proof state before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Y : Set (Set α)
hmod : M.ModularFamily fun x => ↑x
hsub : Y ⊆ X
⊢ M.ModularFamily fun y => ↑y
Tactic:
obtain ⟨B, hB⟩ := hmod
Proof state after:
case intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Y : Set (Set α)
hsub : Y ⊆ X
B : Set α
hB : M.ModularBase B fun x => ↑x
⊢ M.ModularFamily fun y => ↑y
Theorem: Matroid.ModularFamily.subset
Proof state before:
case intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Y : Set (Set α)
hsub : Y ⊆ X
B : Set α
hB : M.ModularBase B fun x => ↑x
⊢ M.ModularFamily fun y => ↑y
Tactic:
refine' ⟨B, hB.subset hsub⟩
Proof state after:
no goals
Theorem: Matroid.modular_finite_intersection
Proof state before:
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
⊢ ⋂₀ X ∈ Fs
Tactic:
obtain (⟨x, rfl⟩ | X_nt) := hnone.exists_eq_singleton_or_nontrivial
Proof state after:
case inl.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
x : Set α
hfin : {x}.Finite
hsub : {x} ⊆ Fs
hmod : M.ModularFamily fun x_1 => ↑x_1
hnone : {x}.Nonempty
⊢ ⋂₀ {x} ∈ Fs

case inr
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
⊢ ⋂₀ X ∈ Fs
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
⊢ ⋂₀ X ∈ Fs
Tactic:
obtain ⟨x, y, xy_ne, xy_sub⟩ := nontrivial_iff_pair_subset.1 X_nt
Proof state after:
case inr.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ ⋂₀ X ∈ Fs
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ ⋂₀ X ∈ Fs
Tactic:
have x_eq_insert : X = insert x (X \ {x})
Proof state after:
case x_eq_insert
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ X = insert x (X \ {x})

case inr.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ ⋂₀ X ∈ Fs
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ ⋂₀ X ∈ Fs
Tactic:
rw [x_eq_insert, sInter_insert]
Proof state after:
case inr.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ x ∩ ⋂₀ (X \ {x}) ∈ Fs
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
⊢ x ∩ ⋂₀ (X \ {x}) ∈ Fs
Tactic:
obtain ⟨B, B_mod⟩ := hmod
Proof state after:
case inr.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ x ∩ ⋂₀ (X \ {x}) ∈ Fs
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ x ∩ ⋂₀ (X \ {x}) ∈ Fs
Tactic:
apply pair_modular (hsub (xy_sub (mem_insert _ _))) _
Proof state after:
case inr.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.ModularPair x (⋂₀ (X \ {x}))

α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ ⋂₀ (X \ {x}) ∈ Fs
Theorem: Matroid.modular_finite_intersection
Proof state before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ ⋂₀ (X \ {x}) ∈ Fs
Tactic:
have encard_lt : (X \ {x}).encard < X.encard
Proof state after:
case encard_lt
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ (X \ {x}).encard < X.encard

α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
encard_lt : (X \ {x}).encard < X.encard
⊢ ⋂₀ (X \ {x}) ∈ Fs
Theorem: Matroid.modular_finite_intersection
Proof state before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
encard_lt : (X \ {x}).encard < X.encard
⊢ ⋂₀ (X \ {x}) ∈ Fs
Tactic:
have:= encard_lt
Proof state after:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
encard_lt this : (X \ {x}).encard < X.encard
⊢ ⋂₀ (X \ {x}) ∈ Fs
Theorem: Matroid.modular_finite_intersection
Proof state before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
encard_lt this : (X \ {x}).encard < X.encard
⊢ ⋂₀ (X \ {x}) ∈ Fs
Tactic:
apply modular_finite_intersection forall_flat pair_modular (hfin.subset diff_subset) (diff_subset.trans
 hsub) (ModularFamily.subset ⟨B, B_mod⟩ diff_subset) ⟨y, ⟨(pair_subset_iff.1 xy_sub).2, _⟩⟩
Proof state after:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
encard_lt this : (X \ {x}).encard < X.encard
⊢ y ∉ {x}
Theorem: Matroid.modular_finite_intersection
Proof state before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
encard_lt this : (X \ {x}).encard < X.encard
⊢ y ∉ {x}
Tactic:
exact xy_ne.symm
Proof state after:
no goals
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inl.intro
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
x : Set α
hfin : {x}.Finite
hsub : {x} ⊆ Fs
hmod : M.ModularFamily fun x_1 => ↑x_1
hnone : {x}.Nonempty
⊢ ⋂₀ {x} ∈ Fs
Tactic:
rwa [sInter_singleton, ← singleton_subset_iff]
Proof state after:
no goals
Theorem: Matroid.modular_finite_intersection
Proof state before:
case x_eq_insert
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hmod : M.ModularFamily fun x => ↑x
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
⊢ X = insert x (X \ {x})
Tactic:
simp [pair_subset_iff.1 xy_sub]
Proof state after:
no goals
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.ModularPair x (⋂₀ (X \ {x}))
Tactic:
refine' ⟨B, B_mod.1, Bool.forall_bool.2 ⟨_, _⟩⟩
Proof state after:
case inr.intro.intro.intro.intro.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.Basis ((fun i => bif i then x else ⋂₀ (X \ {x})) false ∩ B) ((fun i => bif i then x else ⋂₀ (X \ {x})) false)

case inr.intro.intro.intro.intro.refine'_2
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.Basis ((fun i => bif i then x else ⋂₀ (X \ {x})) true ∩ B) ((fun i => bif i then x else ⋂₀ (X \ {x})) true)
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro.intro.refine'_2
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.Basis ((fun i => bif i then x else ⋂₀ (X \ {x})) true ∩ B) ((fun i => bif i then x else ⋂₀ (X \ {x})) true)
Tactic:
apply (B_mod.2 ⟨x, xy_sub (mem_insert _ _)⟩)
Proof state after:
no goals
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro.intro.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.Basis ((fun i => bif i then x else ⋂₀ (X \ {x})) false ∩ B) ((fun i => bif i then x else ⋂₀ (X \ {x})) false)
Tactic:
dsimp
Proof state after:
case inr.intro.intro.intro.intro.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.Basis (⋂₀ (X \ {x}) ∩ B) (⋂₀ (X \ {x}))
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro.intro.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.Basis (⋂₀ (X \ {x}) ∩ B) (⋂₀ (X \ {x}))
Tactic:
rw [sInter_eq_biInter]
Proof state after:
case inr.intro.intro.intro.intro.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.Basis ((⋂ i ∈ X \ {x}, i) ∩ B) (⋂ i ∈ X \ {x}, i)
Theorem: Matroid.modular_finite_intersection
Proof state before:
case inr.intro.intro.intro.intro.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ M.Basis ((⋂ i ∈ X \ {x}, i) ∩ B) (⋂ i ∈ X \ {x}, i)
Tactic:
apply B_mod.1.indep.interBasis_biInter ⟨y, _⟩ (fun i i_mem ↦ B_mod.2 ⟨i, i_mem.1⟩)
Proof state after:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ y ∈ X \ {x}
Theorem: Matroid.modular_finite_intersection
Proof state before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
X Fs : Set (Set α)
forall_flat : ∀ {F : Set α}, F ∈ Fs → M.Flat F
pair_modular : ∀ {F F' : Set α}, F ∈ Fs → F' ∈ Fs → M.ModularPair F F' → F ∩ F' ∈ Fs
hfin : X.Finite
hsub : X ⊆ Fs
hnone : X.Nonempty
X_nt : X.Nontrivial
x y : Set α
xy_ne : x ≠ y
xy_sub : {x, y} ⊆ X
x_eq_insert : X = insert x (X \ {x})
B : Set α
B_mod : M.ModularBase B fun x => ↑x
⊢ y ∈ X \ {x}
Tactic:
exact ⟨(pair_subset_iff.1 xy_sub).2, xy_ne.symm⟩
Proof state after:
no goals
Theorem: Matroid.ModularCut.remove
Proof state before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
⊢ M.cl Y ∈ C
Tactic:
set Js := {M.cl (B \ {b}) | b ∈ B \ Y}
Proof state after:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
⊢ M.cl Y ∈ C
Theorem: Matroid.ModularCut.remove
Proof state before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
⊢ M.cl Y ∈ C
Tactic:
set Js₁ := {(B \ {b}) | b ∈ B \ Y}
Proof state after:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
⊢ M.cl Y ∈ C
Theorem: Matroid.ModularCut.remove
Proof state before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
⊢ M.cl Y ∈ C
Tactic:
obtain (rfl | h_ne) := eq_or_ne Y B
Proof state after:
case inl
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
Y : Set α
hB₁ : M.Indep Y
hB₂ : Y ⊆ Y
h_remove : ∀ b ∈ Y \ Y, M.cl (Y \ {b}) ∈ C
h_B : M.cl Y ∈ C
Js : Set (Set α) := {x | ∃ b ∈ Y \ Y, M.cl (Y \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ Y \ Y, Y \ {b} = x}
⊢ M.cl Y ∈ C

case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
⊢ M.cl Y ∈ C