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

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ (M.relax X).Indep I ↔ M.Indep I ∨ I = X
Tactic:
rw [relax, relaxSet_indep_iff, mem_singleton_iff]
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ ∀ H ∈ {X}, M.Circuit H ∧ M.Hyperplane H

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane X
hC : M.Circuit X
⊢ ∀ H ∈ {X}, M.Circuit H ∧ M.Hyperplane H
Tactic:
simp [hH, hC]
State after:
no goals