## Stream: general

### Topic: Another bug in calc

#### Yury G. Kudryashov (Mar 14 2021 at 06:18):

The following #mwe fails:

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


#### Mario Carneiro (Mar 14 2021 at 06:44):

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 (Mar 14 2021 at 06:44):

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

#### Mario Carneiro (Mar 14 2021 at 06:45):

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

#### Yury G. Kudryashov (Mar 14 2021 at 07:40):

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

Last updated: May 08 2021 at 03:17 UTC