-- Mathlib/Data/List/Chain.lean
theorem chain'_attachWith {l : List α} {p : α → Prop} (h : ∀ x ∈ l, p x)
    {r : {a // p a} → {a // p a} → Prop} :
    (l.attachWith p h).Chain' r ↔ l.Chain' fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩

Proof state:
case nil
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
h : ∀ (x : α), x ∈ [] → p x
⊢ Chain' r ([].attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
⊢ (∀ (y : { a // p a }), (y ∈ l.head?.pbind fun a_1 h_1 => some ⟨a_1, ⋯⟩) → r ⟨a, ⋯⟩ y) ↔
    ∀ (y : α), y ∈ l.head? → ∃ ha hb, r ⟨a, ha⟩ ⟨y, hb⟩

Tactic:
constructor <;>
intro hc b (hb : _ = _)

Result:
case cons.mp
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
hc : ∀ (y : { a // p a }), (y ∈ l.head?.pbind fun a_1 h_1 => some ⟨a_1, ⋯⟩) → r ⟨a, ⋯⟩ y
b : α
hb : l.head? = some b
⊢ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩

case cons.mpr
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
hc : ∀ (y : α), y ∈ l.head? → ∃ ha hb, r ⟨a, ha⟩ ⟨y, hb⟩
b : { a // p a }
hb : (l.head?.pbind fun a_1 h_1 => some ⟨a_1, ⋯⟩) = some b
⊢ r ⟨a, ⋯⟩ b

Proof state:
case cons.mpr
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
hc : ∀ (y : α), y ∈ l.head? → ∃ ha hb, r ⟨a, ha⟩ ⟨y, hb⟩
b : { a // p a }
hb : (l.head?.pbind fun a_1 h_1 => some ⟨a_1, ⋯⟩) = some b
⊢ r ⟨a, ⋯⟩ b

Tactic:
cases l <;> aesop

Result:
no goals

Proof state:
case cons
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
⊢ Chain' r ((a :: l).attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) (a :: l)

Tactic:
rw [attachWith_cons, chain'_cons', chain'_cons', IH, and_congr_left]

Result:
case cons
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
⊢ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l →
    ((∀ (y : { a // p a }), y ∈ (l.attachWith p ⋯).head? → r ⟨a, ⋯⟩ y) ↔
      ∀ (y : α), y ∈ l.head? → ∃ ha hb, r ⟨a, ha⟩ ⟨y, hb⟩)

Proof state:
case cons.mp
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
b : α
hb : l.head? = some b
hc : ∀ (y : { a // p a }), y ∈ some ⟨b, ⋯⟩ → r ⟨a, ⋯⟩ y
⊢ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
have hb' := h b (mem_cons_of_mem a (mem_of_mem_head? hb))

Result:
case cons.mp
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
b : α
hb : l.head? = some b
hc : ∀ (y : { a // p a }), y ∈ some ⟨b, ⋯⟩ → r ⟨a, ⋯⟩ y
hb' : p b
⊢ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩

Proof state:
case cons
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
⊢ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l →
    ((∀ (y : { a // p a }), (y ∈ l.head?.pbind fun a_2 h_1 => some ⟨a_2, ⋯⟩) → r ⟨a, ⋯⟩ y) ↔
      ∀ (y : α), y ∈ l.head? → ∃ ha hb, r ⟨a, ha⟩ ⟨y, hb⟩)

Tactic:
intros

Result:
case cons
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
⊢ (∀ (y : { a // p a }), (y ∈ l.head?.pbind fun a_1 h_1 => some ⟨a_1, ⋯⟩) → r ⟨a, ⋯⟩ y) ↔
    ∀ (y : α), y ∈ l.head? → ∃ ha hb, r ⟨a, ha⟩ ⟨y, hb⟩

Proof state:
case cons
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
⊢ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l →
    ((∀ (y : { a // p a }), y ∈ (l.attachWith p ⋯).head? → r ⟨a, ⋯⟩ y) ↔
      ∀ (y : α), y ∈ l.head? → ∃ ha hb, r ⟨a, ha⟩ ⟨y, hb⟩)

Tactic:
simp_rw [head?_attachWith]

Result:
case cons
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
⊢ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l →
    ((∀ (y : { a // p a }), (y ∈ l.head?.pbind fun a_2 h_1 => some ⟨a_2, ⋯⟩) → r ⟨a, ⋯⟩ y) ↔
      ∀ (y : α), y ∈ l.head? → ∃ ha hb, r ⟨a, ha⟩ ⟨y, hb⟩)

Proof state:
case cons.mp
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
b : α
hb : l.head? = some b
hc : ∀ (y : { a // p a }), y ∈ some ⟨b, ⋯⟩ → r ⟨a, ⋯⟩ y
hb' : p b
⊢ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
exact ⟨h a (mem_cons_self a l), hb', hc ⟨b, hb'⟩ rfl⟩

Result:
no goals

Proof state:
case cons.mp
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
hc : ∀ (y : { a // p a }), (y ∈ l.head?.pbind fun a_1 h_1 => some ⟨a_1, ⋯⟩) → r ⟨a, ⋯⟩ y
b : α
hb : l.head? = some b
⊢ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp_rw [hb, Option.pbind_some] at hc

Result:
case cons.mp
α : Type u
p : α → Prop
r : { a // p a } → { a // p a } → Prop
a : α
l : List α
IH : ∀ (h : ∀ (x : α), x ∈ l → p x), Chain' r (l.attachWith p h) ↔ Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
h : ∀ (x : α), x ∈ a :: l → p x
a✝ : Chain' (fun a b => ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l
b : α
hb : l.head? = some b
hc : ∀ (y : { a // p a }), y ∈ some ⟨b, ⋯⟩ → r ⟨a, ⋯⟩ y
⊢ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩