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

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
C' : Set α
⊢ (circuitOn C).Circuit C' ↔ C' = C
Tactic:
refine ⟨fun h ↦ h.eq_of_subset_circuit (circuitOn_ground_circuit hC) h.subset_ground, ?_⟩
State after:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
C' : Set α
⊢ C' = C → (circuitOn C).Circuit C'

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

State before:
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C' : Set α
hC : C'.Nonempty
⊢ (circuitOn C').Circuit C'
Tactic:
exact circuitOn_ground_circuit hC
State after:
no goals