-- Mathlib/Data/Matroid/Circuit.lean
/-- Fundamental circuits and cocircuits of a base `B` play dual roles;
`e` belongs to the fundamental cocircuit for `B` and `f` if and only if
`f` belongs to the fundamental circuit for `e` and `B`.
This statement isn't so reasonable unless `f ∈ B` and `e ∉ B`,
but holds due to junk values even without these assumptions. -/
lemma IsBase.mem_fundCocircuit_iff_mem_fundCircuit {e f : α} (hB : M.IsBase B) :
    e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B

Proof state:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert e (insert f (B \ {f}))

Tactic:
simp [hfB]

Result:
no goals

Proof state:
case inr.inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M.fundCircuit e B

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he

Result:
case inr.inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ {f}
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M.fundCircuit e B

Proof state:
case inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_not_mem_ground (by simpa)] at he

Result:
case inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ {f}
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B

Proof state:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ M.Indep (insert e B \ {f})

Tactic:
refine hB'.indep.subset ?_

Result:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B \ {f} ⊆ M.E \ (insert f (M✶.E \ B) \ {e})

Proof state:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∈ M.fundCircuit e B

Tactic:
rw [hB.indep.mem_fundCircuit_iff (by rwa [hB.closure_eq]) heB]

Result:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ M.Indep (insert e B \ {f})

Proof state:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B \ {f} ⊆ M.E \ (insert f (M✶.E \ B) \ {e})

Tactic:
simp only [dual_ground, diff_singleton_subset_iff]

Result:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert f (M.E \ (insert f (M.E \ B) \ {e}))

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
⊢ e ∈ M.E \ B

Tactic:
simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
⊢ f ∈ M.fundCircuit e B

Tactic:
obtain hfB | hfB := em' <| f ∈ B

Result:
case inr.inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M.fundCircuit e B

case inr.inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
⊢ f ∈ M.fundCircuit e B

Proof state:
case inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ {f}
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B

Tactic:
contradiction

Result:
no goals

Proof state:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert f (M.E \ (insert f (M.E \ B) \ {e}))

Tactic:
rw [diff_diff_right, inter_eq_self_of_subset_right (by simpa), union_singleton, insert_comm,
  ← union_singleton (s := M.E \ B), ← diff_diff, diff_diff_cancel_left hB.subset_ground]

Result:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ insert e B ⊆ insert e (insert f (B \ {f}))

Proof state:
case inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e : α
he : e ∈ M.fundCocircuit e B
⊢ e ∈ M.fundCircuit e B

Tactic:
simp [mem_fundCircuit]

Result:
no goals

Proof state:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ M.Indep (insert e B \ {f})

Tactic:
have hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e})) :=
  (hB'.exchange_isBase_of_indep' ⟨heE, heB⟩ (by simp [hfE, hfB]) he).compl_isBase_of_dual

Result:
case inr.inr.inr.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ M.Indep (insert e B \ {f})

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∉ B
⊢ f ∈ M✶.E \ B

Tactic:
simp [hfE, hfB]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ {e} ⊆ M.E

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∉ M✶.E

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∉ M✶.E \ B

Tactic:
simp [hfB]

Result:
no goals