internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.add_cancelR
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
⊢ a₁ ≃ a₂
Tactic:
have : b + a₁ ≃ b + a₂ := calc
  _ = b + a₁ := rfl
  _ ≃ a₁ + b := AA.comm
  _ ≃ a₂ + b := ‹a₁ + b ≃ a₂ + b›
  _ ≃ b + a₂ := AA.comm
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
this : b + a₁ ≃ b + a₂
⊢ a₁ ≃ a₂
Theorem: Lean4Axiomatic.Integer.add_cancelR
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
this : b + a₁ ≃ b + a₂
⊢ a₁ ≃ a₂
Tactic:
have : a₁ ≃ a₂ := add_cancelL ‹b + a₁ ≃ b + a₂›
Proof state after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
this✝ : b + a₁ ≃ b + a₂
this : a₁ ≃ a₂
⊢ a₁ ≃ a₂
Theorem: Lean4Axiomatic.Integer.add_cancelR
Proof state before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ b : ℤ
x✝ : a₁ + b ≃ a₂ + b
this✝ : b + a₁ ≃ b + a₂
this : a₁ ≃ a₂
⊢ a₁ ≃ a₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 ↔ n ≃ m
Tactic:
apply Iff.intro
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n——m ≃ 0 → n ≃ m
Tactic:
intro (_ : n——m ≃ 0)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
⊢ n ≃ m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
⊢ n ≃ m
Tactic:
have : n——m ≃ 0——0 := ‹n——m ≃ 0›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this : n——m ≃ 0——0
⊢ n ≃ m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof 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›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n——m ≃ 0
this✝ : n——m ≃ 0——0
this : n + 0 ≃ 0 + m
⊢ n ≃ m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n ≃ m → n——m ≃ 0
Tactic:
intro (_ : n ≃ m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n——m ≃ 0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n——m ≃ 0
Tactic:
show n——m ≃ 0——0
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n——m ≃ 0——0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n——m ≃ 0——0
Tactic:
show n + 0 ≃ 0 + m
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n + 0 ≃ 0 + m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.zero_diff_eqv
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n + 0 ≃ 0 + m
Tactic:
exact Natural.add_swapped_zeros_eqv.mpr ‹n ≃ m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Negative (n——m) ↔ n < m
Tactic:
have neg_diff {k : ℕ} : 0——k ≃ -1 * coe k := by
  apply Rel.symm
  calc
    (-1) * coe k ≃ _ := Rel.refl
    (-1) * k——0  ≃ _ := mul_neg_one
    (-(k——0))    ≃ _ := Rel.refl
    0——k         ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) ↔ n < m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) ↔ n < m
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) → n < m

case mpr
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ n < m → Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) → n < m
Tactic:
case mp =>
  intro (_ : Negative (n——m))
  show n < m
  apply Natural.lt_defn_add.mpr
  show ∃ (k : ℕ), Positive k ∧ m ≃ n + k
  have
    (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : n——m ≃ -1 * coe k))
      := Generic.negative_iff_sign_neg1.mp ‹Negative (n——m)›
  have : n——m ≃ 0——k := Rel.trans ‹n——m ≃ -1 * coe k› (Rel.symm neg_diff)
  have : n + k ≃ 0 + m := ‹n——m ≃ 0——k›
  have : m ≃ n + k := calc
    m     ≃ _ := Rel.symm AA.identL
    0 + m ≃ _ := Rel.symm ‹n + k ≃ 0 + m›
    n + k ≃ _ := Rel.refl
  exact Exists.intro k (And.intro ‹Positive k› ‹m ≃ n + k›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m k : ℕ
⊢ 0——k ≃ -1 * coe k
Tactic:
apply Rel.symm
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m k : ℕ
⊢ -1 * coe k ≃ 0——k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
n m k : ℕ
⊢ -1 * coe k ≃ 0——k
Tactic:
calc
  (-1) * coe k ≃ _ := Rel.refl
  (-1) * k——0  ≃ _ := mul_neg_one
  (-(k——0))    ≃ _ := Rel.refl
  0——k         ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ Negative (n——m) → n < m
Tactic:
intro (_ : Negative (n——m))
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ n < m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ n < m
Tactic:
apply Natural.lt_defn_add.mpr
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ ∃ k, Positive k ∧ m ≃ n + k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have
  (NonzeroWithSign.intro (k : ℕ) (_ : Positive k) (_ : n——m ≃ -1 * coe k))
    := Generic.negative_iff_sign_neg1.mp ‹Negative (n——m)›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have : n——m ≃ 0——k := Rel.trans ‹n——m ≃ -1 * coe k› (Rel.symm neg_diff)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this : n——m ≃ 0——k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this : n——m ≃ 0——k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have : n + k ≃ 0 + m := ‹n——m ≃ 0——k›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this✝ : n——m ≃ 0——k
this : n + k ≃ 0 + m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this✝ : n——m ≃ 0——k
this : n + k ≃ 0 + m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have : m ≃ n + k := calc
  m     ≃ _ := Rel.symm AA.identL
  0 + m ≃ _ := Rel.symm ‹n + k ≃ 0 + m›
  n + k ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this✝¹ : n——m ≃ 0——k
this✝ : n + k ≃ 0 + m
this : m ≃ n + k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : Negative (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ -1 * coe k
this✝¹ : n——m ≃ 0——k
this✝ : n + k ≃ 0 + m
this : m ≃ n + k
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
exact Exists.intro k (And.intro ‹Positive k› ‹m ≃ n + k›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
⊢ n < m → Negative (n——m)
Tactic:
intro (_ : n < m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ Negative (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ Negative (n——m)
Tactic:
apply Generic.negative_iff_sign_neg1.mpr
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ NonzeroWithSign (n——m) (-1)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
⊢ NonzeroWithSign (n——m) (-1)
Tactic:
have (Exists.intro k (And.intro (_ : Positive k) (_ : m ≃ n + k))) :=
  Natural.lt_defn_add.mp ‹n < m›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ NonzeroWithSign (n——m) (-1)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ NonzeroWithSign (n——m) (-1)
Tactic:
apply NonzeroWithSign.intro k ‹Positive k›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ n——m ≃ -1 * coe k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ n——m ≃ -1 * coe k
Tactic:
have : 0——k ≃ -1 * coe k := neg_diff
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
this : 0——k ≃ -1 * coe k
⊢ n——m ≃ -1 * coe k
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
this : 0——k ≃ -1 * coe k
⊢ n——m ≃ 0——k
Tactic:
show n + k ≃ 0 + m
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
this : 0——k ≃ -1 * coe k
⊢ n + k ≃ 0 + m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.neg_diff_lt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
neg_diff : ∀ {k : ℕ}, 0——k ≃ -1 * coe k
x✝ : n < m
k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
this : 0——k ≃ -1 * coe k
⊢ n + k ≃ 0 + m
Tactic:
calc
  n + k ≃ _ := Rel.symm ‹m ≃ n + k›
  m     ≃ _ := Rel.symm AA.identL
  0 + m ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) ↔ n > m
Tactic:
apply Iff.intro
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ Positive (n——m) → n > m
Tactic:
intro (_ : Positive (n——m))
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
⊢ n > m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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)›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ n > m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ m < n
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : Positive (n——m)
k : ℕ
pos✝ : Positive k
eqv✝ : n——m ≃ 1 * coe k
⊢ Negative (m——n)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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
Proof 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)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ n > m → Positive (n——m)
Tactic:
intro (_ : m < n)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
⊢ Positive (n——m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
⊢ Positive (n——m)
Tactic:
apply Generic.positive_iff_sign_pos1.mpr
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
⊢ NonzeroWithSign (n——m) 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
x✝ : m < n
this : Negative (m——n)
⊢ NonzeroWithSign (n——m) 1
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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)›
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Integer.Impl.Difference.pos_diff_gt
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a : Difference ℕ
⊢ AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
revert a
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ (a : Difference ℕ), AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
⊢ ∀ (a : Difference ℕ), AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
intro (n——m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ AA.ExactlyOneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ AA.ExactlyOneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
have natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m) :=
  Natural.trichotomy n m
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.ExactlyOneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.ExactlyOneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
apply AA.ExactlyOneOfThree.mk
Proof state after:
case atLeastOne
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))

case atMostOne
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ ¬AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
case atLeastOne =>
  show AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
  match natOrderTri.atLeastOne with
  | AA.OneOfThree.first (_ : n < m) =>
    have : Negative (n——m) := neg_diff_lt.mpr ‹n < m›
    exact AA.OneOfThree.third ‹Negative (n——m)›
  | AA.OneOfThree.second (_ : n ≃ m) =>
    have : n——m ≃ 0 := zero_diff_eqv.mpr ‹n ≃ m›
    exact AA.OneOfThree.first ‹n——m ≃ 0›
  | AA.OneOfThree.third (_ : n > m) =>
    have : Positive (n——m) := pos_diff_gt.mpr ‹n > m›
    exact AA.OneOfThree.second ‹Positive (n——m)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.sign_trichotomy
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ ¬AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
Tactic:
case atMostOne =>
  intro (h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m)))
  have twoOfThree : AA.TwoOfThree (n < m) (n ≃ m) (n > m) := match h with
  | AA.TwoOfThree.oneAndTwo (_ : n——m ≃ 0) (_ : Positive (n——m)) =>
    have : n ≃ m := zero_diff_eqv.mp ‹n——m ≃ 0›
    have : n > m := pos_diff_gt.mp ‹Positive (n——m)›
    AA.TwoOfThree.twoAndThree ‹n ≃ m› ‹n > m›
  | AA.TwoOfThree.oneAndThree (_ : n——m ≃ 0) (_ : Negative (n——m)) =>
    have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
    have : n ≃ m := zero_diff_eqv.mp ‹n——m ≃ 0›
    AA.TwoOfThree.oneAndTwo ‹n < m› ‹n ≃ m›
  | AA.TwoOfThree.twoAndThree (_ : Positive (n——m)) (_ : Negative (n——m)) =>
    have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
    have : n > m := pos_diff_gt.mp ‹Positive (n——m)›
    AA.TwoOfThree.oneAndThree ‹n < m› ‹n > m›
  show False
  have notTwoOfThree : ¬ AA.TwoOfThree (n < m) (n ≃ m) (n > m) :=
    natOrderTri.atMostOne
  exact absurd twoOfThree notTwoOfThree
Proof state after:
no goals