Theorem: Matroid.uniqueBaseOn_circuit_iff (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 α
⊢ (uniqueBaseOn I E).Circuit C ↔ ∃ e ∈ E \ I, C = {e}
Tactic:
simp only [circuit_iff_dep_forall_diff_singleton_indep, uniqueBaseOn_dep_iff,
  uniqueBaseOn_indep_iff', subset_inter_iff, diff_singleton_subset_iff, mem_diff]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ ((C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E) ↔ ∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ ((C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E) ↔ ∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}
Tactic:
refine ⟨fun ⟨⟨⟨e,he⟩, hCI, hCE⟩, h2⟩ ↦ ⟨e, ⟨hCE he, fun heI ↦ hCI ?_⟩, ?_⟩, ?_⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
heI : e ∈ I
⊢ C ⊆ I

case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C = {e}

case refine_3
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}) → (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E

State before:
case refine_3
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
E D : Set α
⊢ (∃ e, (e ∈ E ∧ e ∉ I) ∧ C = {e}) → (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
Tactic:
rintro ⟨e, ⟨heI,heC⟩, rfl⟩
State after:
case refine_3.intro.intro.intro
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
e : α
heI : e ∈ E
heC : e ∉ I
⊢ ({e}.Nonempty ∧ ¬{e} ⊆ I ∧ {e} ⊆ E) ∧ ∀ e_1 ∈ {e}, {e} ⊆ insert e_1 I ∧ {e} ⊆ insert e_1 E

State before:
case refine_3.intro.intro.intro
α : Type u_1
M : Matroid α
C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
e : α
heI : e ∈ E
heC : e ∉ I
⊢ ({e}.Nonempty ∧ ¬{e} ⊆ I ∧ {e} ⊆ E) ∧ ∀ e_1 ∈ {e}, {e} ⊆ insert e_1 I ∧ {e} ⊆ insert e_1 E
Tactic:
simp [heI, heC]
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 : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
heI : e ∈ I
⊢ C ⊆ I
Tactic:
exact (h2 e he).1.trans (insert_subset heI Subset.rfl)
State after:
no goals

State before:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C = {e}
Tactic:
suffices hsub : C.Subsingleton from hsub.eq_singleton_of_mem he
State after:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C.Subsingleton

State before:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
⊢ C.Subsingleton
Tactic:
refine fun f hf f' hf' ↦ by_contra fun hne ↦ hCI ?_
State after:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f✝ x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
f : α
hf : f ∈ C
f' : α
hf' : f' ∈ C
hne : ¬f = f'
⊢ C ⊆ I

State before:
case refine_2
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e✝ f✝ x y : α
E D : Set α
x✝ : (C.Nonempty ∧ ¬C ⊆ I ∧ C ⊆ E) ∧ ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
e : α
he : e ∈ C
hCI : ¬C ⊆ I
hCE : C ⊆ E
h2 : ∀ e ∈ C, C ⊆ insert e I ∧ C ⊆ insert e E
f : α
hf : f ∈ C
f' : α
hf' : f' ∈ C
hne : ¬f = f'
⊢ C ⊆ I
Tactic:
simpa [inter_insert_eq hne] using subset_inter (h2 f hf).1 (h2 f' hf').1
State after:
no goals