Theorem: Matroid.rFin.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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
⊢ M.ModularPair X Y ↔ M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Tactic:
refine ⟨fun h ↦ h.er_add_er, fun hr ↦ modularPair_iff_exists_basis_basis.2 ?_ ⟩
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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)

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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_basis (X ∩ Y)
State after:
case intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)

State before:
case intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
have hifin : Ii.encard ≠ ⊤ := by
  simpa using (hXfin.inter_right Y).finite_of_basis hIi
State after:
case intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)

State before:
case intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
obtain ⟨IX, hIX, hX⟩ := hIi.indep.subset_basis_of_subset
  (hIi.subset.trans inter_subset_left)
State after:
case intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)

State before:
case intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
obtain ⟨IY, hIY, hY⟩ := hIi.indep.subset_basis_of_subset
  (hIi.subset.trans inter_subset_right)
State after:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)

State before:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ ∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)
Tactic:
refine ⟨IX, IY, hIX, hIY, ?_⟩
State after:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ M.Indep (IX ∪ IY)

State before:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ M.Indep (IX ∪ IY)
Tactic:
rw [hIi.er_eq_encard, hIX.er_eq_encard, ← encard_diff_add_encard_of_subset hX,
  add_comm (encard _), add_assoc, WithTop.add_left_cancel_iff hifin, hIY.er_eq_encard,
  ← encard_union_add_encard_inter, ← union_eq_self_of_subset_left hY, ← union_assoc,
  diff_union_self, union_eq_self_of_subset_right hX] at hr
State after:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ M.Indep (IX ∪ IY)

State before:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ M.Indep (IX ∪ IY)
Tactic:
refine Basis.indep <| (hXfin.union hYfin).basis_of_subset_cl_of_subset_of_encard_le ?_
  (union_subset_union hIX.subset hIY.subset) (le_of_add_le_left hr.le)
State after:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (IX ∪ IY)

State before:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (IX ∪ IY)
Tactic:
rw [← M.cl_union_cl_left_eq, ← M.cl_union_cl_right_eq]
State after:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (M.cl IX ∪ M.cl IY)

State before:
case intro.intro.intro.intro.intro
ι : 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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
hifin : Ii.encard ≠ ⊤
IX : Set α
hIX : M.Basis IX X
hX : Ii ⊆ IX
IY : Set α
hr : (IX ∪ IY).encard + (IX \ Ii ∩ (Ii ∪ IY)).encard = M.er (X ∪ Y)
hIY : M.Basis IY Y
hY : Ii ⊆ IY
⊢ X ∪ Y ⊆ M.cl (M.cl IX ∪ M.cl IY)
Tactic:
exact (M.subset_cl _).trans (M.cl_subset_cl (union_subset_union hIX.subset_cl hIY.subset_cl))
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 : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
⊢ Ii.encard ≠ ⊤
Tactic:
simpa using (hXfin.inter_right Y).finite_of_basis hIi
State after:
no goals