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

State before:
α : Type u_1
M✝ : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
inst✝ : M✶.RkPos
⊢ ∃ C, M.Circuit C ∧ C.encard = M.girth
Tactic:
obtain ⟨⟨C,hC⟩, (hC' : C.encard = _)⟩ :=
  @ciInf_mem ℕ∞ (setOf M.Circuit) _ _ (nonempty_coe_sort.mpr M.exists_circuit)
    (fun C ↦ (C : Set α).encard)
State after:
case intro.mk
α : Type u_1
M✝ : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
inst✝ : M✶.RkPos
C : Set α
hC : C ∈ setOf M.Circuit
hC' : C.encard = ⨅ C, (↑C).encard
⊢ ∃ C, M.Circuit C ∧ C.encard = M.girth

State before:
case intro.mk
α : Type u_1
M✝ : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
inst✝ : M✶.RkPos
C : Set α
hC : C ∈ setOf M.Circuit
hC' : C.encard = ⨅ C, (↑C).encard
⊢ ∃ C, M.Circuit C ∧ C.encard = M.girth
Tactic:
exact ⟨C, hC, by rw [hC', girth, iInf_subtype']⟩
State after:
no goals

State before:
α : Type u_1
M✝ : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f x y : α
k : ℕ∞
M : Matroid α
inst✝ : M✶.RkPos
C : Set α
hC : C ∈ setOf M.Circuit
hC' : C.encard = ⨅ C, (↑C).encard
⊢ C.encard = M.girth
Tactic:
rw [hC', girth, iInf_subtype']
State after:
no goals