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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
⊢ C.Finite
Tactic:
have hi := hC.dep.not_indep
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ¬M.Indep C
⊢ C.Finite

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ¬M.Indep C
⊢ C.Finite
Tactic:
rw [indep_iff_forall_finite_subset_indep] at hi
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite
Tactic:
push_neg at hi
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
⊢ C.Finite

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
⊢ C.Finite
Tactic:
obtain ⟨J, hJC, hJfin, hJ⟩ := hi
State after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite

State before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
inst✝ : M.Finitary
hC : M.Circuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite
Tactic:
rwa [← hC.eq_of_not_indep_subset hJ hJC]
State after:
no goals