Theorem: Matroid.Basis.strong_exchange (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
Tactic:
obtain ⟨f, hf, h₁, h₂⟩ := hI₁.base_restrict.strong_exchange hI₂.base_restrict he
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : (M ↾ X).Base (insert e I₂ \ {f})
h₂ : (M ↾ X).Base (insert f I₁ \ {e})
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : (M ↾ X).Base (insert e I₂ \ {f})
h₂ : (M ↾ X).Base (insert f I₁ \ {e})
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
Tactic:
rw [base_restrict_iff] at h₁ h₂
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : M.Basis (insert e I₂ \ {f}) X
h₂ : M.Basis (insert f I₁ \ {e}) X
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hI₁ : M.Basis I₁ X
hI₂ : M.Basis I₂ X
he : e ∈ I₁ \ I₂
f : α
hf : f ∈ I₂ \ I₁
h₁ : M.Basis (insert e I₂ \ {f}) X
h₂ : M.Basis (insert f I₁ \ {e}) X
⊢ ∃ f ∈ I₂ \ I₁, M.Basis (insert e I₂ \ {f}) X ∧ M.Basis (insert f I₁ \ {e}) X
Tactic:
exact ⟨f, hf, h₁, h₂⟩
State after:
no goals