Gabriel Ebner

We've recently changed `classical` in mathlib to so that it no longer overrides the existing decidable instances. mathlib4 should be adapterd. https://github.com/leanprover-community/mathlib/pull/14122 ```lean import Mathlib.Tactic.Basic example : (by classical; exact...

The `∉` precedence was wrong: https://github.com/leanprover-community/mathlib3port/commit/d3886c253aee234456e6ee149c6a1bea9570c689#r67303397 Other notation probably have the wrong precedence as well.

apply tactic produces incorrect proof

1

```lean def additive (α : Type*) := α instance {α} [has_one α] : has_zero (additive α) := ⟨(1 : α)⟩ example : (0 : ℕ) = (0 : additive ℕ)...

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.236375

Alternative to #152

```lean class foo (n : ℕ) : Prop := (has_true : true) class bar (n : ℕ) : Prop := (has_true : true) @[reducible] def quux := ∀ n [foo...