internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.sgn_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝¹ : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ 1
this✝ : Positive a
this : NonzeroWithSign a 1
⊢ NonzeroWithSign a (sgn a)
Tactic:
have : NonzeroWithSign a (sgn a) :=
  NonzeroWithSign.subst_sign (Rel.symm ‹sgn a ≃ 1›) this
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝² : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ 1
this✝¹ : Positive a
this✝ : NonzeroWithSign a 1
this : NonzeroWithSign a (sgn a)
⊢ NonzeroWithSign a (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝² : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ 1
this✝¹ : Positive a
this✝ : NonzeroWithSign a 1
this : NonzeroWithSign a (sgn a)
⊢ NonzeroWithSign a (sgn a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ -1
⊢ NonzeroWithSign a (sgn a)
Tactic:
have : Negative a := sgn_negative.mpr ‹sgn a ≃ -1›
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝ : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ -1
this : Negative a
⊢ NonzeroWithSign a (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝ : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ -1
this : Negative a
⊢ NonzeroWithSign a (sgn a)
Tactic:
have : NonzeroWithSign a (-1) := negative_iff_sign_neg1.mp this
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝¹ : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ -1
this✝ : Negative a
this : NonzeroWithSign a (-1)
⊢ NonzeroWithSign a (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝¹ : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ -1
this✝ : Negative a
this : NonzeroWithSign a (-1)
⊢ NonzeroWithSign a (sgn a)
Tactic:
have : NonzeroWithSign a (sgn a) :=
  NonzeroWithSign.subst_sign (Rel.symm ‹sgn a ≃ -1›) this
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝² : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ -1
this✝¹ : Negative a
this✝ : NonzeroWithSign a (-1)
this : NonzeroWithSign a (sgn a)
⊢ NonzeroWithSign a (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzeroWithSign
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a : ℤ
inst✝ : Sqrt1 (sgn a)
this✝² : sgn a ≃ 1 ∨ sgn a ≃ -1
h✝ : sgn a ≃ -1
this✝¹ : Negative a
this✝ : NonzeroWithSign a (-1)
this : NonzeroWithSign a (sgn a)
⊢ NonzeroWithSign a (sgn a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → sgn a₁ ≃ sgn a₂
Tactic:
intro (_ : a₁ ≃ a₂)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ sgn a₁ ≃ sgn a₂
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ sgn a₁ ≃ sgn a₂
Tactic:
have : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁) :=
  (sign_trichotomy a₁).atLeastOne
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
⊢ sgn a₁ ≃ sgn a₂
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
⊢ sgn a₁ ≃ sgn a₂
Tactic:
match this with
| AA.OneOfThree.first (_ : a₁ ≃ 0) =>
  have : a₂ ≃ 0 := AA.substLFn ‹a₁ ≃ a₂› ‹a₁ ≃ 0›
  calc
    sgn a₁ ≃ _ := sgn_zero.mp ‹a₁ ≃ 0›
    0      ≃ _ := Rel.symm (sgn_zero.mp ‹a₂ ≃ 0›)
    sgn a₂ ≃ _ := Rel.refl
| AA.OneOfThree.second (_ : Positive a₁) =>
  have : Positive a₂ := positive_subst ‹a₁ ≃ a₂› ‹Positive a₁›
  calc
    sgn a₁ ≃ _ := sgn_positive.mp ‹Positive a₁›
    1      ≃ _ := Rel.symm (sgn_positive.mp ‹Positive a₂›)
    sgn a₂ ≃ _ := Rel.refl
| AA.OneOfThree.third (_ : Negative a₁) =>
  have : Negative a₂ := negative_subst ‹a₁ ≃ a₂› ‹Negative a₁›
  calc
    sgn a₁ ≃ _ := sgn_negative.mp ‹Negative a₁›
    (-1)   ≃ _ := Rel.symm (sgn_negative.mp ‹Negative a₂›)
    sgn a₂ ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
a✝ : a₁ ≃ 0
⊢ sgn a₁ ≃ sgn a₂
Tactic:
have : a₂ ≃ 0 := AA.substLFn ‹a₁ ≃ a₂› ‹a₁ ≃ 0›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
a✝ : a₁ ≃ 0
this : a₂ ≃ 0
⊢ sgn a₁ ≃ sgn a₂
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
a✝ : a₁ ≃ 0
this : a₂ ≃ 0
⊢ sgn a₁ ≃ sgn a₂
Tactic:
calc
  sgn a₁ ≃ _ := sgn_zero.mp ‹a₁ ≃ 0›
  0      ≃ _ := Rel.symm (sgn_zero.mp ‹a₂ ≃ 0›)
  sgn a₂ ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
b✝ : Positive a₁
⊢ sgn a₁ ≃ sgn a₂
Tactic:
have : Positive a₂ := positive_subst ‹a₁ ≃ a₂› ‹Positive a₁›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
b✝ : Positive a₁
this : Positive a₂
⊢ sgn a₁ ≃ sgn a₂
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
b✝ : Positive a₁
this : Positive a₂
⊢ sgn a₁ ≃ sgn a₂
Tactic:
calc
  sgn a₁ ≃ _ := sgn_positive.mp ‹Positive a₁›
  1      ≃ _ := Rel.symm (sgn_positive.mp ‹Positive a₂›)
  sgn a₂ ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
c✝ : Negative a₁
⊢ sgn a₁ ≃ sgn a₂
Tactic:
have : Negative a₂ := negative_subst ‹a₁ ≃ a₂› ‹Negative a₁›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
c✝ : Negative a₁
this : Negative a₂
⊢ sgn a₁ ≃ sgn a₂
Theorem: Lean4Axiomatic.Integer.sgn_subst
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
c✝ : Negative a₁
this : Negative a₂
⊢ sgn a₁ ≃ sgn a₂
Tactic:
calc
  sgn a₁ ≃ _ := sgn_negative.mp ‹Negative a₁›
  (-1)   ≃ _ := Rel.symm (sgn_negative.mp ‹Negative a₂›)
  sgn a₂ ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_idemp
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ sgn (sgn a) ≃ sgn a
Tactic:
have : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a) :=
  (sign_trichotomy a).atLeastOne
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ sgn (sgn a) ≃ sgn a
Theorem: Lean4Axiomatic.Integer.sgn_idemp
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ sgn (sgn a) ≃ sgn a
Tactic:
match this with
| AA.OneOfThree.first (_ : a ≃ 0) =>
  have : sgn a ≃ 0 := sgn_zero.mp ‹a ≃ 0›
  calc
    sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 0›
    sgn (0 : ℤ) ≃ _ := sgn_subst (Rel.symm ‹a ≃ 0›)
    sgn a       ≃ _ := Rel.refl
| AA.OneOfThree.second (_ : Positive a) =>
  have : sgn a ≃ 1 := sgn_positive.mp ‹Positive a›
  calc
    sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 1›
    sgn (1 : ℤ) ≃ _ := sgn_positive.mp one_positive
    1           ≃ _ := Rel.symm ‹sgn a ≃ 1›
    sgn a       ≃ _ := Rel.refl
| AA.OneOfThree.third (_ : Negative a) =>
  have : sgn a ≃ -1 := sgn_negative.mp ‹Negative a›
  calc
    sgn (sgn a)  ≃ _ := sgn_subst ‹sgn a ≃ -1›
    sgn (-1 : ℤ) ≃ _ := sgn_negative.mp neg_one_negative
    (-1)         ≃ _ := Rel.symm ‹sgn a ≃ -1›
    sgn a        ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_idemp
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
a✝ : a ≃ 0
⊢ sgn (sgn a) ≃ sgn a
Tactic:
have : sgn a ≃ 0 := sgn_zero.mp ‹a ≃ 0›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
a✝ : a ≃ 0
this : sgn a ≃ 0
⊢ sgn (sgn a) ≃ sgn a
Theorem: Lean4Axiomatic.Integer.sgn_idemp
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
a✝ : a ≃ 0
this : sgn a ≃ 0
⊢ sgn (sgn a) ≃ sgn a
Tactic:
calc
  sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 0›
  sgn (0 : ℤ) ≃ _ := sgn_subst (Rel.symm ‹a ≃ 0›)
  sgn a       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_idemp
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
⊢ sgn (sgn a) ≃ sgn a
Tactic:
have : sgn a ≃ 1 := sgn_positive.mp ‹Positive a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
this : sgn a ≃ 1
⊢ sgn (sgn a) ≃ sgn a
Theorem: Lean4Axiomatic.Integer.sgn_idemp
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
this : sgn a ≃ 1
⊢ sgn (sgn a) ≃ sgn a
Tactic:
calc
  sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 1›
  sgn (1 : ℤ) ≃ _ := sgn_positive.mp one_positive
  1           ≃ _ := Rel.symm ‹sgn a ≃ 1›
  sgn a       ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_idemp
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
⊢ sgn (sgn a) ≃ sgn a
Tactic:
have : sgn a ≃ -1 := sgn_negative.mp ‹Negative a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
this : sgn a ≃ -1
⊢ sgn (sgn a) ≃ sgn a
Theorem: Lean4Axiomatic.Integer.sgn_idemp
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
this : sgn a ≃ -1
⊢ sgn (sgn a) ≃ sgn a
Tactic:
calc
  sgn (sgn a)  ≃ _ := sgn_subst ‹sgn a ≃ -1›
  sgn (-1 : ℤ) ≃ _ := sgn_negative.mp neg_one_negative
  (-1)         ≃ _ := Rel.symm ‹sgn a ≃ -1›
  sgn a        ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_sgn_split_nonzero_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ Nonzero (a * b) → Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Tactic:
intro (_ : Nonzero (a * b))
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
⊢ Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Theorem: Lean4Axiomatic.Integer.sqrt1_sgn_split_nonzero_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
⊢ Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Tactic:
have (And.intro (_ : Nonzero a) (_ : Nonzero b)) :=
  nonzero_factors_if_nonzero_product ‹Nonzero (a * b)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
⊢ Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Theorem: Lean4Axiomatic.Integer.sqrt1_sgn_split_nonzero_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
⊢ Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Tactic:
have : Sqrt1 (sgn a) := sgn_nonzero.mp ‹Nonzero a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Theorem: Lean4Axiomatic.Integer.sqrt1_sgn_split_nonzero_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Tactic:
have : Sqrt1 (sgn b) := sgn_nonzero.mp ‹Nonzero b›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
this✝ : Sqrt1 (sgn a)
this : Sqrt1 (sgn b)
⊢ Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Theorem: Lean4Axiomatic.Integer.sqrt1_sgn_split_nonzero_mul
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
this✝ : Sqrt1 (sgn a)
this : Sqrt1 (sgn b)
⊢ Sqrt1 (sgn a) ∧ Sqrt1 (sgn b)
Tactic:
exact And.intro ‹Sqrt1 (sgn a)› ‹Sqrt1 (sgn b)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_mul_from_sqrt1_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Tactic:
have nws_a : NonzeroWithSign a (sgn a) := sgn_nonzeroWithSign
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_mul_from_sqrt1_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Tactic:
have nws_b : NonzeroWithSign b (sgn b) := sgn_nonzeroWithSign
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
nws_b : NonzeroWithSign b (sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_mul_from_sqrt1_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
nws_b : NonzeroWithSign b (sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Tactic:
have : NonzeroWithSign (a * b) (sgn a * sgn b) :=
  mul_preserves_nonzeroWithSign nws_a nws_b
Proof state after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
nws_b : NonzeroWithSign b (sgn b)
this : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_mul_from_sqrt1_sgn
Proof state before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
nws_b : NonzeroWithSign b (sgn b)
this : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_sgn_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
⊢ Positive (a * b) ↔ sgn a ≃ sgn b
Tactic:
have (And.intro (_ : Sqrt1 (sgn a)) (_ : Sqrt1 (sgn b))) :=
  sqrt1_sgn_split_nonzero_mul ‹Nonzero (a * b)›
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
⊢ Positive (a * b) ↔ sgn a ≃ sgn b
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_sgn_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
⊢ Positive (a * b) ↔ sgn a ≃ sgn b
Tactic:
have nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b) :=
  nonzeroWithSign_mul_from_sqrt1_sgn
Proof state after:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ Positive (a * b) ↔ sgn a ≃ sgn b
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_sgn_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ Positive (a * b) ↔ sgn a ≃ sgn b
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ Positive (a * b) → sgn a ≃ sgn b

case mpr
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ sgn a ≃ sgn b → Positive (a * b)
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_sgn_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ Positive (a * b) → sgn a ≃ sgn b
Tactic:
case mp =>
  intro (_ : Positive (a * b))
  show sgn a ≃ sgn b
  have nws_ab_one : NonzeroWithSign (a * b) 1 :=
    positive_iff_sign_pos1.mp ‹Positive (a * b)›
  have : sgn a * sgn b ≃ 1 :=
    nonzeroWithSign_sign_inject nws_ab_sgn nws_ab_one
  have (And.intro _ (_ : sgn a ≃ sgn b)) := mul_sqrt1_eqv.mp this
  exact ‹sgn a ≃ sgn b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.positive_mul_iff_sgn_eqv
Proof state before:
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab_sgn : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ sgn a ≃ sgn b → Positive (a * b)
Tactic:
case mpr =>
  intro (_ : sgn a ≃ sgn b)
  show Positive (a * b)
  have : Sqrt1 (sgn b) ∧ sgn a ≃ sgn b :=
    And.intro ‹Sqrt1 (sgn b)› ‹sgn a ≃ sgn b›
  have : sgn a * sgn b ≃ 1 := mul_sqrt1_eqv.mpr this
  have : NonzeroWithSign (a * b) 1 :=
    NonzeroWithSign.subst_sign ‹sgn a * sgn b ≃ 1› nws_ab_sgn
  have : Positive (a * b) := positive_iff_sign_pos1.mpr this
  exact this
Proof state after:
no goals