Theorem: Matroid.ModularCut.mem_of_ssubset_indep_of_forall_diff (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
⊢ M.cl J ∈ U
Tactic:
set Is : ↑(I \ J) → Set α := fun e ↦ I \ {e.1} with hIs
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
⊢ M.cl J ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
⊢ M.cl J ∈ U
Tactic:
have hmod : M.ModularFamily Is := hI.modularFamily_of_subsets (by simp [hIs])
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
⊢ M.cl J ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
⊢ M.cl J ∈ U
Tactic:
have hne := nonempty_of_ssubset hJI
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
⊢ M.cl J ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
⊢ M.cl J ∈ U
Tactic:
have h_inter : ⋂ e, Is e = J := by
  rw [hIs, ← biInter_eq_iInter (t := fun x _ ↦ I \ {x}), biInter_diff_singleton_eq_diff _ hne,
    diff_diff_right, diff_self, empty_union, inter_eq_self_of_subset_right hJI.subset]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
⊢ M.cl J ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
⊢ M.cl J ∈ U
Tactic:
have _ := hne.coe_sort
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ M.cl J ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ M.cl J ∈ U
Tactic:
rw [← h_inter, ← hmod.iInter_cl_eq_cl_iInter]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ ⋂ i, M.cl (Is i) ∈ U

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝ : Nonempty ↑(I \ J)
⊢ ⋂ i, M.cl (Is i) ∈ U
Tactic:
exact U.iInter_mem _ (fun ⟨i, hi⟩ ↦ h _ (by simpa)) hmod.cls_modularFamily
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
⊢ ⋃ i, Is i ⊆ I
Tactic:
simp [hIs]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
⊢ ⋂ e, Is e = J
Tactic:
rw [hIs, ← biInter_eq_iInter (t := fun x _ ↦ I \ {x}), biInter_diff_singleton_eq_diff _ hne,
  diff_diff_right, diff_self, empty_union, inter_eq_self_of_subset_right hJI.subset]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hI : M.Indep I
hJI : J ⊂ I
h : ∀ e ∈ I \ J, M.cl (I \ {e}) ∈ U
Is : ↑(I \ J) → Set α := fun e => I \ {↑e}
hIs : Is = fun e => I \ {↑e}
hmod : M.ModularFamily Is
hne : (I \ J).Nonempty
h_inter : ⋂ e, Is e = J
x✝¹ : Nonempty ↑(I \ J)
x✝ : ↑(I \ J)
i : α
hi : i ∈ I \ J
⊢ ↑⟨i, hi⟩ ∈ I \ J
Tactic:
simpa
State after:
no goals