Theorem: Matroid.ConnectedTo.trans (Matroid/Connectivity.lean)

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₂
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₂

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
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₂

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₂
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₂

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₁
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₂

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₂
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₂

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₁)
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₂

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₁)
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₂

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₁]))
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₂

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
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₂

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
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₂

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
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₂

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₂
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₂

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]
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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₁]
State after:
no goals

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]
State after:
no goals

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])
State after:
no goals

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]
State after:
no goals

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₁⟩
State after:
no goals