simp_rw [indep_iff_forall_subset_not_circuit', and_iff_left (diff_subset.trans
  (insert_subset ((M.cl_subset_ground I) he.1) hI.subset_ground)), imp_not_comm, subset_diff,
  disjoint_singleton_right, not_and, not_not]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ M.Indep (insert e I \ {f}) ↔ f ∈ M.fundCct e I
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
I₁ I₂ B₁ B₂ : Set α
hI : M.Indep I
he : e ∈ M.cl I \ I
⊢ (∀ (C : Set α), M.Circuit C → C ⊆ insert e I → f ∈ C) ↔ f ∈ M.fundCct e I