Theorem: Matroid.eq_of_cl_eq_cl_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 : α
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.cl X = M₂.cl X
⊢ M₁.E = M₂.E
Tactic:
simpa using h univ
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 : α
M₁ M₂ : Matroid α
h : ∀ (X : Set α), M₁.cl X = M₂.cl X
x✝¹ : Set α
x✝ : x✝¹ ⊆ M₁.E
⊢ M₁.Indep x✝¹ ↔ M₂.Indep x✝¹
Tactic:
simp_rw [indep_iff_cl_diff_ne_forall, h]
State after:
no goals