Theorem: Matroid.relaxSet_indep_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).Indep I ↔ M.Indep I ∨ I ∈ Hs
Tactic:
simp_rw [indep_iff, relaxSet_base_iff h]
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
⊢ (∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B) ↔ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ 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
⊢ (∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B) ↔ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ Hs
Tactic:
refine' ⟨fun ⟨B, hB, hIB⟩ ↦ hB.elim (fun hB' ↦ Or.inl ⟨B, hB', hIB⟩) (fun hB' ↦ _),
  fun h ↦ h.elim (fun ⟨B, hB, hIB⟩ ↦ ⟨B, Or.inl hB, hIB⟩) fun hI ↦ ⟨I, Or.inr hI, rfl.subset⟩⟩
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
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
⊢ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ 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
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
⊢ (∃ B, M.Base B ∧ I ⊆ B) ∨ I ∈ Hs
Tactic:
refine hIB.eq_or_ssubset.elim (fun h ↦ Or.inr (by rwa [h])) (fun hss ↦ Or.inl ?_)
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
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
hss : I ⊂ B
⊢ ∃ B, M.Base B ∧ I ⊆ B

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
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
hss : I ⊂ B
⊢ ∃ B, M.Base B ∧ I ⊆ B
Tactic:
apply Indep.exists_base_superset (hB.elim (fun h' ↦ h'.indep.subset hIB)
  (fun h' ↦ (h _ h').1.ssubset_indep hss))
State after:
no goals

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
x✝ : ∃ B, (M.Base B ∨ B ∈ Hs) ∧ I ⊆ B
B : Set α
hB : M.Base B ∨ B ∈ Hs
hIB : I ⊆ B
hB' : B ∈ Hs
h : I = B
⊢ I ∈ Hs
Tactic:
rwa [h]
State after:
no goals