internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
⊢ Positive a
Tactic:
have : NonzeroWithSign (-a) (-1) :=
  negative_iff_sign_neg1.mp ‹Negative (-a)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this : NonzeroWithSign (-a) (-1)
⊢ Positive a
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this : NonzeroWithSign (-a) (-1)
⊢ Positive a
Tactic:
have : NonzeroWithSign a (-(-1)) :=
  nonzeroWithSign_swap_neg.mp ‹NonzeroWithSign (-a) (-1)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝ : NonzeroWithSign (-a) (-1)
this : NonzeroWithSign a (- -1)
⊢ Positive a
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝ : NonzeroWithSign (-a) (-1)
this : NonzeroWithSign a (- -1)
⊢ Positive a
Tactic:
have : NonzeroWithSign a 1 :=
  NonzeroWithSign.subst_sign neg_involutive ‹NonzeroWithSign a (-(-1))›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝¹ : NonzeroWithSign (-a) (-1)
this✝ : NonzeroWithSign a (- -1)
this : NonzeroWithSign a 1
⊢ Positive a
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝¹ : NonzeroWithSign (-a) (-1)
this✝ : NonzeroWithSign a (- -1)
this : NonzeroWithSign a 1
⊢ Positive a
Tactic:
have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝² : NonzeroWithSign (-a) (-1)
this✝¹ : NonzeroWithSign a (- -1)
this✝ : NonzeroWithSign a 1
this : Positive a
⊢ Positive a
Theorem: Lean4Axiomatic.Integer.positive_iff_negated_negative
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝² : NonzeroWithSign (-a) (-1)
this✝¹ : NonzeroWithSign a (- -1)
this✝ : NonzeroWithSign a 1
this : Positive a
⊢ Positive a
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative a ↔ Positive (-a)
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative a → Positive (-a)

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive (-a) → Negative a
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative a → Positive (-a)
Tactic:
case mp =>
  intro (_ : Negative a)
  show Positive (-a)
  have : NonzeroWithSign a (-1) := negative_iff_sign_neg1.mp ‹Negative a›
  have : NonzeroWithSign (-a) 1 :=
    nonzeroWithSign_swap_neg.mpr ‹NonzeroWithSign a (-1)›
  have : Positive (-a) := positive_iff_sign_pos1.mpr ‹NonzeroWithSign (-a) 1›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive (-a) → Negative a
Tactic:
case mpr =>
  intro (_ : Positive (-a))
  show Negative a
  have : NonzeroWithSign (-a) 1 := positive_iff_sign_pos1.mp ‹Positive (-a)›
  have : NonzeroWithSign a (-1) :=
    nonzeroWithSign_swap_neg.mp ‹NonzeroWithSign (-a) 1›
  have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative a → Positive (-a)
Tactic:
intro (_ : Negative a)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative a
⊢ Positive (-a)
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative a
⊢ Positive (-a)
Tactic:
have : NonzeroWithSign a (-1) := negative_iff_sign_neg1.mp ‹Negative a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative a
this : NonzeroWithSign a (-1)
⊢ Positive (-a)
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative a
this : NonzeroWithSign a (-1)
⊢ Positive (-a)
Tactic:
have : NonzeroWithSign (-a) 1 :=
  nonzeroWithSign_swap_neg.mpr ‹NonzeroWithSign a (-1)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative a
this✝ : NonzeroWithSign a (-1)
this : NonzeroWithSign (-a) 1
⊢ Positive (-a)
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative a
this✝ : NonzeroWithSign a (-1)
this : NonzeroWithSign (-a) 1
⊢ Positive (-a)
Tactic:
have : Positive (-a) := positive_iff_sign_pos1.mpr ‹NonzeroWithSign (-a) 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative a
this✝¹ : NonzeroWithSign a (-1)
this✝ : NonzeroWithSign (-a) 1
this : Positive (-a)
⊢ Positive (-a)
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative a
this✝¹ : NonzeroWithSign a (-1)
this✝ : NonzeroWithSign (-a) 1
this : Positive (-a)
⊢ Positive (-a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive (-a) → Negative a
Tactic:
intro (_ : Positive (-a))
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive (-a)
⊢ Negative a
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive (-a)
⊢ Negative a
Tactic:
have : NonzeroWithSign (-a) 1 := positive_iff_sign_pos1.mp ‹Positive (-a)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive (-a)
this : NonzeroWithSign (-a) 1
⊢ Negative a
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive (-a)
this : NonzeroWithSign (-a) 1
⊢ Negative a
Tactic:
have : NonzeroWithSign a (-1) :=
  nonzeroWithSign_swap_neg.mp ‹NonzeroWithSign (-a) 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive (-a)
this✝ : NonzeroWithSign (-a) 1
this : NonzeroWithSign a (-1)
⊢ Negative a
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive (-a)
this✝ : NonzeroWithSign (-a) 1
this : NonzeroWithSign a (-1)
⊢ Negative a
Tactic:
have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive (-a)
this✝¹ : NonzeroWithSign (-a) 1
this✝ : NonzeroWithSign a (-1)
this : Negative a
⊢ Negative a
Theorem: Lean4Axiomatic.Integer.negative_iff_negated_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive (-a)
this✝¹ : NonzeroWithSign (-a) 1
this✝ : NonzeroWithSign a (-1)
this : Negative a
⊢ Negative a
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a ↔ Sqrt1 (sgn a)
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → Sqrt1 (sgn a)

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 (sgn a) → Nonzero a
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → Sqrt1 (sgn a)
Tactic:
case mp =>
  intro (_ : Nonzero a)
  show Sqrt1 (sgn a)
  have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
  match this with
  | Or.inl (_ : Positive a) =>
    have : 1 ≃ sgn a := Rel.symm (sgn_positive.mp ‹Positive a›)
    have : Sqrt1 (1:ℤ) := sqrt1_one
    have : Sqrt1 (sgn a) := sqrt1_subst ‹1 ≃ sgn a› ‹Sqrt1 (1:ℤ)›
    exact this
  | Or.inr (_ : Negative a) =>
    have : -1 ≃ sgn a := Rel.symm (sgn_negative.mp ‹Negative a›)
    have : Sqrt1 (-1:ℤ) := sqrt1_neg_one
    have : Sqrt1 (sgn a) := sqrt1_subst ‹-1 ≃ sgn a› ‹Sqrt1 (-1:ℤ)›
    exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 (sgn a) → Nonzero a
Tactic:
case mpr =>
  intro (_ : Sqrt1 (sgn a))
  show Nonzero a
  have : sgn a ≃ 1 ∨ sgn a ≃ -1 := sqrt1_cases.mp ‹Sqrt1 (sgn a)›
  have : Positive a ∨ Negative a := match this with
  | Or.inl (_ : sgn a ≃ 1) =>
    have : Positive a := sgn_positive.mpr ‹sgn a ≃ 1›
    Or.inl this
  | Or.inr (_ : sgn a ≃ -1) =>
    have : Negative a := sgn_negative.mpr ‹sgn a ≃ -1›
    Or.inr this
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr ‹Positive a ∨ Negative a›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → Sqrt1 (sgn a)
Tactic:
intro (_ : Nonzero a)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ Sqrt1 (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ Sqrt1 (sgn a)
Tactic:
have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ Sqrt1 (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ Sqrt1 (sgn a)
Tactic:
match this with
| Or.inl (_ : Positive a) =>
  have : 1 ≃ sgn a := Rel.symm (sgn_positive.mp ‹Positive a›)
  have : Sqrt1 (1:ℤ) := sqrt1_one
  have : Sqrt1 (sgn a) := sqrt1_subst ‹1 ≃ sgn a› ‹Sqrt1 (1:ℤ)›
  exact this
| Or.inr (_ : Negative a) =>
  have : -1 ≃ sgn a := Rel.symm (sgn_negative.mp ‹Negative a›)
  have : Sqrt1 (-1:ℤ) := sqrt1_neg_one
  have : Sqrt1 (sgn a) := sqrt1_subst ‹-1 ≃ sgn a› ‹Sqrt1 (-1:ℤ)›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Positive a ∨ Negative a
h✝ : Positive a
⊢ Sqrt1 (sgn a)
Tactic:
have : 1 ≃ sgn a := Rel.symm (sgn_positive.mp ‹Positive a›)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Positive a ∨ Negative a
h✝ : Positive a
this : 1 ≃ sgn a
⊢ Sqrt1 (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Positive a ∨ Negative a
h✝ : Positive a
this : 1 ≃ sgn a
⊢ Sqrt1 (sgn a)
Tactic:
have : Sqrt1 (1:ℤ) := sqrt1_one
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Positive a ∨ Negative a
h✝ : Positive a
this✝ : 1 ≃ sgn a
this : Sqrt1 1
⊢ Sqrt1 (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Positive a ∨ Negative a
h✝ : Positive a
this✝ : 1 ≃ sgn a
this : Sqrt1 1
⊢ Sqrt1 (sgn a)
Tactic:
have : Sqrt1 (sgn a) := sqrt1_subst ‹1 ≃ sgn a› ‹Sqrt1 (1:ℤ)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Positive a ∨ Negative a
h✝ : Positive a
this✝¹ : 1 ≃ sgn a
this✝ : Sqrt1 1
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Positive a ∨ Negative a
h✝ : Positive a
this✝¹ : 1 ≃ sgn a
this✝ : Sqrt1 1
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Positive a ∨ Negative a
h✝ : Negative a
⊢ Sqrt1 (sgn a)
Tactic:
have : -1 ≃ sgn a := Rel.symm (sgn_negative.mp ‹Negative a›)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Positive a ∨ Negative a
h✝ : Negative a
this : -1 ≃ sgn a
⊢ Sqrt1 (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Positive a ∨ Negative a
h✝ : Negative a
this : -1 ≃ sgn a
⊢ Sqrt1 (sgn a)
Tactic:
have : Sqrt1 (-1:ℤ) := sqrt1_neg_one
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Positive a ∨ Negative a
h✝ : Negative a
this✝ : -1 ≃ sgn a
this : Sqrt1 (-1)
⊢ Sqrt1 (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Positive a ∨ Negative a
h✝ : Negative a
this✝ : -1 ≃ sgn a
this : Sqrt1 (-1)
⊢ Sqrt1 (sgn a)
Tactic:
have : Sqrt1 (sgn a) := sqrt1_subst ‹-1 ≃ sgn a› ‹Sqrt1 (-1:ℤ)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Positive a ∨ Negative a
h✝ : Negative a
this✝¹ : -1 ≃ sgn a
this✝ : Sqrt1 (-1)
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn a)
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Positive a ∨ Negative a
h✝ : Negative a
this✝¹ : -1 ≃ sgn a
this✝ : Sqrt1 (-1)
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn a)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 (sgn a) → Nonzero a
Tactic:
intro (_ : Sqrt1 (sgn a))
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
⊢ Nonzero a
Tactic:
have : sgn a ≃ 1 ∨ sgn a ≃ -1 := sqrt1_cases.mp ‹Sqrt1 (sgn a)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this : sgn a ≃ 1 ∨ sgn a ≃ -1
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this : sgn a ≃ 1 ∨ sgn a ≃ -1
⊢ Nonzero a
Tactic:
have : Positive a ∨ Negative a := match this with
| Or.inl (_ : sgn a ≃ 1) =>
  have : Positive a := sgn_positive.mpr ‹sgn a ≃ 1›
  Or.inl this
| Or.inr (_ : sgn a ≃ -1) =>
  have : Negative a := sgn_negative.mpr ‹sgn a ≃ -1›
  Or.inr this
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this✝ : sgn a ≃ 1 ∨ sgn a ≃ -1
this : Positive a ∨ Negative a
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this✝ : sgn a ≃ 1 ∨ sgn a ≃ -1
this : Positive a ∨ Negative a
⊢ Nonzero a
Tactic:
have : Nonzero a := nonzero_iff_pos_or_neg.mpr ‹Positive a ∨ Negative a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this✝¹ : sgn a ≃ 1 ∨ sgn a ≃ -1
this✝ : Positive a ∨ Negative a
this : Nonzero a
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.sgn_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this✝¹ : sgn a ≃ 1 ∨ sgn a ≃ -1
this✝ : Positive a ∨ Negative a
this : Nonzero a
⊢ Nonzero 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)
⊢ NonzeroWithSign a (sgn a)
Tactic:
have : sgn a ≃ 1 ∨ sgn a ≃ -1 := sqrt1_cases.mp ‹Sqrt1 (sgn a)›
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
⊢ 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
⊢ NonzeroWithSign a (sgn a)
Tactic:
match this with
| Or.inl (_ : sgn a ≃ 1) =>
  have : Positive a := sgn_positive.mpr ‹sgn a ≃ 1›
  have : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp this
  have : NonzeroWithSign a (sgn a) :=
    NonzeroWithSign.subst_sign (Rel.symm ‹sgn a ≃ 1›) this
  exact this
| Or.inr (_ : sgn a ≃ -1) =>
  have : Negative a := sgn_negative.mpr ‹sgn a ≃ -1›
  have : NonzeroWithSign a (-1) := negative_iff_sign_neg1.mp this
  have : NonzeroWithSign a (sgn a) :=
    NonzeroWithSign.subst_sign (Rel.symm ‹sgn a ≃ -1›) this
  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 : Positive a := sgn_positive.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 : Positive 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
⊢ NonzeroWithSign a (sgn a)
Tactic:
have : NonzeroWithSign a 1 := positive_iff_sign_pos1.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✝ : Positive a
this : NonzeroWithSign a 1
⊢ NonzeroWithSign a (sgn a)