## Stream: general

### Topic: strange bug, maybe a diamond?

#### Heather Macbeth (Aug 12 2021 at 19:20):

In the following example, abel fails, and I'm guessing it's a symptom that two things which look equal in the goal state are different at some lower level. I'm having trouble minimizing it, though. Can anyone diagnose it?

import analysis.normed_space.inner_product

variables {V : Type*} [inner_product_space ℝ V] (s : submodule ℝ V) [complete_space s]

include s

-- fails
example (x : V) : true :=
begin
let w := _root_.orthogonal_projection s x,
let v := x - (w:V),
have : bit0 (s.subtype (_root_.orthogonal_projection s x)) - x = (w:V) - v,
{ simp [bit0],
dsimp [w, v],
abel, -- left with a goal which looks like it should be in the scope of abel

},
end

-- works
example (x : V) : true :=
begin
let w : s := _root_.orthogonal_projection s x,
let v := x - (w:V),
have : bit0 (s.subtype (_root_.orthogonal_projection s x)) - x = (w:V) - v,
{ simp [bit0],
dsimp [w, v],
abel },
end


#### Heather Macbeth (Aug 12 2021 at 19:21):

The difference between the working and non-working examples is that in the working one, the type of w is specified:

  let w : s := _root_.orthogonal_projection s x,


#### Rob Lewis (Aug 12 2021 at 19:31):

This is fixed by @Anne Baanen 's #8628 so I think your guess is correct

#### Anne Baanen (Aug 12 2021 at 20:22):

Heh, perfect timing! :grinning_face_with_smiling_eyes:

Last updated: Dec 20 2023 at 11:08 UTC