Theorem: Matroid.Partition.conn_dual (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.dual.conn = P.conn
Tactic:
change M✶.conn _ _ = M.conn _ _
State after:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M.conn P.left P.right

State before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M.conn P.left P.right
Tactic:
rw [← P.compl_left, conn_compl_dual, P.compl_left]
State after:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M✶.conn P.left P.right

State before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M✶.conn P.left P.right
Tactic:
rfl
State after:
no goals