Theorem: Matroid.Base.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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
Tactic:
suffices h1 : (∃ f, f ∈ B₂ \ B₁ ∧  M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})) by
  obtain ⟨f, hf, h₁, h₂⟩ := h1;
  exact ⟨f, hf, hB₂.exchange_base_of_indep' hf.1 he.2 h₁,
    hB₁.exchange_base_of_indep' he.1 hf.2 h₂⟩
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
Tactic:
have he₁ : e ∈ M.cl B₂ \ B₂ := by
  rw [hB₂.cl_eq]; exact ⟨hB₁.subset_ground he.1, he.2⟩
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
Tactic:
simp_rw [hB₂.indep.rev_exchange_indep_iff he₁]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ ∧ M.Indep (insert f B₁ \ {e})

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
⊢ ∃ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ ∧ M.Indep (insert f B₁ \ {e})
Tactic:
by_contra! h
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
⊢ False

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
⊢ False
Tactic:
have hC := hB₂.indep.fundCct_circuit he₁
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ False

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ False
Tactic:
have hCss : M.fundCct e B₂ \ {e} ⊆ B₂ := by
  rw [diff_subset_iff, singleton_union]; exact fundCct_subset_insert _ _
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
⊢ False

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
⊢ False
Tactic:
have hcl : M.fundCct e B₂ ⊆ M.cl (B₁ \ {e}) := by
  refine' (hC.subset_cl_diff_singleton e).trans (cl_subset_cl_of_subset_cl (fun f hf ↦ _))
  have hef : f ≠ e := by rintro rfl; exact hf.2 rfl
  rw [(hB₁.indep.diff {e}).mem_cl_iff, dep_iff, insert_subset_iff,
    and_iff_left (diff_subset.trans hB₁.subset_ground), or_iff_not_imp_right, mem_diff,
    and_iff_left (hC.subset_ground hf.1), mem_singleton_iff,
    and_iff_left hef, insert_diff_singleton_comm hef]
  exact fun hfB₁ ↦ h _ ⟨hCss hf,hfB₁⟩ (diff_subset hf)
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
hcl : M.fundCct e B₂ ⊆ M.cl (B₁ \ {e})
⊢ False

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
hcl : M.fundCct e B₂ ⊆ M.cl (B₁ \ {e})
⊢ False
Tactic:
exact hB₁.indep.not_mem_cl_diff_of_mem he.1 (hcl (mem_fundCct _ _ _))
State after:
no goals

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
h1 : ∃ f ∈ B₂ \ B₁, M.Indep (insert e B₂ \ {f}) ∧ M.Indep (insert f B₁ \ {e})
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
Tactic:
obtain ⟨f, hf, h₁, h₂⟩ := h1
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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
f : α
hf : f ∈ B₂ \ B₁
h₁ : M.Indep (insert e B₂ \ {f})
h₂ : M.Indep (insert f B₁ \ {e})
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
f : α
hf : f ∈ B₂ \ B₁
h₁ : M.Indep (insert e B₂ \ {f})
h₂ : M.Indep (insert f B₁ \ {e})
⊢ ∃ f ∈ B₂ \ B₁, M.Base (insert e B₂ \ {f}) ∧ M.Base (insert f B₁ \ {e})
Tactic:
exact ⟨f, hf, hB₂.exchange_base_of_indep' hf.1 he.2 h₁,
  hB₁.exchange_base_of_indep' he.1 hf.2 h₂⟩
State after:
no goals

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ e ∈ M.cl B₂ \ B₂
Tactic:
rw [hB₂.cl_eq]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ e ∈ M.E \ B₂

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
⊢ e ∈ M.E \ B₂
Tactic:
exact ⟨hB₁.subset_ground he.1, he.2⟩
State after:
no goals

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ M.fundCct e B₂ \ {e} ⊆ B₂
Tactic:
rw [diff_subset_iff, singleton_union]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ M.fundCct e B₂ ⊆ insert e B₂

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
⊢ M.fundCct e B₂ ⊆ insert e B₂
Tactic:
exact fundCct_subset_insert _ _
State after:
no goals

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
⊢ M.fundCct e B₂ ⊆ M.cl (B₁ \ {e})
Tactic:
refine' (hC.subset_cl_diff_singleton e).trans (cl_subset_cl_of_subset_cl (fun f hf ↦ _))
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
⊢ f ∈ M.cl (B₁ \ {e})

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
⊢ f ∈ M.cl (B₁ \ {e})
Tactic:
have hef : f ≠ e := by rintro rfl; exact hf.2 rfl
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
hef : f ≠ e
⊢ f ∈ M.cl (B₁ \ {e})

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
hef : f ≠ e
⊢ f ∈ M.cl (B₁ \ {e})
Tactic:
rw [(hB₁.indep.diff {e}).mem_cl_iff, dep_iff, insert_subset_iff,
  and_iff_left (diff_subset.trans hB₁.subset_ground), or_iff_not_imp_right, mem_diff,
  and_iff_left (hC.subset_ground hf.1), mem_singleton_iff,
  and_iff_left hef, insert_diff_singleton_comm hef]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
hef : f ≠ e
⊢ f ∉ B₁ → ¬M.Indep (insert f B₁ \ {e})

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
hef : f ≠ e
⊢ f ∉ B₁ → ¬M.Indep (insert f B₁ \ {e})
Tactic:
exact fun hfB₁ ↦ h _ ⟨hCss hf,hfB₁⟩ (diff_subset hf)
State after:
no goals

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 α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
he : e ∈ B₁ \ B₂
he₁ : e ∈ M.cl B₂ \ B₂
h : ∀ f ∈ B₂ \ B₁, f ∈ M.fundCct e B₂ → ¬M.Indep (insert f B₁ \ {e})
hC : M.Circuit (M.fundCct e B₂)
hCss : M.fundCct e B₂ \ {e} ⊆ B₂
f : α
hf : f ∈ M.fundCct e B₂ \ {e}
⊢ f ≠ e
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
f : α
he : f ∈ B₁ \ B₂
he₁ : f ∈ M.cl B₂ \ B₂
h : ∀ f_1 ∈ B₂ \ B₁, f_1 ∈ M.fundCct f B₂ → ¬M.Indep (insert f_1 B₁ \ {f})
hC : M.Circuit (M.fundCct f B₂)
hCss : M.fundCct f B₂ \ {f} ⊆ B₂
hf : f ∈ M.fundCct f B₂ \ {f}
⊢ False

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
f✝ x y : α
I₁ I₂ B₁ B₂ : Set α
hB₁ : M.Base B₁
hB₂ : M.Base B₂
f : α
he : f ∈ B₁ \ B₂
he₁ : f ∈ M.cl B₂ \ B₂
h : ∀ f_1 ∈ B₂ \ B₁, f_1 ∈ M.fundCct f B₂ → ¬M.Indep (insert f_1 B₁ \ {f})
hC : M.Circuit (M.fundCct f B₂)
hCss : M.fundCct f B₂ \ {f} ⊆ B₂
hf : f ∈ M.fundCct f B₂ \ {f}
⊢ False
Tactic:
exact hf.2 rfl
State after:
no goals