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

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 c a) (g c' a)) →
        r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (foldl (fun acc a => f acc a) (f a a✝) l) (foldl (fun acc a => g acc a) (g b a✝) l)

Tactic:
apply ih

Result:
case cons.h
α : 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 c a) (g c' a)) →
        r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (f a a✝) (g b a✝)

case cons.h'
α : 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 c a) (g c' a)) →
        r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)

Proof state:
case cons.h'
α : 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 c a) (g c' a)) →
        r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)

Tactic:
exact 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 c a) (g c' a)) →
        r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (foldl (fun acc a => f acc a) a (a✝ :: l)) (foldl (fun acc a => g acc a) b (a✝ :: l))

Tactic:
simp only [foldl_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 c a) (g c' a)) →
        r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (foldl (fun acc a => f acc a) (f a a✝) l) (foldl (fun acc a => g acc a) (g b a✝) l)

Proof state:
case cons.h
α : 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 c a) (g c' a)) →
        r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)
a b : β
h : r a b
h' : ∀ (a : α), a ∈ a✝ :: l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
⊢ r (f a a✝) (g b a✝)

Tactic:
simp_all

Result:
no goals

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 c a) (g c' a)
⊢ r (foldl (fun acc a => f acc a) a []) (foldl (fun acc a => g acc a) b [])

Tactic:
simp_all

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 c a) (g c' a)) →
        r (foldl (fun acc a => f acc a) a l) (foldl (fun acc a => g acc a) b l)
a✝ b : β
h✝ : r a✝ b
h' : ∀ (a : α), a ∈ a✝¹ :: l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)
a : α
m : a ∈ l
c c' : β
h : r c c'
⊢ a ∈ a✝¹ :: l

Tactic:
simp_all

Result:
no goals