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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).Circuit C ↔ M.Circuit C ∧ C ⊆ R
Tactic:
refine' ⟨_, fun h ↦ h.1.circuit_restrict_of_subset h.2⟩
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).Circuit C → M.Circuit C ∧ C ⊆ R

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

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