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

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
⊢ o₁ = o₂ → ord_sgn o₁ ≃ ord_sgn o₂
Tactic:
intro (_ : o₁ = o₂)
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
x✝ : o₁ = o₂
⊢ ord_sgn o₁ ≃ ord_sgn o₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
x✝ : o₁ = o₂
⊢ ord_sgn o₁ ≃ ord_sgn o₂
Tactic:
rw [‹o₁ = o₂›]
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
x✝ : o₁ = o₂
⊢ ord_sgn o₂ ≃ ord_sgn o₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
o₁ o₂ : Ordering
x✝ : o₁ = o₂
⊢ ord_sgn o₂ ≃ ord_sgn o₂
Tactic:
exact Rel.refl
State after:
no goals