Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hf : ¬M.Coloop f
hB : M.Base (insert e I)
⊢ M.ConnectedTo e f
Tactic:
simp only [hB.mem_coloop_iff_forall_not_mem_fundCct (.inr hfI), mem_diff, mem_insert_iff, not_or,
  and_imp, not_forall, Classical.not_imp, not_not, exists_prop, exists_and_left] at hf
State after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
hf : ∃ x ∈ M.E, ¬x = e ∧ x ∉ I ∧ f ∈ M.fundCct x (insert e I)
⊢ M.ConnectedTo e f

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
hf : ∃ x ∈ M.E, ¬x = e ∧ x ∉ I ∧ f ∈ M.fundCct x (insert e I)
⊢ M.ConnectedTo e f
Tactic:
obtain ⟨x, hx, hxe, hxI, hfC⟩ := hf
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ M.ConnectedTo e f

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ M.ConnectedTo e f
Tactic:
have hxi : M.Indep ((insert x I) \ {e}) := by
  rw [diff_singleton_eq_self (by simp [Ne.symm hxe, heI.2]), hI.insert_indep_iff_of_not_mem hxI,
    hI'.flat.cl]
  exact ⟨hx, hxI⟩
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
⊢ M.ConnectedTo e f

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
⊢ M.ConnectedTo e f
Tactic:
have hC := Base.fundCct_circuit hB (show x ∈ M.E \ insert e I by simp [hx, hxI, hxe])
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
⊢ M.ConnectedTo e f

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
⊢ M.ConnectedTo e f
Tactic:
refine hC.mem_connectedTo_mem (by_contra fun heC ↦ ?_) hfC
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
heC : e ∉ M.fundCct x (insert e I)
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
heC : e ∉ M.fundCct x (insert e I)
⊢ False
Tactic:
have hss := subset_diff_singleton (fundCct_subset_insert x (insert e I)) heC
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
heC : e ∉ M.fundCct x (insert e I)
hss : M.fundCct x (insert e I) ⊆ insert x (insert e I) \ {e}
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
heC : e ∉ M.fundCct x (insert e I)
hss : M.fundCct x (insert e I) ⊆ insert x (insert e I) \ {e}
⊢ False
Tactic:
simp only [insert_comm, mem_singleton_iff, insert_diff_of_mem] at hss
State after:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
heC : e ∉ M.fundCct x (insert e I)
hss : M.fundCct x (insert e I) ⊆ insert x I \ {e}
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
hC : M.Circuit (M.fundCct x (insert e I))
heC : e ∉ M.fundCct x (insert e I)
hss : M.fundCct x (insert e I) ⊆ insert x I \ {e}
⊢ False
Tactic:
exact hC.dep.not_indep (hxi.subset hss)
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hf : ¬M.Coloop f
⊢ M.Base (insert e I)
Tactic:
refine Indep.base_of_spanning ?_ (hI'.spanning_of_ssuperset (ssubset_insert heI.2))
State after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hf : ¬M.Coloop f
⊢ M.Indep (insert e I)

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hf : ¬M.Coloop f
⊢ M.Indep (insert e I)
Tactic:
rwa [hI.insert_indep_iff_of_not_mem heI.2, hI'.flat.cl]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ M.Indep (insert x I \ {e})
Tactic:
rw [diff_singleton_eq_self (by simp [Ne.symm hxe, heI.2]), hI.insert_indep_iff_of_not_mem hxI,
  hI'.flat.cl]
State after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ x ∈ M.E \ I

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ x ∈ M.E \ I
Tactic:
exact ⟨hx, hxI⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
⊢ e ∉ insert x I
Tactic:
simp [Ne.symm hxe, heI.2]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
I : Set α
hI : M.Indep I
hI' : M.Hyperplane I
heI : e ∈ M.E \ I
hfI : f ∈ I
hB : M.Base (insert e I)
x : α
hx : x ∈ M.E
hxe : ¬x = e
hxI : x ∉ I
hfC : f ∈ M.fundCct x (insert e I)
hxi : M.Indep (insert x I \ {e})
⊢ x ∈ M.E \ insert e I
Tactic:
simp [hx, hxI, hxe]
State after:
no goals