Theorem: Matroid.modular_finite_intersection (Matroid/Old/_ModularCut.lean)

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
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

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
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

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})
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

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]
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

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
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

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 _ _))) _
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

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
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

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
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

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, _⟩⟩
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}

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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 ⟨_, _⟩⟩
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)

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 _ _)⟩)
State after:
no goals

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
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}))

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]
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)

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⟩)
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}

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⟩
State after:
no goals