Theorem: Lean4Axiomatic.Integer.gt_iff_pos_diff (Lean4Axiomatic/Integer/Order.lean)

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

case mpr
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Positive (a - b) → a > b

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ a > b → Positive (a - b)
Tactic:
case mp =>
  intro (_ : b < a)
  show Positive (a - b)
  have (And.intro (_ : b ≤ a) (_ : b ≄ a)) := lt_iff_le_neqv.mp ‹b < a›
  have (Exists.intro (k : ℕ) (_ : a ≃ b + coe k)) :=
    le_iff_add_nat.mp ‹b ≤ a›
  have : a - b ≃ coe k := subR_moveR_addL.mpr ‹a ≃ b + coe k›
  have : a - b ≄ 0 := mt zero_diff_iff_eqv.mp (Rel.symm ‹b ≄ a›)
  have : (k:ℤ) ≄ 0 := AA.neqv_substL ‹a - b ≃ coe k› ‹a - b ≄ 0›
  have : k ≄ 0 := AA.inject ‹coe k ≄ coe (0 : ℕ)›
  have : Positive k := Signed.positive_defn.mpr ‹k ≄ 0›
  have : Positive (a - b) := positive_intro_nat ‹Positive k› ‹a - b ≃ coe k›
  exact this
State after:
no goals

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
⊢ Positive (a - b) → a > b
Tactic:
case mpr =>
  intro (_ : Positive (a - b))
  show b < a
  have
    (Exists.intro (k : ℕ) (And.intro (_ : Positive k) (_ : a - b ≃ coe k)))
      := positive_elim_nat ‹Positive (a - b)›
  apply lt_iff_le_neqv.mpr
  show b ≤ a ∧ b ≄ a
  have : a ≃ b + coe k := subR_moveR_addL.mp ‹a - b ≃ coe k›
  have : b ≤ a := le_iff_add_nat.mpr (Exists.intro k ‹a ≃ b + coe k›)
  have : k ≄ 0 := Signed.positive_defn.mp ‹Positive k›
  have : (k:ℤ) ≄ ((0:ℕ):ℤ) := AA.subst₁ ‹k ≄ 0›
  have : a - b ≄ 0 :=
    AA.neqv_substL (Rel.symm ‹a - b ≃ coe k›) ‹(coe k : ℤ) ≄ 0›
  have : b ≄ a := Rel.symm (mt zero_diff_iff_eqv.mpr ‹a - b ≄ 0›)
  exact And.intro ‹b ≤ a› ‹b ≄ a›
State after:
no goals

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

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
⊢ Positive (a - b)
Tactic:
have (And.intro (_ : b ≤ a) (_ : b ≄ a)) := lt_iff_le_neqv.mp ‹b < a›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
⊢ Positive (a - b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
⊢ Positive (a - b)
Tactic:
have (Exists.intro (k : ℕ) (_ : a ≃ b + coe k)) :=
  le_iff_add_nat.mp ‹b ≤ a›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
⊢ Positive (a - b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
⊢ Positive (a - b)
Tactic:
have : a - b ≃ coe k := subR_moveR_addL.mpr ‹a ≃ b + coe k›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this : a - b ≃ coe k
⊢ Positive (a - b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this : a - b ≃ coe k
⊢ Positive (a - b)
Tactic:
have : a - b ≄ 0 := mt zero_diff_iff_eqv.mp (Rel.symm ‹b ≄ a›)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝ : a - b ≃ coe k
this : a - b ≄ 0
⊢ Positive (a - b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝ : a - b ≃ coe k
this : a - b ≄ 0
⊢ Positive (a - b)
Tactic:
have : (k:ℤ) ≄ 0 := AA.neqv_substL ‹a - b ≃ coe k› ‹a - b ≄ 0›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝¹ : a - b ≃ coe k
this✝ : a - b ≄ 0
this : coe k ≄ 0
⊢ Positive (a - b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝¹ : a - b ≃ coe k
this✝ : a - b ≄ 0
this : coe k ≄ 0
⊢ Positive (a - b)
Tactic:
have : k ≄ 0 := AA.inject ‹coe k ≄ coe (0 : ℕ)›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝² : a - b ≃ coe k
this✝¹ : a - b ≄ 0
this✝ : coe k ≄ 0
this : k ≄ 0
⊢ Positive (a - b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝² : a - b ≃ coe k
this✝¹ : a - b ≄ 0
this✝ : coe k ≄ 0
this : k ≄ 0
⊢ Positive (a - b)
Tactic:
have : Positive k := Signed.positive_defn.mpr ‹k ≄ 0›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝³ : a - b ≃ coe k
this✝² : a - b ≄ 0
this✝¹ : coe k ≄ 0
this✝ : k ≄ 0
this : Positive k
⊢ Positive (a - b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝³ : a - b ≃ coe k
this✝² : a - b ≄ 0
this✝¹ : coe k ≄ 0
this✝ : k ≄ 0
this : Positive k
⊢ Positive (a - b)
Tactic:
have : Positive (a - b) := positive_intro_nat ‹Positive k› ‹a - b ≃ coe k›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝⁴ : a - b ≃ coe k
this✝³ : a - b ≄ 0
this✝² : coe k ≄ 0
this✝¹ : k ≄ 0
this✝ : Positive k
this : Positive (a - b)
⊢ Positive (a - b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝⁴ : a - b ≃ coe k
this✝³ : a - b ≄ 0
this✝² : coe k ≄ 0
this✝¹ : k ≄ 0
this✝ : Positive k
this : Positive (a - b)
⊢ Positive (a - b)
Tactic:
exact this
State after:
no goals

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

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
⊢ a > b
Tactic:
show b < a
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
⊢ b < a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
⊢ b < a
Tactic:
have
  (Exists.intro (k : ℕ) (And.intro (_ : Positive k) (_ : a - b ≃ coe k)))
    := positive_elim_nat ‹Positive (a - b)›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
⊢ b < a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
⊢ b < a
Tactic:
apply lt_iff_le_neqv.mpr
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
⊢ b ≤ a ∧ b ≄ a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : a ≃ b + coe k := subR_moveR_addL.mp ‹a - b ≃ coe k›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this : a ≃ b + coe k
⊢ b ≤ a ∧ b ≄ a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this : a ≃ b + coe k
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : b ≤ a := le_iff_add_nat.mpr (Exists.intro k ‹a ≃ b + coe k›)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝ : a ≃ b + coe k
this : b ≤ a
⊢ b ≤ a ∧ b ≄ a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝ : a ≃ b + coe k
this : b ≤ a
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : k ≄ 0 := Signed.positive_defn.mp ‹Positive k›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝¹ : a ≃ b + coe k
this✝ : b ≤ a
this : k ≄ 0
⊢ b ≤ a ∧ b ≄ a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝¹ : a ≃ b + coe k
this✝ : b ≤ a
this : k ≄ 0
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : (k:ℤ) ≄ ((0:ℕ):ℤ) := AA.subst₁ ‹k ≄ 0›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝² : a ≃ b + coe k
this✝¹ : b ≤ a
this✝ : k ≄ 0
this : coe k ≄ coe 0
⊢ b ≤ a ∧ b ≄ a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝² : a ≃ b + coe k
this✝¹ : b ≤ a
this✝ : k ≄ 0
this : coe k ≄ coe 0
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : a - b ≄ 0 :=
  AA.neqv_substL (Rel.symm ‹a - b ≃ coe k›) ‹(coe k : ℤ) ≄ 0›
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝³ : a ≃ b + coe k
this✝² : b ≤ a
this✝¹ : k ≄ 0
this✝ : coe k ≄ coe 0
this : a - b ≄ 0
⊢ b ≤ a ∧ b ≄ a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝³ : a ≃ b + coe k
this✝² : b ≤ a
this✝¹ : k ≄ 0
this✝ : coe k ≄ coe 0
this : a - b ≄ 0
⊢ b ≤ a ∧ b ≄ a
Tactic:
have : b ≄ a := Rel.symm (mt zero_diff_iff_eqv.mpr ‹a - b ≄ 0›)
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝⁴ : a ≃ b + coe k
this✝³ : b ≤ a
this✝² : k ≄ 0
this✝¹ : coe k ≄ coe 0
this✝ : a - b ≄ 0
this : b ≄ a
⊢ b ≤ a ∧ b ≄ a

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : Positive (a - b)
k : ℕ
left✝ : Positive k
right✝ : a - b ≃ coe k
this✝⁴ : a ≃ b + coe k
this✝³ : b ≤ a
this✝² : k ≄ 0
this✝¹ : coe k ≄ coe 0
this✝ : a - b ≄ 0
this : b ≄ a
⊢ b ≤ a ∧ b ≄ a
Tactic:
exact And.intro ‹b ≤ a› ‹b ≄ a›
State after:
no goals