Theorem: Matroid.modularPair_iff (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 : α
M : Matroid α
X Y : Set α
⊢ M.ModularPair X Y ↔ ∃ I, M.Indep I ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
Tactic:
simp only [ModularPair, ModularFamily, mem_singleton_iff, modularBase_pair_iff, indep_iff]
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 : α
M : Matroid α
X Y : Set α
⊢ (∃ B, M.ModularBase B fun i => bif i then X else Y) ↔
    ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) 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 : α
M : Matroid α
X Y : Set α
⊢ (∃ B, M.ModularBase B fun i => bif i then X else Y) ↔
    ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
Tactic:
refine ⟨fun ⟨B, hB, hB'⟩ ↦ ⟨B, indep_iff.1 hB.indep, ?_⟩,
  fun ⟨I, ⟨B, hB, hIB⟩, hIX, hIY⟩ ↦ ⟨B, hB, ?_⟩ ⟩
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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (X ∩ B) X ∧ M.Basis (Y ∩ B) Y

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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)

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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
Tactic:
simp only [Bool.forall_bool, cond_false, cond_true]
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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ M.Basis (Y ∩ B) Y ∧ M.Basis (X ∩ B) X

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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ M.Basis (Y ∩ B) Y ∧ M.Basis (X ∩ B) X
Tactic:
rw [← hIX.eq_of_subset_indep (hB.indep.inter_left X) (inter_subset_inter_right _ hIB)
  inter_subset_left, ← hIY.eq_of_subset_indep (hB.indep.inter_left Y)
  (inter_subset_inter_right _ hIB) inter_subset_left]
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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ M.Basis (Y ∩ I) Y ∧ M.Basis (X ∩ I) X

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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ I, (∃ B, M.Base B ∧ I ⊆ B) ∧ M.Basis (X ∩ I) X ∧ M.Basis (Y ∩ I) Y
I B : Set α
hB : M.Base B
hIB : I ⊆ B
hIX : M.Basis (X ∩ I) X
hIY : M.Basis (Y ∩ I) Y
⊢ M.Basis (Y ∩ I) Y ∧ M.Basis (X ∩ I) X
Tactic:
exact ⟨hIY,hIX⟩
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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (X ∩ B) X ∧ M.Basis (Y ∩ B) Y
Tactic:
exact ⟨by simpa using hB' true, by simpa using hB' false⟩
State after:
no goals

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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (X ∩ B) X
Tactic:
simpa using hB' true
State after:
no goals

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 : α
M : Matroid α
X Y : Set α
x✝ : ∃ B, M.ModularBase B fun i => bif i then X else Y
B : Set α
hB : M.Base B
hB' : ∀ (i : Bool), M.Basis ((fun i => bif i then X else Y) i ∩ B) ((fun i => bif i then X else Y) i)
⊢ M.Basis (Y ∩ B) Y
Tactic:
simpa using hB' false
State after:
no goals