internlm/Lean-Github huggingface dataset:
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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
Proof 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
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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
Proof 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
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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)
Proof state after:
no goals
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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))
Proof 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)
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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]
Proof state after:
no goals
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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]
Proof 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
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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⟩
Proof state after:
no goals
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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]
Proof state after:
no goals
Theorem: Matroid.connectedTo_of_indep_hyperplane_of_not_coloop
Proof 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]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
⊢ M.ConnectedTo e₁ e₂
Tactic:
obtain (rfl | hne) := eq_or_ne e₁ e₂
Proof state after:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₁
⊢ M.ConnectedTo e₁ e₁

case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
⊢ M.ConnectedTo e₁ e₂
Tactic:
obtain (rfl | hne₁) := eq_or_ne e₁ f
Proof state after:
case inr.inl
α : Type u_1
M : Matroid α
C K : Set α
e g e₁ e₂ : α
hne : e₁ ≠ e₂
h₁ : M.ConnectedTo e₁ e₁
h₂ : M.ConnectedTo e₁ e₂
⊢ M.ConnectedTo e₁ e₂

case inr.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
⊢ M.ConnectedTo e₁ e₂
Tactic:
obtain (rfl | hne₂) := eq_or_ne f e₂
Proof state after:
case inr.inr.inl
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ : α
h₁ : M.ConnectedTo e₁ f
hne₁ : e₁ ≠ f
h₂ : M.ConnectedTo f f
hne : e₁ ≠ f
⊢ M.ConnectedTo e₁ f

case inr.inr.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
⊢ M.ConnectedTo e₁ e₂
Tactic:
obtain ⟨K₁, hK₁, he₁K₁, hfK₁⟩ := h₁.exists_cocircuit_of_ne hne₁
Proof state after:
case inr.inr.inr.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
⊢ M.ConnectedTo e₁ e₂
Tactic:
obtain ⟨C₂, hC₂, hfC₂, he₂C₂⟩ := h₂.exists_circuit_of_ne hne₂
Proof state after:
case inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
⊢ M.ConnectedTo e₁ e₂
Tactic:
obtain (he₂K₁ | he₂K₁) := em (e₂ ∈ K₁)
Proof state after:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∈ K₁
⊢ M.ConnectedTo e₁ e₂

case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∈ K₁
⊢ M.ConnectedTo e₁ e₂

case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
⊢ M.ConnectedTo e₁ e₂
Tactic:
exact (hK₁.mem_connectedTo_mem he₁K₁ he₂K₁)
Proof state after:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
⊢ M.ConnectedTo e₁ e₂
Tactic:
have hC₂i : M.Indep (C₂ \ K₁) := (hC₂.diff_singleton_indep hfC₂).subset
    (subset_diff_singleton diff_subset (by simp [hfK₁]))
Proof state after:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
⊢ M.ConnectedTo e₁ e₂
Tactic:
have hH := hK₁.compl_hyperplane
Proof state after:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
⊢ M.ConnectedTo e₁ e₂
Tactic:
obtain ⟨J, hJ, he₂J⟩ :=
  hC₂i.subset_basis_of_subset (diff_subset_diff_left hC₂.subset_ground) hH.subset_ground
Proof state after:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ M.ConnectedTo e₁ e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ M.ConnectedTo e₁ e₂
Tactic:
refine (connectedTo_of_indep_hyperplane_of_not_coloop ?_
  (hH.basis_hyperplane_delete hJ) ?_ ?_ ?_).of_delete
Proof state after:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ (M ＼ ((M.E \ K₁) \ J)).Indep J

case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ e₁ ∈ (M ＼ ((M.E \ K₁) \ J)).E \ J

case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_3
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ e₂ ∈ J

case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_4
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ ¬(M ＼ ((M.E \ K₁) \ J)).Coloop e₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_4
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ ¬(M ＼ ((M.E \ K₁) \ J)).Coloop e₂
Tactic:
refine Circuit.not_coloop_of_mem ?_ he₂C₂
Proof state after:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_4
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ (M ＼ ((M.E \ K₁) \ J)).Circuit C₂
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_4
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ (M ＼ ((M.E \ K₁) \ J)).Circuit C₂
Tactic:
rwa [delete_circuit_iff, and_iff_right hC₂, disjoint_iff_inter_eq_empty, ← inter_diff_assoc,
  diff_eq_empty, ← inter_diff_assoc, inter_eq_self_of_subset_left hC₂.subset_ground]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inl
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₁
⊢ M.ConnectedTo e₁ e₁
Tactic:
simp [h₁.mem_ground_left]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inl
α : Type u_1
M : Matroid α
C K : Set α
e g e₁ e₂ : α
hne : e₁ ≠ e₂
h₁ : M.ConnectedTo e₁ e₁
h₂ : M.ConnectedTo e₁ e₂
⊢ M.ConnectedTo e₁ e₂
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inl
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ : α
h₁ : M.ConnectedTo e₁ f
hne₁ : e₁ ≠ f
h₂ : M.ConnectedTo f f
hne : e₁ ≠ f
⊢ M.ConnectedTo e₁ f
Tactic:
assumption
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
⊢ f ∉ C₂ \ K₁
Tactic:
simp [hfK₁]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ (M ＼ ((M.E \ K₁) \ J)).Indep J
Tactic:
simp [disjoint_sdiff_right, hJ.indep]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ e₁ ∈ (M ＼ ((M.E \ K₁) \ J)).E \ J
Tactic:
simpa [h₁.mem_ground_left, he₁K₁] using
  not_mem_subset hJ.subset (by simp [he₁K₁, h₁.mem_ground_left])
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ e₁ ∉ M.E \ K₁
Tactic:
simp [he₁K₁, h₁.mem_ground_left]
Proof state after:
no goals
Theorem: Matroid.ConnectedTo.trans
Proof state before:
case inr.inr.inr.intro.intro.intro.intro.intro.intro.inr.intro.intro.refine_3
α : Type u_1
M : Matroid α
C K : Set α
e f g e₁ e₂ : α
h₁ : M.ConnectedTo e₁ f
h₂ : M.ConnectedTo f e₂
hne : e₁ ≠ e₂
hne₁ : e₁ ≠ f
hne₂ : f ≠ e₂
K₁ : Set α
hK₁ : M.Cocircuit K₁
he₁K₁ : e₁ ∈ K₁
hfK₁ : f ∈ K₁
C₂ : Set α
hC₂ : M.Circuit C₂
hfC₂ : f ∈ C₂
he₂C₂ : e₂ ∈ C₂
he₂K₁ : e₂ ∉ K₁
hC₂i : M.Indep (C₂ \ K₁)
hH : M.Hyperplane (M.E \ K₁)
J : Set α
hJ : M.Basis J (M.E \ K₁)
he₂J : C₂ \ K₁ ⊆ J
⊢ e₂ ∈ J
Tactic:
exact he₂J ⟨he₂C₂, he₂K₁⟩
Proof state after:
no goals
Theorem: Matroid.Connected.to_dual
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
⊢ M✶.Nonempty
Tactic:
have := hM.1
Proof state after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
this : M.Nonempty
⊢ M✶.Nonempty
Theorem: Matroid.Connected.to_dual
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M.Connected
this : M.Nonempty
⊢ M✶.Nonempty
Tactic:
apply dual_nonempty
Proof state after:
no goals
Theorem: Matroid.Connected.of_dual
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
hM : M✶.Connected
⊢ M.Connected
Tactic:
simpa using hM.to_dual
Proof state after:
no goals
Theorem: Matroid.Coloop.not_connected
Proof state before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
he : M.Coloop e
hE : M.E.Nontrivial
⊢ ¬M.Connected
Tactic:
obtain ⟨f, hfE, hfe⟩ := hE.exists_ne e
Proof state after:
case intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
⊢ ¬M.Connected
Theorem: Matroid.Coloop.not_connected
Proof state before:
case intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
⊢ ¬M.Connected
Tactic:
rintro ⟨-, hconn⟩
Proof state after:
case intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
⊢ False
Theorem: Matroid.Coloop.not_connected
Proof state before:
case intro.intro.intro
α : Type u_1
M : Matroid α
C K : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
⊢ False
Tactic:
obtain ⟨K, hK, heK, -⟩ := (hconn he.mem_ground hfE).exists_circuit_of_ne hfe.symm
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
M : Matroid α
C K✝ : Set α
e f✝ g : α
he : M.Coloop e
hE : M.E.Nontrivial
f : α
hfE : f ∈ M.E
hfe : f ≠ e
hconn : ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.ConnectedTo e f
K : Set α
hK : M.Circuit K
heK : e ∈ K
⊢ False