lean stuck trying to use isosceles triangle theorem

Stream: general

[David Renshaw]

When I ask Lean to typecheck this program, it gets stuck for a very long time (maybe forever):

import geometry.euclidean.triangle
open_locale euclidean_geometry

theorem angles_equal
    (A C D: euclidean_space ℝ (fin 2))
    (H : dist A D = dist C D) :
    ∠ D A C = ∠ D C A :=
begin
  have := euclidean_geometry.angle_eq_angle_of_dist_eq H,
  sorry
end

Am I doing something wrong? Is this a known bug?

[David Renshaw]

Hm... ok, so it works fine if I change the order of the points in the H hypothesis, like this:

(H : dist D A = dist D C)

[David Renshaw]

but I'm still puzzled about why it behaves so badly when I get the order wrong

[Kevin Buzzard]

docs#euclidean_geometry.angle_eq_angle_of_dist_eq

[Kevin Buzzard]

Lean is trying to construct a proof that A=C the first time, because you've fed H into a function which is expecting an input of the form dist X Y = dist X Z. Although why it doesn't give up is not a question I can answer.

[Kevin Buzzard]

Maybe the types of A and C are really complicated if you unravel everything

[Yakov Pechersky]

Yeah they're pretty complicated, euclidean_space is just a type synonym with a different metric on it than regular pi types.