Theorem: Lean4Axiomatic.Natural.Impl.Nat.compare_substR (Lean4Axiomatic/Natural/Impl/Nat.lean)

State before:
n₁ n₂ m : Nat
⊢ n₁ ≃ n₂ → compare m n₁ = compare m n₂
Tactic:
intro (_ : n₁ ≃ n₂)
State after:
n₁ n₂ m : Nat
x✝ : n₁ ≃ n₂
⊢ compare m n₁ = compare m n₂

State before:
n₁ n₂ m : Nat
x✝ : n₁ ≃ n₂
⊢ compare m n₁ = compare m n₂
Tactic:
rw [‹n₁ ≃ n₂›]
State after:
no goals