Theorem: Matroid.skew_iff_cl_skew_left (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 : α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y
Tactic:
by_cases hY : Y ⊆ M.E
State after:
case pos
ι : 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : Y ⊆ M.E
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y

case neg
ι : 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : ¬Y ⊆ M.E
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y

State before:
case neg
ι : 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : ¬Y ⊆ M.E
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y
Tactic:
exact iff_of_false (fun h ↦ hY <| h.subset_ground_right) (fun h ↦ hY <| h.subset_ground_right)
State after:
no goals

State before:
case pos
ι : 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
hY : Y ⊆ M.E
⊢ M.Skew X Y ↔ M.Skew (M.cl X) Y
Tactic:
rw [skew_iff_cl_skew, iff_comm, skew_iff_cl_skew, cl_cl]
State after:
no goals