Error from the output of `tidy`

Stream: new members

[Stuart Presnell]

I'm working on eliminating the use of finish in order/filter/lift, specifically the use in eventually_lift'_powerset_eventually. I tried commenting out finish and replacing it with tidy, which closes the goal: when the cursor is between tidy and the closing bracket I get goals accomplished 🎉. However, now I also get an error type mismatch at application ᾰ_w ᾰ, attributed to the line of the statement of lemma eventually_lift'_powerset_eventually rather than the line where tidy appears.

Is tidy producing a faulty solution (by duplicating names)? And if so, why is it not being blamed in the error statement?

import order.filter.bases
open set

open_locale classical filter

namespace filter
variables {α : Type*} {β : Type*} {f f₁ f₂ : filter α}

protected def lift (f : filter α) (g : set α → filter β) :=
⨅s ∈ f, g s

protected def lift' (f : filter α) (h : set α → set β) :=
f.lift (𝓟 ∘ h)

lemma eventually_lift'_powerset' {f : filter α} {p : set α → Prop}
  (hp : ∀ ⦃s t⦄, s ⊆ t → p t → p s) :
  (∀ᶠ s in f.lift' powerset, p s) ↔ ∃ s ∈ f, p s := sorry

@[simp] lemma eventually_lift'_powerset_eventually {f g : filter α} {p : α → Prop} :
  (∀ᶠ s in f.lift' powerset, ∀ᶠ x in g, x ∈ s → p x) ↔ ∀ᶠ x in f ⊓ g, p x :=
calc _ ↔ ∃ s ∈ f, ∀ᶠ x in g, x ∈ s → p x :
  eventually_lift'_powerset' $ λ s t hst ht, ht.mono $ λ x hx hs, hx (hst hs)
... ↔ ∃ (s ∈ f) (t ∈ g), ∀ x, x ∈ t → x ∈ s → p x :
  by simp only [eventually_iff_exists_mem]
... ↔ ∀ᶠ x in f ⊓ g, p x : by { rw eventually_inf, tidy }

end filter

[Ruben Van de Velde]

Dunno about the error, but this works:

... ↔ ∀ᶠ x in f ⊓ g, p x : by { rw eventually_inf, simp only [and_comm, mem_inter_iff, ←and_imp] }

[Ruben Van de Velde]

Or

... ↔ ∀ᶠ x in f ⊓ g, p x : by simp only [eventually_inf, and_comm, mem_inter_iff, ←and_imp]

[Stuart Presnell]

Ah, thanks!