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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hCR : C ⊆ R
⊢ (M ↾ R).Circuit C
Tactic:
simp_rw [circuit_iff, restrict_dep_iff, dep_iff, and_imp] at *
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ R → I ⊆ C → I = C

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hCR : C ⊆ R
hC : (¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C
⊢ (¬M.Indep C ∧ C ⊆ R) ∧ ∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ R → I ⊆ C → I = C
Tactic:
refine' ⟨⟨hC.1.1, hCR⟩, fun I hI _ hIC ↦ hC.2 hI (hIC.trans hC.1.2) hIC⟩
State after:
no goals