Theorem: Matroid.simple_iff_three_le_girth (Matroid/Simple.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ 3 ≤ M.girth
Tactic:
rw [le_girth_iff]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
⊢ M.Simple ↔ ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
Tactic:
refine ⟨fun h C hC ↦ le_of_not_lt fun hlt ↦ ?_, fun h ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
C : Set α
hC : M.Circuit C
hlt : C.encard < 3
⊢ False

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ M.Simple

State before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ M.Simple
Tactic:
rw [simple_iff_loopless_eq_of_parallel_forall, loopless_iff_forall_circuit, and_iff_left]
State after:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (C : Set α), M.Circuit C → 1 < C.encard

case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (e f : α), M.Parallel e f → e = f

State before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (e f : α), M.Parallel e f → e = f
Tactic:
refine fun e f hef ↦ by_contra fun hne ↦ ?_
State after:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
⊢ False

State before:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
⊢ False
Tactic:
have hcon := (h _ (hef.circuit_of_ne hne)).trans_eq (encard_pair hne)
State after:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
hcon : 3 ≤ 2
⊢ False

State before:
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
hcon : 3 ≤ 2
⊢ False
Tactic:
norm_num at hcon
State after:
no goals

State before:
case refine_1
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Simple
C : Set α
hC : M.Circuit C
hlt : C.encard < 3
⊢ False
Tactic:
exact hC.dep.not_indep <| indep_of_encard_le_two (ENat.le_of_lt_add_one hlt)
State after:
no goals

State before:
case refine_2
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
⊢ ∀ (C : Set α), M.Circuit C → 1 < C.encard
Tactic:
exact fun C hC ↦ (show (1 : ℕ∞) < 3 from Nat.one_lt_ofNat).trans_le (h C hC)
State after:
no goals