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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
⊢ (loopyOn E).girth = 1
Tactic:
have _ : RkPos (loopyOn E)✶ := by rw [loopyOn_dual_eq]; exact freeOn_rkPos hE
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth = 1

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth = 1
Tactic:
refine le_antisymm ?_ (one_le_girth _)
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth ≤ 1

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ (loopyOn E).girth ≤ 1
Tactic:
simp only [girth_le_iff, loopyOn_circuit_iff]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ ∃ C, (∃ e ∈ E, C = {e}) ∧ C.encard ≤ 1

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ ∃ C, (∃ e ∈ E, C = {e}) ∧ C.encard ≤ 1
Tactic:
exact ⟨{hE.some}, ⟨_, hE.some_mem, rfl⟩, by simp⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
⊢ (loopyOn E)✶.RkPos
Tactic:
rw [loopyOn_dual_eq]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
⊢ (freeOn E).RkPos

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
⊢ (freeOn E).RkPos
Tactic:
exact freeOn_rkPos hE
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
hE : E.Nonempty
x✝ : (loopyOn E)✶.RkPos
⊢ {hE.some}.encard ≤ 1
Tactic:
simp
State after:
no goals