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

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ (M.relaxSet Hs).Base B ↔ M.Base B ∨ B ∈ Hs
Tactic:
simp only [relaxSet, Matroid.ofBase]
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ M.Base B ∨ B ∈ Hs ∧ M.Circuit B ∧ M.Hyperplane B ↔ M.Base B ∨ B ∈ Hs

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
Hs : Set (Set α)
h : ∀ H ∈ Hs, M.Circuit H ∧ M.Hyperplane H
⊢ M.Base B ∨ B ∈ Hs ∧ M.Circuit B ∧ M.Hyperplane B ↔ M.Base B ∨ B ∈ Hs
Tactic:
exact ⟨fun h' ↦ h'.elim Or.inl (Or.inr ∘ And.left),
  fun h' ↦ h'.elim Or.inl (fun hBs ↦ Or.inr ⟨hBs, h B hBs⟩)⟩
State after:
no goals