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

State before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
⊢ M.cl Y ∈ C
Tactic:
set Js := {M.cl (B \ {b}) | b ∈ B \ Y}
State after:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
⊢ M.cl Y ∈ C

State before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
⊢ M.cl Y ∈ C
Tactic:
set Js₁ := {(B \ {b}) | b ∈ B \ Y}
State after:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
⊢ M.cl Y ∈ C

State before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
⊢ M.cl Y ∈ C
Tactic:
obtain (rfl | h_ne) := eq_or_ne Y B
State after:
case inl
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
Y : Set α
hB₁ : M.Indep Y
hB₂ : Y ⊆ Y
h_remove : ∀ b ∈ Y \ Y, M.cl (Y \ {b}) ∈ C
h_B : M.cl Y ∈ C
Js : Set (Set α) := {x | ∃ b ∈ Y \ Y, M.cl (Y \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ Y \ Y, Y \ {b} = x}
⊢ M.cl Y ∈ C

case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
⊢ M.cl Y ∈ C

State before:
case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
⊢ M.cl Y ∈ C
Tactic:
have Js₁_none : Js₁.Nonempty
State after:
case Js₁_none
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
⊢ Js₁.Nonempty

case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
⊢ M.cl Y ∈ C

State before:
case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
⊢ M.cl Y ∈ C
Tactic:
have Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
State after:
case Js₁_sInter_sub_B
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
⊢ ⋂₀ Js₁ ⊆ B

case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
⊢ M.cl Y ∈ C

State before:
case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
⊢ M.cl Y ∈ C
Tactic:
have Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁ := (by simp)
State after:
case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ M.cl Y ∈ C

State before:
case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ M.cl Y ∈ C
Tactic:
have Js_inter_eq : ⋂₀ Js = M.cl Y
State after:
case Js_inter_eq
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ ⋂₀ Js = M.cl Y

case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ M.cl Y ∈ C

State before:
case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ M.cl Y ∈ C
Tactic:
rw [← Js_inter_eq]
State after:
case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ ⋂₀ Js ∈ C

State before:
case inr
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ ⋂₀ Js ∈ C
Tactic:
apply C.modular
State after:
case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ Js ⊆ C.Fs

case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ Js.Nonempty

case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ M.ModularFamily fun X => ↑X

State before:
case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ M.ModularFamily fun X => ↑X
Tactic:
have:= hB₁
State after:
case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
this : M.Indep B
⊢ M.ModularFamily fun X => ↑X

State before:
case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
this : M.Indep B
⊢ M.ModularFamily fun X => ↑X
Tactic:
obtain ⟨B', B'_base, B_sub_B'⟩ := this
State after:
no goals

State before:
case inl
α : Type u_1
M✝ : Matroid α
I B : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
Y : Set α
hB₁ : M.Indep Y
hB₂ : Y ⊆ Y
h_remove : ∀ b ∈ Y \ Y, M.cl (Y \ {b}) ∈ C
h_B : M.cl Y ∈ C
Js : Set (Set α) := {x | ∃ b ∈ Y \ Y, M.cl (Y \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ Y \ Y, Y \ {b} = x}
⊢ M.cl Y ∈ C
Tactic:
assumption
State after:
no goals

State before:
case Js₁_none
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
⊢ Js₁.Nonempty
Tactic:
obtain ⟨b, hb⟩ := exists_of_ssubset (ssubset_iff_subset_ne.2 ⟨hB₂, h_ne⟩)
State after:
case Js₁_none.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
b : α
hb : b ∈ B ∧ b ∉ Y
⊢ Js₁.Nonempty

State before:
case Js₁_none.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
b : α
hb : b ∈ B ∧ b ∉ Y
⊢ Js₁.Nonempty
Tactic:
refine' ⟨B \ {b}, ⟨b, ⟨hb.1, hb.2⟩, rfl⟩⟩
State after:
no goals

State before:
case Js₁_sInter_sub_B
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
⊢ ⋂₀ Js₁ ⊆ B
Tactic:
intro j j_mem
State after:
case Js₁_sInter_sub_B
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
j : α
j_mem : j ∈ ⋂₀ Js₁
⊢ j ∈ B

State before:
case Js₁_sInter_sub_B
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
j : α
j_mem : j ∈ ⋂₀ Js₁
⊢ j ∈ B
Tactic:
rw [mem_sInter] at j_mem
State after:
case Js₁_sInter_sub_B
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
j : α
j_mem : ∀ t ∈ Js₁, j ∈ t
⊢ j ∈ B

State before:
case Js₁_sInter_sub_B
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
j : α
j_mem : ∀ t ∈ Js₁, j ∈ t
⊢ j ∈ B
Tactic:
obtain ⟨t, ht⟩ := Js₁_none
State after:
case Js₁_sInter_sub_B.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
j : α
j_mem : ∀ t ∈ Js₁, j ∈ t
t : Set α
ht : t ∈ Js₁
⊢ j ∈ B

State before:
case Js₁_sInter_sub_B.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
j : α
j_mem : ∀ t ∈ Js₁, j ∈ t
t : Set α
ht : t ∈ Js₁
⊢ j ∈ B
Tactic:
apply ((_ : t ⊆ B) (j_mem t ht))
State after:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
j : α
j_mem : ∀ t ∈ Js₁, j ∈ t
t : Set α
ht : t ∈ Js₁
⊢ t ⊆ B

State before:
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
j : α
j_mem : ∀ t ∈ Js₁, j ∈ t
t : Set α
ht : t ∈ Js₁
⊢ t ⊆ B
Tactic:
obtain ⟨b, _, rfl⟩ := ht
State after:
case intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
j : α
j_mem : ∀ t ∈ Js₁, j ∈ t
b : α
left✝ : b ∈ B \ Y
⊢ B \ {b} ⊆ B

State before:
case intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
j : α
j_mem : ∀ t ∈ Js₁, j ∈ t
b : α
left✝ : b ∈ B \ Y
⊢ B \ {b} ⊆ B
Tactic:
exact diff_subset _ _
State after:
no goals

State before:
case Js_inter_eq
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ ⋂₀ Js = M.cl Y
Tactic:
rw [sInter_eq_biInter, Js_biInter_eq, ← hB₁.cl_sInter_eq_biInter_cl_of_forall_subset Js₁_none]
State after:
case Js_inter_eq
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ M.cl (⋂₀ Js₁) = M.cl Y

case Js_inter_eq
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ ∀ J ∈ Js₁, J ⊆ B

State before:
case Js_inter_eq
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ ∀ J ∈ Js₁, J ⊆ B
Tactic:
rintro J ⟨b, _, rfl⟩
State after:
case Js_inter_eq.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
b : α
left✝ : b ∈ B \ Y
⊢ B \ {b} ⊆ B

State before:
case Js_inter_eq.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
b : α
left✝ : b ∈ B \ Y
⊢ B \ {b} ⊆ B
Tactic:
exact diff_subset _ _
State after:
no goals

State before:
case Js_inter_eq
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ M.cl (⋂₀ Js₁) = M.cl Y
Tactic:
congr!
State after:
case Js_inter_eq.h.e'_3
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ ⋂₀ Js₁ = Y

State before:
case Js_inter_eq.h.e'_3
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
⊢ ⋂₀ Js₁ = Y
Tactic:
ext x
State after:
case Js_inter_eq.h.e'_3.h
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
⊢ x ∈ ⋂₀ Js₁ ↔ x ∈ Y

State before:
case Js_inter_eq.h.e'_3.h
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
⊢ x ∈ ⋂₀ Js₁ ↔ x ∈ Y
Tactic:
refine' ⟨fun x_mem ↦ _, fun x_mem I I_mem ↦ _⟩
State after:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
⊢ x ∈ Y

case Js_inter_eq.h.e'_3.h.refine'_2
α : Type u_1
M✝ : Matroid α
I✝ B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ Y
I : Set α
I_mem : I ∈ Js₁
⊢ x ∈ I

State before:
case Js_inter_eq.h.e'_3.h.refine'_2
α : Type u_1
M✝ : Matroid α
I✝ B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ Y
I : Set α
I_mem : I ∈ Js₁
⊢ x ∈ I
Tactic:
obtain ⟨b, hb, rfl⟩ := I_mem
State after:
case Js_inter_eq.h.e'_3.h.refine'_2.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ Y
b : α
hb : b ∈ B \ Y
⊢ x ∈ B \ {b}

State before:
case Js_inter_eq.h.e'_3.h.refine'_2.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ Y
b : α
hb : b ∈ B \ Y
⊢ x ∈ B \ {b}
Tactic:
exact ⟨hB₂ x_mem, ne_of_mem_of_not_mem x_mem hb.2⟩
State after:
no goals

State before:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
⊢ x ∈ Y
Tactic:
by_contra x_notin_Y
State after:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
x_notin_Y : x ∉ Y
⊢ False

State before:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
x_notin_Y : x ∉ Y
⊢ False
Tactic:
have xBY : x ∈ B \ Y := ⟨Js₁_sInter_sub_B x_mem, x_notin_Y⟩
State after:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False

State before:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : x ∈ ⋂₀ Js₁
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False
Tactic:
rw [mem_sInter] at x_mem
State after:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : ∀ t ∈ Js₁, x ∈ t
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False

State before:
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : ∀ t ∈ Js₁, x ∈ t
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False
Tactic:
exact absurd rfl (x_mem (B \ {x}) ⟨x, xBY, rfl⟩).2
State after:
no goals

State before:
case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ Js ⊆ C.Fs
Tactic:
rintro J ⟨b, hb, rfl⟩
State after:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
b : α
hb : b ∈ B \ Y
⊢ M.cl (B \ {b}) ∈ C.Fs

State before:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
b : α
hb : b ∈ B \ Y
⊢ M.cl (B \ {b}) ∈ C.Fs
Tactic:
exact h_remove b hb
State after:
no goals

State before:
case inr.a
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
⊢ Js.Nonempty
Tactic:
obtain ⟨A, a, ha⟩ := Js₁_none
State after:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
A : Set α
a : α
ha : a ∈ B \ Y ∧ B \ {a} = A
⊢ Js.Nonempty

State before:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
A : Set α
a : α
ha : a ∈ B \ Y ∧ B \ {a} = A
⊢ Js.Nonempty
Tactic:
refine' ⟨M.cl (B \ {a}), _⟩
State after:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
A : Set α
a : α
ha : a ∈ B \ Y ∧ B \ {a} = A
⊢ M.cl (B \ {a}) ∈ Js

State before:
case inr.a.intro.intro
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
Js_inter_eq : ⋂₀ Js = M.cl Y
A : Set α
a : α
ha : a ∈ B \ Y ∧ B \ {a} = A
⊢ M.cl (B \ {a}) ∈ Js
Tactic:
refine' ⟨a, ha.1, rfl⟩
State after:
no goals