Theorem: Lean4Axiomatic.Integer.ord_sgn_inject (Lean4Axiomatic/Integer/Sign.lean)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 0
⊢ -1 ≃ 0
Tactic:
assumption
State after:
no goals

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : -1 ≃ 1
⊢ -1 ≃ 1
Tactic:
assumption
State after:
no goals

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : 0 ≃ -1
⊢ 0 ≃ -1
Tactic:
assumption
State after:
no goals

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : 0 ≃ 1
⊢ 0 ≃ 1
Tactic:
assumption
State after:
no goals

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : 1 ≃ -1
⊢ 1 ≃ -1
Tactic:
assumption
State after:
no goals

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
x✝ : 1 ≃ 0
⊢ 1 ≃ 0
Tactic:
assumption
State after:
no goals