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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
⊢ C = M.fundCct e I
Tactic:
have heI : e ∉ I := by
  intro heI; rw [insert_eq_of_mem heI] at hCI; exact (hC.dep.superset hCI).not_indep hI
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
⊢ C = M.fundCct e I

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
⊢ C = M.fundCct e I
Tactic:
have heC : e ∈ C := by
  refine' by_contra fun heC ↦ (hI.subset _).not_dep hC.dep
  rwa [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self heC] at hCI
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ C = M.fundCct e I

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ C = M.fundCct e I
Tactic:
have he : e ∈ M.cl I := by
  rw [mem_cl_iff_exists_circuit_of_not_mem heI]; exact ⟨C, hC, heC, hCI⟩
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
⊢ C = M.fundCct e I

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
⊢ C = M.fundCct e I
Tactic:
by_contra! hne
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
⊢ False

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
⊢ False
Tactic:
obtain ⟨Cf, hCf, hCfss⟩ := hC.elimination (hI.fundCct_circuit ⟨he,heI⟩) hne e
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ False

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ False
Tactic:
refine' hCf.dep.not_indep (hI.subset (hCfss.trans _))
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ (C ∪ M.fundCct e I) \ {e} ⊆ I

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ (C ∪ M.fundCct e I) \ {e} ⊆ I
Tactic:
rw [diff_subset_iff, singleton_union, union_subset_iff, and_iff_right hCI]
State after:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ M.fundCct e I ⊆ insert e I

State before:
case intro.intro
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
he : e ∈ M.cl I
hne : C ≠ M.fundCct e I
Cf : Set α
hCf : M.Circuit Cf
hCfss : Cf ⊆ (C ∪ M.fundCct e I) \ {e}
⊢ M.fundCct e I ⊆ insert e I
Tactic:
exact fundCct_subset_insert _ _
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
⊢ e ∉ I
Tactic:
intro heI
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∈ I
⊢ False

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∈ I
⊢ False
Tactic:
rw [insert_eq_of_mem heI] at hCI
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ I
heI : e ∈ I
⊢ False

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ I
heI : e ∈ I
⊢ False
Tactic:
exact (hC.dep.superset hCI).not_indep hI
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
⊢ e ∈ C
Tactic:
refine' by_contra fun heC ↦ (hI.subset _).not_dep hC.dep
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∉ C
⊢ C ⊆ I

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∉ C
⊢ C ⊆ I
Tactic:
rwa [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self heC] at hCI
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ e ∈ M.cl I
Tactic:
rw [mem_cl_iff_exists_circuit_of_not_mem heI]
State after:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e I

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
hC : M.Circuit C
hI : M.Indep I
hCI : C ⊆ insert e I
heI : e ∉ I
heC : e ∈ C
⊢ ∃ C, M.Circuit C ∧ e ∈ C ∧ C ⊆ insert e I
Tactic:
exact ⟨C, hC, heC, hCI⟩
State after:
no goals