Theorem: Matroid.mem_cl_iff_forall_hyperplane (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 ↔ ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H
Tactic:
simp_rw [← M.cl_inter_ground X,
  M.cl_eq_sInter_hyperplanes _ (inter_subset_left.trans hX), mem_inter_iff, and_iff_left he,
  mem_sInter, mem_setOf_eq, 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (t : Set α), M.Hyperplane t → X ∩ M.E ⊆ t → e ∈ t) ↔ ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H

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✝
⊢ (∀ (t : Set α), M.Hyperplane t → X ∩ M.E ⊆ t → e ∈ t) ↔ ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H
Tactic:
exact ⟨fun h H hH hXH ↦ h _ hH (inter_subset_left.trans hXH),
  fun h H hH hXH ↦ h H hH (by rwa [inter_eq_self_of_subset_left hX] at hXH )⟩
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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
h : ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H
H : Set α
hH : M.Hyperplane H
hXH : X ∩ M.E ⊆ H
⊢ X ⊆ H
Tactic:
rwa [inter_eq_self_of_subset_left hX] at hXH
State after:
no goals