Theorem: Matroid.mem_dual_cl_iff_forall_circuit (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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M✶.cl X ↔ ∀ (C : Set α), M.Circuit C → e ∈ C → (X ∩ C).Nonempty
Tactic:
rw [← dual_dual M]
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M✶✶✶.cl X ↔ ∀ (C : Set α), M✶✶.Circuit C → e ∈ C → (X ∩ C).Nonempty

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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M✶✶✶.cl X ↔ ∀ (C : Set α), M✶✶.Circuit C → e ∈ C → (X ∩ C).Nonempty
Tactic:
simp_rw [← cocircuit_def, dual_dual M, mem_cl_iff_forall_hyperplane (M := M✶) hX he]
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H) ↔ ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty

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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H) ↔ ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
Tactic:
refine' ⟨fun h C hC heC ↦ by_contra fun hne ↦ _, fun h H hH hXE ↦ by_contra fun he' ↦ _⟩
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : ¬(X ∩ C).Nonempty
⊢ False

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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
⊢ False

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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
⊢ False
Tactic:
obtain ⟨f, hf⟩ := h _ hH.compl_cocircuit ⟨he, he'⟩
State after:
case refine'_2.intro
α : 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✝ : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
f : α
hf : f ∈ X ∩ (M✶.E \ H)
⊢ False

State before:
case refine'_2.intro
α : 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✝ : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty
H : Set α
hH : M✶.Hyperplane H
hXE : X ⊆ H
he' : e ∉ H
f : α
hf : f ∈ X ∩ (M✶.E \ H)
⊢ False
Tactic:
exact hf.2.2 (hXE hf.1)
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : ¬(X ∩ C).Nonempty
⊢ False
Tactic:
rw [nonempty_iff_ne_empty, not_not, ← disjoint_iff_inter_eq_empty] at hne
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : Disjoint X C
⊢ False

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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H
C : Set α
hC : M✶.Cocircuit C
heC : e ∈ C
hne : Disjoint X C
⊢ False
Tactic:
exact (h _ hC.compl_hyperplane (subset_diff.mpr ⟨hX, hne⟩)).2 heC
State after:
no goals