Theorem: Matroid.Modular_cut_pair (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert a (insert b X))
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ M.cl X ∈ C
Tactic:
rw [← union_insert_eq] at h_ind
State after:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ M.cl X ∈ C

State before:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ M.cl X ∈ C
Tactic:
have ab_cl_inter_eq : sInter {M.cl (insert b X), M.cl (insert a X)} = M.cl X
State after:
case ab_cl_inter_eq
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X

α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
ab_cl_inter_eq : ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
⊢ M.cl X ∈ C

State before:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
ab_cl_inter_eq : ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
⊢ M.cl X ∈ C
Tactic:
rw [← ab_cl_inter_eq]
State after:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
ab_cl_inter_eq : ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
⊢ ⋂₀ {M.cl (insert b X), M.cl (insert a X)} ∈ C

State before:
case ab_cl_inter_eq
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
Tactic:
rw [sInter_pair, ← h_ind.cl_inter_eq_inter_cl, inter_insert_eq hne.symm]
State after:
no goals