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

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.cl X ∈ C
Tactic:
rw [← (@inter_insert_eq _ X _ _ hne), Indep.cl_inter_eq_inter_cl]
State after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.cl (insert a X) ∩ M.cl (insert b X) ∈ C

α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Indep (insert a X ∪ insert b X)

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Indep (insert a X ∪ insert b X)
Tactic:
rwa [union_insert_eq, insert_comm]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.cl (insert a X) ∩ M.cl (insert b X) ∈ C
Tactic:
apply C.inter ha hb (modularPair_iff.2 ⟨(insert a (insert b X)), hI, _⟩)
State after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (M.cl (insert a X) ∩ insert a (insert b X)) (M.cl (insert a X)) ∧
    M.Basis (M.cl (insert b X) ∩ insert a (insert b X)) (M.cl (insert b X))

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (M.cl (insert a X) ∩ insert a (insert b X)) (M.cl (insert a X)) ∧
    M.Basis (M.cl (insert b X) ∩ insert a (insert b X)) (M.cl (insert b X))
Tactic:
rw [hI.cl_inter_eq_self_of_subset (subset_insert _ _), hI.cl_inter_eq_self_of_subset]
State after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (insert a X) (M.cl (insert a X)) ∧ M.Basis (insert b X) (M.cl (insert b X))

α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert a (insert b X)

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert a (insert b X)
Tactic:
rw [insert_comm]
State after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert b (insert a X)

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert b (insert a X)
Tactic:
exact subset_insert _ _
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (insert a X) (M.cl (insert a X)) ∧ M.Basis (insert b X) (M.cl (insert b X))
Tactic:
refine' ⟨Indep.basis_cl (hI.subset _), Indep.basis_cl (hI.subset (subset_insert _ _))⟩
State after:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert a (insert b X)