Theorem: Matroid.compl_cocircuit_iff_hyperplane (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
⊢ M.Cocircuit (M.E \ H) ↔ M.Hyperplane H
Tactic:
simp_rw [cocircuit_iff_mem_minimals_compl_nonspanning, hyperplane_iff_maximal_nonspanning,
  (and_comm (b := _ ⊆ _)), mem_minimals_setOf_iff, mem_maximals_setOf_iff,
  diff_diff_cancel_left hH, and_iff_right hH, subset_diff, and_imp, and_congr_right_iff]
State after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
⊢ ¬M.Spanning H →
    ((∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y) ↔
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
⊢ ¬M.Spanning H →
    ((∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y) ↔
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y)
Tactic:
refine' fun _ ↦ ⟨fun h X hXE hX hHX ↦ _, fun h X hX hXE hXH ↦ _⟩
State after:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H = X

case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ M.E \ H = X

State before:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ M.E \ H = X
Tactic:
rw [h diff_subset hX, diff_diff_cancel_left hXE]
State after:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ H ⊆ M.E \ X

State before:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ H ⊆ M.E \ X
Tactic:
rw [subset_diff]
State after:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ H ⊆ M.E ∧ Disjoint H X

State before:
case refine'_2
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXE : X ⊆ M.E
hXH : Disjoint X H
⊢ H ⊆ M.E ∧ Disjoint H X
Tactic:
exact ⟨hH, hXH.symm⟩
State after:
no goals

State before:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H = X
Tactic:
rw [← diff_diff_cancel_left hH, ← diff_diff_cancel_left hXE,
  h (y := M.E \ X) (by rwa [diff_diff_cancel_left hXE]) diff_subset]
State after:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ Disjoint (M.E \ X) H

State before:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ Disjoint (M.E \ X) H
Tactic:
rw [← subset_compl_iff_disjoint_left, diff_eq, compl_inter, compl_compl]
State after:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H ⊆ M.Eᶜ ∪ X

State before:
case refine'_1
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ H ⊆ M.Eᶜ ∪ X
Tactic:
exact hHX.trans subset_union_right
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hH : autoParam (H ⊆ M.E) _auto✝
x✝ : ¬M.Spanning H
h : ∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y
X : Set α
hXE : X ⊆ M.E
hX : ¬M.Spanning X
hHX : H ⊆ X
⊢ ¬M.Spanning (M.E \ (M.E \ X))
Tactic:
rwa [diff_diff_cancel_left hXE]
State after:
no goals