-- Mathlib/Data/Matroid/Circuit.lean
/-- For `I` independent, `M.fundCircuit e I` is the only circuit contained in `insert e I`. -/
lemma IsCircuit.eq_fundCircuit_of_subset (hC : M.IsCircuit C) (hI : M.Indep I)
    (hCs : C ⊆ insert e I) : C = M.fundCircuit e I

Proof state:
case inl
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
hCI : C ⊆ I
⊢ C = M.fundCircuit e I

Tactic:
exact (hC.not_indep (hI.subset hCI)).elim

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ M.fundCircuit e I ⊆ C

Tactic:
rw [fundCircuit_eq_sInter heI]

Result:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}) ⊆ C

Proof state:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ C = M.fundCircuit e I

Tactic:
refine hC.eq_of_superset_isCircuit (hI.fundCircuit_isCircuit ?_ fun heI ↦ ?_) hss

Result:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ e ∈ M.closure I

case refine_2
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
heI : e ∈ I
⊢ False

Proof state:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ M.Dep (insert e I) ∨ e ∈ I

Tactic:
exact .inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
⊢ M.fundCircuit e I ⊆ C

Tactic:
have heCcl := (hC.diff_singleton_isBasis heC).subset_closure heC

Result:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
⊢ M.fundCircuit e I ⊆ C

Proof state:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
heI : e ∈ I
⊢ insert e I ⊆ I

Tactic:
simp [heI]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
⊢ C = M.fundCircuit e I

Tactic:
obtain hCI | ⟨heC, hCeI⟩ := subset_insert_iff.1 hCs

Result:
case inl
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
hCI : C ⊆ I
⊢ C = M.fundCircuit e I

case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
⊢ C = M.fundCircuit e I

Proof state:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
⊢ M.fundCircuit e I ⊆ C

Tactic:
have heI : e ∈ M.closure I := M.closure_subset_closure hCeI heCcl

Result:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ M.fundCircuit e I ⊆ C

Proof state:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ e ∈ M.closure I

Tactic:
rw [hI.mem_closure_iff]

Result:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ M.Dep (insert e I) ∨ e ∈ I

Proof state:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}) ⊆ C

Tactic:
refine insert_subset heC <| (sInter_subset_of_mem (t := C \ {e}) ?_).trans diff_subset

Result:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ C \ {e} ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Proof state:
case inr.intro
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ C \ {e} ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
exact ⟨hCeI, heCcl⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
heI : e ∈ I
⊢ False

Tactic:
exact hC.not_indep (hI.subset (hCs.trans (by simp [heI])))

Result:
no goals