Theorem: Matroid.antichain_of_circuit_hyperplane (Matroid/Constructions/Relax.lean)

State before:
α : Type u_1
M✝ : Matroid α
E I H B X : Set α
e f : α
M : Matroid α
⊢ IsAntichain (fun x x_1 => x ⊆ x_1) ({B | M.Base B} ∪ {H | M.Circuit H ∧ M.Hyperplane H})
Tactic:
rintro X ((hX : M.Base X) | ⟨hXc, -⟩) Y ((hY : M.Base Y) | ⟨hYc, hYh⟩) hne hss
State after:
case inl.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False

case inl.inr.intro
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hYc : M.Circuit Y
hYh : M.Hyperplane Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False

case inr.intro.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False

case inr.intro.inr.intro
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hYc : M.Circuit Y
hYh : M.Hyperplane Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False

State before:
case inr.intro.inr.intro
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hYc : M.Circuit Y
hYh : M.Hyperplane Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Tactic:
exact hne (hXc.eq_of_subset_circuit hYc hss)
State after:
no goals

State before:
case inl.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Tactic:
exact hne (hX.eq_of_subset_base hY hss)
State after:
no goals

State before:
case inl.inr.intro
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hYc : M.Circuit Y
hYh : M.Hyperplane Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Tactic:
exact hYh.not_spanning (hX.spanning.superset hss)
State after:
no goals

State before:
case inr.intro.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
Tactic:
exact (hY.indep.subset hss).not_dep hXc.dep
State after:
no goals