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

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

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