Type class inference failed even though instance exists

Stream: mathlib4

[Andrey Yao]

import Mathlib.Order.Defs
import Mathlib.Order.BooleanAlgebra
import Mathlib.Order.Lattice

instance : BoundedOrder Bool := by infer_instance

lemma list_fold_lattice_bot {α β : Type} [DistribLattice α] [BoundedOrder α] :
  ∀ (f : β -> α) (l : List β), List.foldl (fun acc e => acc ⊓ f e) ⊥ l = ⊥ := by
  intros f l
  induction l with
  | nil => rfl
  | cons hd tl IH => simp; exact IH

lemma list_fold_true_impl_forall_true {β : Type} :
  ∀ (f : β -> Bool) (l : List β), List.foldl (fun acc e => acc ⊓ f e) ⊤ l = ⊤ →
  ∀ e ∈ l, f e = ⊤ := by
  intros f l eq; induction l with
  | nil => simp
  | cons hd tl IHtl => simp; cases val : (f hd) with
    | true => aesop
    | false =>
      simp at eq; apply And.intro
      . rw [val] at eq; rw [<- list_fold_lattice_bot f tl] at eq
      . rw [val, list_fold_lattice_bot] at eq; apply IHtl eq

Hello! I am trying to prove the lemma list_fold_true_impl_forall_true, but at the second to last line, Lean4 complains that tactic 'rewrite' failed, did not find instance of the pattern in the target expression ⊥, even though there is one. How would one go about fixing/debuggin these typeclass inference-related errors? Thanks

[Damiano Testa]

I think that rw is just telling you that it cannot find ⊥ in your expression. If you get it to be there, then your next rw seems to work: try adding

rw [← bot_eq_false] at eq

to make Lean represent false as ⊥.

[Ruben Van de Velde]

Why are you using lattice operations on booleans anyway?

[Andrey Yao]

Damiano Testa said:

I think that rw is just telling you that it cannot find ⊥ in your expression. If you get it to be there, then your next rw seems to work: try adding

rw [← bot_eq_false] at eq

to make Lean represent false as ⊥.

Thanks! It worked by adding some rewrites

[Andrey Yao]

Ruben Van de Velde said:

Why are you using lattice operations on booleans anyway?

I'm trying to prove some more general results using bounded distributive lattices, and the boolean one is just one of the examples