-- Mathlib/Data/Matroid/Circuit.lean
lemma Indep.fundCircuit_isCircuit (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) :
    M.IsCircuit (M.fundCircuit e I)

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simp [show ∃ x ⊆ I, e ∈ M.closure x ∧ e ∉ x from ⟨I, by simp [hecl, heI]⟩]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}))

Tactic:
refine (hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}

case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

case refine_3
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ f ∈ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}, e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ M.IsCircuit (M.fundCircuit e I)

Tactic:
have aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I := sInter_subset_of_mem (by simpa)

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (M.fundCircuit e I)

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ J ∈ {J | J ⊆ I ∧ e ∈ M.closure J}, J ⊆ I

Tactic:
simp +contextual

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ I ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ ⋂ J ∈ {J | J ⊆ I ∧ e ∈ M.closure J}, M.closure J

Tactic:
simp

Result:
no goals

Proof state:
case refine_3
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ (f : α), (∀ t ⊆ I, e ∈ M.closure t → f ∈ t) → e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
exact fun f hf hecl ↦ (hf _ (diff_subset.trans aux) hecl).2 rfl

Result:
no goals

Proof state:
case refine_3
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ f ∈ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}, e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
simp only [mem_sInter, mem_setOf_eq, and_imp]

Result:
case refine_3
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ (f : α), (∀ t ⊆ I, e ∈ M.closure t → f ∈ t) → e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ I ⊆ I ∧ e ∈ M.closure I ∧ e ∉ I

Tactic:
simp [hecl, heI]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (M.fundCircuit e I)

Tactic:
rw [fundCircuit_eq_sInter hecl]

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}))

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ I ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

Tactic:
rw [hI.closure_sInter_eq_biInter_closure_of_forall_subset ⟨I, by simpa⟩ (by simp +contextual)]

Result:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ ⋂ J ∈ {J | J ⊆ I ∧ e ∈ M.closure J}, M.closure J