Theorem: Matroid.ModularCut.inter (Matroid/Old/_ModularCut.lean)

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ F ∩ F' ∈ C
Tactic:
rw [← sInter_pair]
State after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ ⋂₀ {F, F'} ∈ C

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ ⋂₀ {F, F'} ∈ C
Tactic:
apply C.sInter (pair_subset hF hF') _ (by simp)
State after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ M.ModularFamily fun X => ↑X

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ M.ModularFamily fun X => ↑X
Tactic:
let ⟨B, hB⟩ := hFF'
State after:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
⊢ M.ModularFamily fun X => ↑X

State before:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
⊢ M.ModularFamily fun X => ↑X
Tactic:
refine' ⟨B, hB.1, fun i ↦ _⟩
State after:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
⊢ M.Basis ((fun X => ↑X) i ∩ B) ((fun X => ↑X) i)

State before:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
⊢ M.Basis ((fun X => ↑X) i ∩ B) ((fun X => ↑X) i)
Tactic:
dsimp
State after:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
⊢ M.Basis (↑i ∩ B) ↑i

State before:
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
⊢ M.Basis (↑i ∩ B) ↑i
Tactic:
obtain (eq | ne) := mem_insert_iff.2 (Subtype.mem i)
State after:
case inl
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
eq : ↑i = F
⊢ M.Basis (↑i ∩ B) ↑i

case inr
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
ne : ↑i ∈ {F'}
⊢ M.Basis (↑i ∩ B) ↑i

State before:
case inr
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
ne : ↑i ∈ {F'}
⊢ M.Basis (↑i ∩ B) ↑i
Tactic:
rw [mem_singleton_iff.1 ne]
State after:
case inr
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
ne : ↑i ∈ {F'}
⊢ M.Basis (F' ∩ B) F'

State before:
case inr
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
ne : ↑i ∈ {F'}
⊢ M.Basis (F' ∩ B) F'
Tactic:
exact hB.2 false
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
⊢ {F, F'}.Nonempty
Tactic:
simp
State after:
no goals

State before:
case inl
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
eq : ↑i = F
⊢ M.Basis (↑i ∩ B) ↑i
Tactic:
rw [eq]
State after:
case inl
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
eq : ↑i = F
⊢ M.Basis (F ∩ B) F

State before:
case inl
α : Type u_1
M : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
F F' : Set α
C : M.ModularCut
hF : F ∈ C
hF' : F' ∈ C
hFF' : M.ModularPair F F'
B : Set α
hB : M.ModularBase B fun i => bif i then F else F'
i : ↑{F, F'}
eq : ↑i = F
⊢ M.Basis (F ∩ B) F
Tactic:
exact hB.2 true
State after:
no goals