Theorem: Matroid.eq_of_spanning_iff_spanning_forall (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M = M'
Tactic:
have hsp' : M.Spanning = M'.Spanning := by
  ext S
  refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE] )
    (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
    (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
State after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ M = M'

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ M = M'
Tactic:
rw [← dual_inj, eq_iff_indep_iff_indep_forall, dual_ground, dual_ground, and_iff_right h]
State after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ ∀ I ⊆ M.E, M✶.Indep I ↔ M'✶.Indep I

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ ∀ I ⊆ M.E, M✶.Indep I ↔ M'✶.Indep I
Tactic:
intro I hIE
State after:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I
Tactic:
rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
⊢ M.Spanning = M'.Spanning
Tactic:
ext S
State after:
case h.a
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S✝ T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
⊢ M.Spanning S ↔ M'.Spanning S

State before:
case h.a
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S✝ T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
⊢ M.Spanning S ↔ M'.Spanning S
Tactic:
refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE] )
  (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
  (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X Y B C R : Set α
e f x y : α
S✝ T : Set α
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
⊢ M.Spanning S ↔ M'.Spanning S
Tactic:
rw [hsp _ hSE]
State after:
no goals