-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} (r : β → β → Prop)
    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
    r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b)

Proof state:
case nil
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a b : β
h : r a b
h' : ∀ (a : α), a ∈ [] → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (foldr (fun a acc => f a acc) a []) (foldr (fun a acc => g a acc) b [])

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.a
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a✝ : α
l : List α
ih :
  ∀ {a b : β},
    r a b →
      (∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) →
        r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ a✝ ∈ a✝ :: l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a✝¹ : α
l : List α
ih :
  ∀ {a b : β},
    r a b →
      (∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) →
        r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)
a✝ b : β
h✝ : r a✝ b
h' : ∀ (a : α), a ∈ a✝¹ :: l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
a : α
m : a ∈ l
c c' : β
h : r c c'
⊢ a ∈ a✝¹ :: l

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.a
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a✝ : α
l : List α
ih :
  ∀ {a b : β},
    r a b →
      (∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) →
        r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)

Tactic:
exact ih h fun a m c c' h => h' _ (by simp_all) _ _ h

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a✝ : α
l : List α
ih :
  ∀ {a b : β},
    r a b →
      (∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) →
        r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (f a✝ (foldr (fun a acc => f a acc) a l)) (g a✝ (foldr (fun a acc => g a acc) b l))

Tactic:
apply h'

Result:
case cons.a
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a✝ : α
l : List α
ih :
  ∀ {a b : β},
    r a b →
      (∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) →
        r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ a✝ ∈ a✝ :: l

case cons.a
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a✝ : α
l : List α
ih :
  ∀ {a b : β},
    r a b →
      (∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) →
        r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)

Proof state:
case cons
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a✝ : α
l : List α
ih :
  ∀ {a b : β},
    r a b →
      (∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) →
        r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (foldr (fun a acc => f a acc) a (a✝ :: l)) (foldr (fun a acc => g a acc) b (a✝ :: l))

Tactic:
simp only [foldr_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f g : α → β → β
r : β → β → Prop
a✝ : α
l : List α
ih :
  ∀ {a b : β},
    r a b →
      (∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) →
        r (foldr (fun a acc => f a acc) a l) (foldr (fun a acc => g a acc) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f a c) (g a c')
⊢ r (f a✝ (foldr (fun a acc => f a acc) a l)) (g a✝ (foldr (fun a acc => g a acc) b l))