Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv (Lean4Axiomatic/Integer/Impl/Difference/Sign.lean)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 ↔ n ≃ m
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → n ≃ m

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n ≃ m → n——m ≃ 0

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → n ≃ m
Tactic:
case mp =>
  intro (_ : n——m ≃ 0)
  show n ≃ m
  have : n——m ≃ 0——0 := ‹n——m ≃ 0›
  have : n + 0 ≃ 0 + m := ‹n——m ≃ 0——0›
  exact Natural.add_swapped_zeros_eqv.mp ‹n + 0 ≃ 0 + m›
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n ≃ m → n——m ≃ 0
Tactic:
case mpr =>
  intro (_ : n ≃ m)
  show n——m ≃ 0
  show n——m ≃ 0——0
  show n + 0 ≃ 0 + m
  exact Natural.add_swapped_zeros_eqv.mpr ‹n ≃ m›
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → n ≃ m
Tactic:
intro (_ : n——m ≃ 0)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
⊢ n ≃ m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
⊢ n ≃ m
Tactic:
have : n——m ≃ 0——0 := ‹n——m ≃ 0›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this : n——m ≃ 0——0
⊢ n ≃ m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this : n——m ≃ 0——0
⊢ n ≃ m
Tactic:
have : n + 0 ≃ 0 + m := ‹n——m ≃ 0——0›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝ : n——m ≃ 0——0
this : n + 0 ≃ 0 + m
⊢ n ≃ m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝ : n——m ≃ 0——0
this : n + 0 ≃ 0 + m
⊢ n ≃ m
Tactic:
exact Natural.add_swapped_zeros_eqv.mp ‹n + 0 ≃ 0 + m›
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n ≃ m → n——m ≃ 0
Tactic:
intro (_ : n ≃ m)
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n——m ≃ 0

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n——m ≃ 0
Tactic:
show n——m ≃ 0——0
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n——m ≃ 0——0

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n——m ≃ 0——0
Tactic:
show n + 0 ≃ 0 + m
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n + 0 ≃ 0 + m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n + 0 ≃ 0 + m
Tactic:
exact Natural.add_swapped_zeros_eqv.mpr ‹n ≃ m›
State after:
no goals