Theorem: Matroid.mem_cl_iff_exists_circuit_of_not_mem (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
⊢ e ∈ M.cl X ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
rw [← cl_inter_ground, mem_cl_iff_mem_or_exists_circuit, mem_inter_iff, iff_false_intro he,
  false_and_iff, false_or_iff]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
⊢ (∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e (X ∩ M.E)) ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
⊢ (∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e (X ∩ M.E)) ↔ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
Tactic:
refine' ⟨
  fun ⟨C, hC, heC, h⟩ ↦ ⟨C, hC, heC, h.trans ((insert_subset_insert inter_subset_left))⟩,
  fun ⟨C, hC, heC, h⟩ ↦ ⟨C, hC, heC, (subset_inter h hC.subset_ground).trans _⟩⟩
State after:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
h : C ⊆ insert e X
⊢ insert e X ∩ M.E ⊆ insert e (X ∩ M.E)

State before:
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
he : e ∉ X
x✝ : ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e X
C : Set α
hC : M.Circuit C
heC : e ∈ C
h : C ⊆ insert e X
⊢ insert e X ∩ M.E ⊆ insert e (X ∩ M.E)
Tactic:
rw [insert_inter_of_mem (hC.subset_ground heC)]
State after:
no goals