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

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) ↔ n > m
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) → n > m

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n > m → Positive (n——m)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) → n > m
Tactic:
case mp =>
  intro (_ : Positive (n——m))
  have
    (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : n——m ≃ 1 * coe k))
      := Generic.positive_iff_sign_pos1.mp ‹Positive (n——m)›
  show m < n
  apply neg_diff_lt.mp
  show Negative (m——n)
  apply Generic.negative_iff_sign_neg1.mpr
  show NonzeroWithSign (m——n) (-1)
  apply NonzeroWithSign.intro k ‹Positive k›
  show m——n ≃ -1 * coe k
  calc
    m——n           ≃ _ := Rel.symm neg_involutive
    (-(-(m——n)))   ≃ _ := Rel.refl
    (-(n——m))      ≃ _ := AA.subst₁ ‹n——m ≃ 1 * coe k›
    (-(1 * coe k)) ≃ _ := AA.scompatL
    (-1) * coe k   ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n > m → Positive (n——m)
Tactic:
case mpr =>
  intro (_ : m < n)
  show Positive (n——m)
  apply Generic.positive_iff_sign_pos1.mpr
  show NonzeroWithSign (n——m) 1
  have : Negative (m——n) := neg_diff_lt.mpr ‹m < n›
  have
    (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : m——n ≃ -1 * coe k))
      := Generic.negative_iff_sign_neg1.mp ‹Negative (m——n)›
  apply NonzeroWithSign.intro k ‹Positive k›
  show n——m ≃ 1 * coe k
  calc
    n——m              ≃ _ := Rel.symm neg_involutive
    (-(-(n——m)))      ≃ _ := Rel.refl
    (-(m——n))         ≃ _ := AA.subst₁ ‹m——n ≃ -1 * coe k›
    (-(-1 * coe k))   ≃ _ := AA.subst₁ (Rel.symm AA.scompatL)
    (-(-(1 * coe k))) ≃ _ := neg_involutive
    1 * coe k         ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
⊢ n > m
Tactic:
have
  (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : n——m ≃ 1 * coe k))
    := Generic.positive_iff_sign_pos1.mp ‹Positive (n——m)›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ n > m

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ n > m
Tactic:
show m < n
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ m < n

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ m < n
Tactic:
apply neg_diff_lt.mp
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ Negative (m——n)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ Negative (m——n)
Tactic:
apply Generic.negative_iff_sign_neg1.mpr
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ NonzeroWithSign (m——n) (-1)

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ NonzeroWithSign (m——n) (-1)
Tactic:
apply NonzeroWithSign.intro k ‹Positive k›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ m——n ≃ -1 * coe k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ m——n ≃ -1 * coe k
Tactic:
calc
  m——n           ≃ _ := Rel.symm neg_involutive
  (-(-(m——n)))   ≃ _ := Rel.refl
  (-(n——m))      ≃ _ := AA.subst₁ ‹n——m ≃ 1 * coe k›
  (-(1 * coe k)) ≃ _ := AA.scompatL
  (-1) * coe k   ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
⊢ Positive (n——m)
Tactic:
apply Generic.positive_iff_sign_pos1.mpr
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
⊢ NonzeroWithSign (n——m) 1

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
⊢ NonzeroWithSign (n——m) 1
Tactic:
have : Negative (m——n) := neg_diff_lt.mpr ‹m < n›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
⊢ NonzeroWithSign (n——m) 1

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
⊢ NonzeroWithSign (n——m) 1
Tactic:
have
  (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : m——n ≃ -1 * coe k))
    := Generic.negative_iff_sign_neg1.mp ‹Negative (m——n)›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
k : ℕ
pos✝ : Positive k
eqv✝ : m——n ≃ -1 * coe k
⊢ NonzeroWithSign (n——m) 1

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
k : ℕ
pos✝ : Positive k
eqv✝ : m——n ≃ -1 * coe k
⊢ NonzeroWithSign (n——m) 1
Tactic:
apply NonzeroWithSign.intro k ‹Positive k›
State after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
k : ℕ
pos✝ : Positive k
eqv✝ : m——n ≃ -1 * coe k
⊢ n——m ≃ 1 * coe k

State before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
k : ℕ
pos✝ : Positive k
eqv✝ : m——n ≃ -1 * coe k
⊢ n——m ≃ 1 * coe k
Tactic:
calc
  n——m              ≃ _ := Rel.symm neg_involutive
  (-(-(n——m)))      ≃ _ := Rel.refl
  (-(m——n))         ≃ _ := AA.subst₁ ‹m——n ≃ -1 * coe k›
  (-(-1 * coe k))   ≃ _ := AA.subst₁ (Rel.symm AA.scompatL)
  (-(-(1 * coe k))) ≃ _ := neg_involutive
  1 * coe k         ≃ _ := Rel.refl
State after:
no goals