have : (1 : ℕ) ≃ 0 := AA.inject ‹coe (1 : ℕ) ≃ coe (0 : ℕ)›
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this : coe 1 ≃ coe 0
⊢ False
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝ : coe 1 ≃ coe 0
this : 1 ≃ 0
⊢ False