Theorem: Lean4Axiomatic.Integer.zero_diff_iff_eqv (Lean4Axiomatic/Integer/Subtraction.lean)

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a - b ≃ 0 ↔ a ≃ b
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a - b ≃ 0 → a ≃ b

case mpr
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a ≃ b → a - b ≃ 0

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a - b ≃ 0 → a ≃ b
Tactic:
case mp =>
  intro (_ : a - b ≃ 0)
  show a ≃ b
  calc
    a            ≃ _ := Rel.symm AA.identR
    a + 0        ≃ _ := AA.substR (Rel.symm AA.inverseL)
    a + (-b + b) ≃ _ := Rel.symm AA.assoc
    (a + -b) + b ≃ _ := AA.substL (Rel.symm sub_defn)
    (a - b) + b  ≃ _ := AA.substL ‹a - b ≃ 0›
    0 + b        ≃ _ := AA.identL
    b            ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a ≃ b → a - b ≃ 0
Tactic:
case mpr =>
  intro (_ : a ≃ b)
  show a - b ≃ 0
  calc
    a - b  ≃ _ := AA.substL ‹a ≃ b›
    b - b  ≃ _ := sub_same
    0      ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a - b ≃ 0 → a ≃ b
Tactic:
intro (_ : a - b ≃ 0)
State after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
x✝ : a - b ≃ 0
⊢ a ≃ b

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
x✝ : a - b ≃ 0
⊢ a ≃ b
Tactic:
calc
  a            ≃ _ := Rel.symm AA.identR
  a + 0        ≃ _ := AA.substR (Rel.symm AA.inverseL)
  a + (-b + b) ≃ _ := Rel.symm AA.assoc
  (a + -b) + b ≃ _ := AA.substL (Rel.symm sub_defn)
  (a - b) + b  ≃ _ := AA.substL ‹a - b ≃ 0›
  0 + b        ≃ _ := AA.identL
  b            ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
⊢ a ≃ b → a - b ≃ 0
Tactic:
intro (_ : a ≃ b)
State after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
x✝ : a ≃ b
⊢ a - b ≃ 0

State before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b : ℤ
x✝ : a ≃ b
⊢ a - b ≃ 0
Tactic:
calc
  a - b  ≃ _ := AA.substL ‹a ≃ b›
  b - b  ≃ _ := sub_same
  0      ≃ _ := Rel.refl
State after:
no goals