Another bug in calc

Stream: general

[Yury G. Kudryashov]

The following #mwe fails:

example {n : ℕ} : n ∈ (univ : set ℕ) :=
calc n ∈ univ : trivial
... ⊆ univ : subset.rfl
... = univ : rfl

[Mario Carneiro]

trans_rel_left appears to only work on relations on the same type

theorem trans_rel_left : ∀ {α : Sort u} {a b c : α} (r : α → α → Prop), r a b → b = c → r a c :=

[Mario Carneiro]

I didn't even know that calc allowed things like a \in b \subset c as trans rules

[Mario Carneiro]

(I suspect the author of calc also didn't)

[Yury G. Kudryashov]

Thanks! I'll look into fixing this tomorrow or on Monday.