Theorem: Matroid.circuitOn_dep_iff (Matroid/Constructions/Truncate.lean)

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ (circuitOn C).Dep D ↔ D = C
Tactic:
simp only [Dep, circuitOn_indep_iff hC, ssubset_iff_subset_ne, ne_eq, not_and, not_not,
  circuitOn_ground]
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ (D ⊆ C → D = C) ∧ D ⊆ C ↔ D = C

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ (D ⊆ C → D = C) ∧ D ⊆ C ↔ D = C
Tactic:
exact ⟨fun h ↦ h.1 h.2, by rintro rfl; simp [Subset.rfl]⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ D = C → (D ⊆ C → D = C) ∧ D ⊆ C
Tactic:
rintro rfl
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
D : Set α
hC : D.Nonempty
⊢ (D ⊆ D → D = D) ∧ D ⊆ D

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
D : Set α
hC : D.Nonempty
⊢ (D ⊆ D → D = D) ∧ D ⊆ D
Tactic:
simp [Subset.rfl]
State after:
no goals