Theorem: Matroid.skew_iff_exist_bases (Matroid/Modular.lean)

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ M.Skew X Y ↔ ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
change (M.ModularPair X Y ∧ _) ↔ _
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ (M.ModularPair X Y ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ (M.ModularPair X Y ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
rw [modularPair_iff_exists_basis_basis]
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ ((∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)) ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ ((∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)) ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
simp only [exists_and_left, ne_eq, Bool.forall_bool, Bool.not_eq_false, cond_false,
  Bool.not_eq_true, cond_true, inter_self, IsEmpty.forall_iff, forall_true_left, true_and,
  and_true]
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅ ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅ ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
Tactic:
refine ⟨fun ⟨⟨I, hI, J, hJ, hIJ⟩, h, _⟩ ↦ ⟨I, J, hIJ, ?_, hI, hJ⟩,
  fun ⟨I, J, hu, hdj, hI, hJ⟩ ↦ ⟨⟨I,hI,J,hJ,hu⟩  , ?_⟩ ⟩
State after:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
hIJ : M.Indep (I ∪ J)
h : Y ∩ X ⊆ M.cl ∅
right✝ : X ∩ Y ⊆ M.cl ∅
⊢ Disjoint I J

case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅

State before:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
Tactic:
rw [inter_comm, and_self]
State after:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ X ∩ Y ⊆ M.cl ∅

State before:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ X ∩ Y ⊆ M.cl ∅
Tactic:
refine (inter_subset_inter hI.subset_cl hJ.subset_cl).trans ?_
State after:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ M.cl I ∩ M.cl J ⊆ M.cl ∅

State before:
case refine_2
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
I J : Set α
hu : M.Indep (I ∪ J)
hdj : Disjoint I J
hI : M.Basis I X
hJ : M.Basis J Y
⊢ M.cl I ∩ M.cl J ⊆ M.cl ∅
Tactic:
rw [← hu.cl_inter_eq_inter_cl, hdj.inter_eq]
State after:
no goals

State before:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
hIJ : M.Indep (I ∪ J)
h : Y ∩ X ⊆ M.cl ∅
right✝ : X ∩ Y ⊆ M.cl ∅
⊢ Disjoint I J
Tactic:
rw [disjoint_iff_forall_ne]
State after:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
hIJ : M.Indep (I ∪ J)
h : Y ∩ X ⊆ M.cl ∅
right✝ : X ∩ Y ⊆ M.cl ∅
⊢ ∀ ⦃a : α⦄, a ∈ I → ∀ ⦃b : α⦄, b ∈ J → a ≠ b

State before:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
x✝ : (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
hIJ : M.Indep (I ∪ J)
h : Y ∩ X ⊆ M.cl ∅
right✝ : X ∩ Y ⊆ M.cl ∅
⊢ ∀ ⦃a : α⦄, a ∈ I → ∀ ⦃b : α⦄, b ∈ J → a ≠ b
Tactic:
rintro e heI _ heJ rfl
State after:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
X Y : Set α
x✝ : (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
hIJ : M.Indep (I ∪ J)
h : Y ∩ X ⊆ M.cl ∅
right✝ : X ∩ Y ⊆ M.cl ∅
e : α
heI : e ∈ I
heJ : e ∈ J
⊢ False

State before:
case refine_1
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J✝ X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
X Y : Set α
x✝ : (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
hIJ : M.Indep (I ∪ J)
h : Y ∩ X ⊆ M.cl ∅
right✝ : X ∩ Y ⊆ M.cl ∅
e : α
heI : e ∈ I
heJ : e ∈ J
⊢ False
Tactic:
exact (hI.indep.nonloop_of_mem heI).not_loop (h ⟨hJ.subset heJ, hI.subset heI⟩)
State after:
no goals