Theorem: Matroid.mem_ofDeleteElem_iff (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ F ∈ ModularCut.ofDeleteElem M e ↔ e ∉ F ∧ M.cl F = insert e F
Tactic:
change _ ∧ _ ↔ _
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (M ＼ e).Flat F ∧ e ∈ M.cl F ↔ e ∉ F ∧ M.cl F = insert e F

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (M ＼ e).Flat F ∧ e ∈ M.cl F ↔ e ∉ F ∧ M.cl F = insert e F
Tactic:
rw [flat_deleteElem_iff, and_assoc, and_congr_right_iff]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F → ((M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F ↔ M.cl F = insert e F)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F → ((M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F ↔ M.cl F = insert e F)
Tactic:
refine fun he ↦ ⟨?_, fun h ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F → M.cl F = insert e F

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
h : M.cl F = insert e F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F

State before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
h : M.cl F = insert e F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F
Tactic:
rw [h, and_iff_left (.inl rfl), ← h]
State after:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
h : M.cl F = insert e F
⊢ M.Flat F ∨ M.Flat (M.cl F)

State before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
h : M.cl F = insert e F
⊢ M.Flat F ∨ M.Flat (M.cl F)
Tactic:
exact .inr (M.cl_flat F)
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
⊢ (M.Flat F ∨ M.Flat (insert e F)) ∧ e ∈ M.cl F → M.cl F = insert e F
Tactic:
rintro ⟨(hF | hF), heF⟩
State after:
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat F
⊢ M.cl F = insert e F

case refine_1.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat (insert e F)
⊢ M.cl F = insert e F

State before:
case refine_1.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat (insert e F)
⊢ M.cl F = insert e F
Tactic:
rw [← hF.cl, ← cl_insert_cl_eq_cl_insert, insert_eq_of_mem heF, cl_cl]
State after:
no goals

State before:
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ M.cl F
hF : M.Flat F
⊢ M.cl F = insert e F
Tactic:
rw [hF.cl] at heF
State after:
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ F
hF : M.Flat F
⊢ M.cl F = insert e F

State before:
case refine_1.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∉ F
heF : e ∈ F
hF : M.Flat F
⊢ M.cl F = insert e F
Tactic:
contradiction
State after:
no goals