-- 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
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
⊢ f ∈ M.fundCircuit e B

Tactic:
have hB' : M✶.IsBase (M✶.E \ B) := hB.compl_isBase_dual

Result:
case 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)
⊢ 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 : e ∈ M.fundCocircuit f 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.fundCircuit e B

Tactic:
rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he

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
⊢ f ∈ M.fundCircuit e B

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✶.closure (M✶.E \ B)

Tactic:
rwa [hB'.closure_eq]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
⊢ ∀ {N : Matroid α} {B' : Set α}, N.IsBase B' → ∀ {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'

Tactic:
clear! B M e f

Result:
α : Type u_1
⊢ ∀ {N : Matroid α} {B' : Set α}, N.IsBase B' → ∀ {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
aux : ∀ {N : Matroid α} {B' : Set α}, N.IsBase B' → ∀ {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'
h : f ∈ M.fundCircuit e B
⊢ f ∈ M✶.fundCocircuit e (M.E \ B)

Tactic:
simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]

Result:
no goals

Proof state:
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

Tactic:
obtain ⟨heE, heB⟩ : e ∈ M.E \ B :=
  by simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he

Result:
case inr.inr.inr.intro
α : 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
heE : e ∈ M.E
heB : e ∉ B
⊢ f ∈ M.fundCircuit e B

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

Tactic:
obtain rfl | hne := eq_or_ne e f

Result:
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

case inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
⊢ f ∈ M.fundCircuit e B

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
⊢ f ∉ M✶.E \ B

Tactic:
simp [hfE, hfB]

Result:
no goals

Proof state:
case 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)
⊢ f ∈ M.fundCircuit e B

Tactic:
obtain hfE | hfE := em' <| f ∈ M.E

Result:
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

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

Proof state:
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

Tactic:
contradiction

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
⊢ e ∈ M.closure B

Tactic:
rwa [hB.closure_eq]

Result:
no goals

Proof state:
α : Type u_1
⊢ ∀ {N : Matroid α} {B' : Set α}, N.IsBase B' → ∀ {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'

Tactic:
intro M B hB e f he

Result:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
⊢ f ∈ M.fundCircuit e B

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
⊢ e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B

Tactic:
suffices aux : ∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f},
    e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B' from
  ⟨fun h ↦ aux hB h , fun h ↦ aux hB.compl_isBase_dual <| by
    simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]⟩

Result:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
⊢ ∀ {N : Matroid α} {B' : Set α}, N.IsBase B' → ∀ {e f : α}, e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B'