-- Mathlib/Data/Matroid/Circuit.lean
lemma fundCircuit_restrict {R : Set α} (hIR : I ⊆ R) (heR : e ∈ R) (hR : R ⊆ M.E) :
    (M ↾ R).fundCircuit e I = M.fundCircuit e I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ {e} ⊆ R

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ M.closure J ∩ R
⊢ {e} ⊆ M.closure J

Tactic:
simp only [subset_inter_iff, inter_subset_right, and_true] at heJ

Result:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ M.closure J
⊢ {e} ⊆ M.closure J

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

Tactic:
refine subset_antisymm (insert_subset_insert (inter_subset_inter_right _ ?_))
  (insert_subset_insert (inter_subset_inter_right _ ?_))

Result:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J} ⊆ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}

case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J} ⊆ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ M.closure J
⊢ {e} ⊆ M.closure {e} ∩ R

Tactic:
simpa [M.mem_closure_of_mem' (mem_singleton e) (hR heR)]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ⊆ M.closure (J ∩ R)

Tactic:
rwa [inter_eq_self_of_subset_left (hJI.trans hIR)]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ∩ R ⊆ M.closure (J ∩ R) ∩ R ∪ R \ M.E

Tactic:
refine (inter_subset_inter_left _ ?_).trans subset_union_left

Result:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ⊆ M.closure (J ∩ R)

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ∩ R ⊆ (M ↾ R).closure J

Tactic:
simp only [restrict_closure_eq', union_subset_iff, subset_union_right, and_true]

Result:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ∩ R ⊆ M.closure (J ∩ R) ∩ R ∪ R \ M.E

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J} ⊆ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}

Tactic:
refine subset_sInter fun J ⟨hJI, heJ⟩ ↦ sInter_subset_of_mem ⟨hJI, ?_⟩

Result:
case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ∩ R ⊆ (M ↾ R).closure J

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J} ⊆ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}

Tactic:
refine subset_sInter fun J ⟨hJI, heJ⟩ ↦ sInter_subset_of_mem
  ⟨hJI, M.closure_subset_closure_of_subset_closure ?_⟩

Result:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ (M ↾ R).closure J
⊢ {e} ⊆ M.closure J

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ M.closure J
⊢ {e} ⊆ M.closure J

Tactic:
exact subset_trans (by simpa [M.mem_closure_of_mem' (mem_singleton e) (hR heR)]) heJ

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ (M ↾ R).closure J
⊢ {e} ⊆ M.closure J

Tactic:
rw [restrict_closure_eq _ (hJI.trans hIR) hR] at heJ

Result:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
x✝ : J ∈ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ M.closure J ∩ R
⊢ {e} ⊆ M.closure J

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ (M ↾ R).fundCircuit e I = M.fundCircuit e I

Tactic:
simp_rw [fundCircuit, M.restrict_closure_eq (R := R) (X := {e}) (by simpa)]

Result:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})