Theorem: Matroid.hyperplane_iff_maximal_nonspanning (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 : α
⊢ M.Hyperplane H ↔ H ∈ maximals (fun x x_1 => x ⊆ x_1) {X | ¬M.Spanning X ∧ X ⊆ M.E}
Tactic:
simp_rw [and_comm (b := _ ⊆ _), mem_maximals_setOf_iff, and_imp]
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 : α
⊢ M.Hyperplane H ↔ (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃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 : α
⊢ M.Hyperplane H ↔ (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
Tactic:
refine' ⟨fun h ↦ ⟨⟨h.subset_ground, h.not_spanning⟩, fun X hX hX' hHX ↦ _⟩, fun h ↦ _⟩
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 : α
h : M.Hyperplane H
X : Set α
hX : 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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ M.Hyperplane H

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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ M.Hyperplane H
Tactic:
rw [hyperplane_iff_covBy, covBy_iff, and_iff_right M.ground_flat,
  flat_iff_ssubset_cl_insert_forall h.1.1]
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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ (∀ e ∈ M.E \ H, M.cl H ⊂ M.cl (insert e H)) ∧ H ⊂ M.E ∧ ∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E

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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ (∀ e ∈ M.E \ H, M.cl H ⊂ M.cl (insert e H)) ∧ H ⊂ M.E ∧ ∀ (F : Set α), M.Flat F → H ⊆ F → F ⊆ M.E → F = H ∨ F = M.E
Tactic:
refine'
  ⟨fun e he ↦ _, h.1.1.ssubset_of_ne (by rintro rfl; exact h.1.2 M.ground_spanning),
    fun F hF hHF hFE ↦ or_iff_not_imp_right.mpr fun hFE' ↦ _⟩
State after:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
⊢ M.cl H ⊂ M.cl (insert e H)

case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
⊢ F = H

State before:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
⊢ F = H
Tactic:
have h' := h.2 hFE
State after:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬M.Spanning F → H ⊆ F → H = F
⊢ F = H

State before:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬M.Spanning F → H ⊆ F → H = F
⊢ F = H
Tactic:
rw [hF.spanning_iff] at h'
State after:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬F = M.E → H ⊆ F → H = F
⊢ F = H

State before:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
F : Set α
hF : M.Flat F
hHF : H ⊆ F
hFE : F ⊆ M.E
hFE' : ¬F = M.E
h' : ¬F = M.E → H ⊆ F → H = F
⊢ F = H
Tactic:
rw [h' hFE' hHF]
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 : α
h : M.Hyperplane H
X : Set α
hX : X ⊆ M.E
hX' : ¬M.Spanning X
hHX : H ⊆ X
⊢ H = X
Tactic:
exact by_contra fun hne ↦ hX' (h.spanning_of_ssuperset (hHX.ssubset_of_ne hne))
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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
⊢ H ≠ M.E
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H₁ H₂ H' B C K : Set α
e f : α
h : (M.E ⊆ M.E ∧ ¬M.Spanning M.E) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → M.E ⊆ y → M.E = y
⊢ False

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H₁ H₂ H' B C K : Set α
e f : α
h : (M.E ⊆ M.E ∧ ¬M.Spanning M.E) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → M.E ⊆ y → M.E = y
⊢ False
Tactic:
exact h.1.2 M.ground_spanning
State after:
no goals

State before:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
⊢ M.cl H ⊂ M.cl (insert e H)
Tactic:
have h' := h.2 (insert_subset he.1 h.1.1)
State after:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : ¬M.Spanning (insert e H) → H ⊆ insert e H → H = insert e H
⊢ M.cl H ⊂ M.cl (insert e H)

State before:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : ¬M.Spanning (insert e H) → H ⊆ insert e H → H = insert e H
⊢ M.cl H ⊂ M.cl (insert e H)
Tactic:
simp only [subset_insert, forall_true_left, @eq_comm _ H, insert_eq_self, iff_false_intro he.2,
  imp_false, Classical.not_not, spanning_iff_cl]  at h'
State after:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.Spanning (insert e H)
⊢ M.cl H ⊂ M.cl (insert e H)

State before:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.Spanning (insert e H)
⊢ M.cl H ⊂ M.cl (insert e H)
Tactic:
rw [spanning_iff_cl] at h'
State after:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ M.cl H ⊂ M.cl (insert e H)

State before:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ M.cl H ⊂ M.cl (insert e H)
Tactic:
rw [h', ← not_spanning_iff_cl h.1.1]
State after:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ ¬M.Spanning H

State before:
case refine'_2.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 : α
h : (H ⊆ M.E ∧ ¬M.Spanning H) ∧ ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y
e : α
he : e ∈ M.E \ H
h' : M.cl (insert e H) = M.E
⊢ ¬M.Spanning H
Tactic:
exact h.1.2
State after:
no goals