Theorem: Matroid.finitary_iff_forall_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 : α
⊢ M.Finitary ↔ ∀ (C : Set α), M.Circuit C → C.Finite
Tactic:
refine ⟨fun _ _ ↦ Circuit.finite, fun h ↦
  ⟨fun I hI ↦ indep_iff_not_dep.2 ⟨fun hd ↦ ?_,fun x hx ↦ ?_⟩⟩ ⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False

case refine_2
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x✝ y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E

State before:
case refine_2
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x✝ y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E
Tactic:
simpa using (hI {x} (by simpa) (finite_singleton _)).subset_ground
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
⊢ False
Tactic:
obtain ⟨C, hCI, hC⟩ := hd.exists_circuit_subset
State after:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
C : Set α
hCI : C ⊆ I
hC : M.Circuit C
⊢ False

State before:
case refine_1.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e f x y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
hd : M.Dep I
C : Set α
hCI : C ⊆ I
hC : M.Circuit C
⊢ False
Tactic:
exact hC.dep.not_indep <| hI _ hCI (h C hC)
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I✝ X K C₁ C₂ R : Set α
e f x✝ y : α
h : ∀ (C : Set α), M.Circuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ {x} ⊆ I
Tactic:
simpa
State after:
no goals