internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝² : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝¹ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this : Positive a
⊢ s₁ ≃ s₂
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 s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝³ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝² : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝¹ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this✝ : Positive a
this : Negative a
⊢ s₁ ≃ s₂
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝³ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝² : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝¹ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this✝ : Positive a
this : Negative a
⊢ s₁ ≃ s₂
Tactic:
have : Positive a ∧ Negative a := And.intro ‹Positive a› ‹Negative a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝⁴ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝³ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝² : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this✝¹ : Positive a
this✝ : Negative a
this : Positive a ∧ Negative a
⊢ s₁ ≃ s₂
Theorem: Lean4Axiomatic.Integer.nonzeroWithSign_sign_inject
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝⁴ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝³ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝² : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this✝¹ : Positive a
this✝ : Negative a
this : Positive a ∧ Negative a
⊢ s₁ ≃ s₂
Tactic:
exact absurd ‹Positive a ∧ Negative a› not_positive_and_negative
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ SameSign a b → Positive a → Positive b
Tactic:
intro (SameSign.intro (s : ℤ) (_ : Sqrt1 s) nwsa nwsb)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
⊢ Positive a → Positive b
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
⊢ Positive a → Positive b
Tactic:
have : NonzeroWithSign a s := nwsa
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this : NonzeroWithSign a s
⊢ Positive a → Positive b
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this : NonzeroWithSign a s
⊢ Positive a → Positive b
Tactic:
have : NonzeroWithSign b s := nwsb
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
⊢ Positive a → Positive b
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
⊢ Positive a → Positive b
Tactic:
intro (_ : Positive a)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
x✝ : Positive a
⊢ Positive b
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝ : NonzeroWithSign a s
this : NonzeroWithSign b s
x✝ : Positive a
⊢ Positive b
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 b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign b s
x✝ : Positive a
this : NonzeroWithSign a 1
⊢ Positive b
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign b s
x✝ : Positive a
this : NonzeroWithSign a 1
⊢ Positive b
Tactic:
have : s ≃ 1 :=
  nonzeroWithSign_sign_inject ‹NonzeroWithSign a s› ‹NonzeroWithSign a 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝² : NonzeroWithSign a s
this✝¹ : NonzeroWithSign b s
x✝ : Positive a
this✝ : NonzeroWithSign a 1
this : s ≃ 1
⊢ Positive b
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝² : NonzeroWithSign a s
this✝¹ : NonzeroWithSign b s
x✝ : Positive a
this✝ : NonzeroWithSign a 1
this : s ≃ 1
⊢ Positive b
Tactic:
have : NonzeroWithSign b 1 :=
  NonzeroWithSign.subst_sign ‹s ≃ 1› ‹NonzeroWithSign b s›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝³ : NonzeroWithSign a s
this✝² : NonzeroWithSign b s
x✝ : Positive a
this✝¹ : NonzeroWithSign a 1
this✝ : s ≃ 1
this : NonzeroWithSign b 1
⊢ Positive b
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝³ : NonzeroWithSign a s
this✝² : NonzeroWithSign b s
x✝ : Positive a
this✝¹ : NonzeroWithSign a 1
this✝ : s ≃ 1
this : NonzeroWithSign b 1
⊢ Positive b
Tactic:
have : Positive b := positive_iff_sign_pos1.mpr ‹NonzeroWithSign b 1›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝⁴ : NonzeroWithSign a s
this✝³ : NonzeroWithSign b s
x✝ : Positive a
this✝² : NonzeroWithSign a 1
this✝¹ : s ≃ 1
this✝ : NonzeroWithSign b 1
this : Positive b
⊢ Positive b
Theorem: Lean4Axiomatic.Integer.same_sign_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝⁴ : NonzeroWithSign a s
this✝³ : NonzeroWithSign b s
x✝ : Positive a
this✝² : NonzeroWithSign a 1
this✝¹ : s ≃ 1
this✝ : NonzeroWithSign b 1
this : Positive b
⊢ Positive b
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a ↔ Positive a ∨ Negative 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 → Positive a ∨ Negative a

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a ∨ Negative a → Nonzero a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → Positive a ∨ Negative a
Tactic:
case mp =>
  intro (_ : Nonzero a)
  show Positive a ∨ Negative a
  have (Nonzero.intro (s : ℤ) (_ : Sqrt1 s) nwsa) := ‹Nonzero a›
  have : NonzeroWithSign a s := nwsa
  have : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1) :=
    nonzeroWithSign_cases ‹NonzeroWithSign a s›
  match ‹NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)› with
  | Or.inl (_ : NonzeroWithSign a 1) =>
    have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
    exact Or.inl ‹Positive a›
  | Or.inr (_ : NonzeroWithSign a (-1)) =>
    have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
    exact Or.inr ‹Negative a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a ∨ Negative a → Nonzero a
Tactic:
case mpr =>
  intro (_ : Positive a ∨ Negative a)
  show Nonzero a
  match ‹Positive a ∨ Negative a› with
  | Or.inl (_ : Positive a) =>
    have : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp ‹Positive a›
    exact Nonzero.mk ‹NonzeroWithSign a 1›
  | Or.inr (_ : Negative a) =>
    have : NonzeroWithSign a (-1) := negative_iff_sign_neg1.mp ‹Negative a›
    exact Nonzero.mk ‹NonzeroWithSign a (-1)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → Positive a ∨ Negative 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
⊢ Positive a ∨ Negative a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ Positive a ∨ Negative a
Tactic:
have (Nonzero.intro (s : ℤ) (_ : Sqrt1 s) nwsa) := ‹Nonzero a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
⊢ Positive a ∨ Negative a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
⊢ Positive a ∨ Negative a
Tactic:
have : NonzeroWithSign a s := nwsa
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this : NonzeroWithSign a s
⊢ Positive a ∨ Negative a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this : NonzeroWithSign a s
⊢ Positive a ∨ Negative a
Tactic:
have : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1) :=
  nonzeroWithSign_cases ‹NonzeroWithSign a s›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝ : NonzeroWithSign a s
this : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
⊢ Positive a ∨ Negative a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝ : NonzeroWithSign a s
this : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
⊢ Positive a ∨ Negative a
Tactic:
match ‹NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)› with
| Or.inl (_ : NonzeroWithSign a 1) =>
  have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
  exact Or.inl ‹Positive a›
| Or.inr (_ : NonzeroWithSign a (-1)) =>
  have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
  exact Or.inr ‹Negative a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝ : NonzeroWithSign a s
this : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
h✝ : NonzeroWithSign a 1
⊢ Positive a ∨ Negative 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✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
h✝ : NonzeroWithSign a 1
this : Positive a
⊢ Positive a ∨ Negative a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
h✝ : NonzeroWithSign a 1
this : Positive a
⊢ Positive a ∨ Negative a
Tactic:
exact Or.inl ‹Positive a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝ : NonzeroWithSign a s
this : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
h✝ : NonzeroWithSign a (-1)
⊢ Positive a ∨ 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✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
h✝ : NonzeroWithSign a (-1)
this : Negative a
⊢ Positive a ∨ Negative a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
h✝ : NonzeroWithSign a (-1)
this : Negative a
⊢ Positive a ∨ Negative a
Tactic:
exact Or.inr ‹Negative a›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a ∨ Negative a → Nonzero a
Tactic:
intro (_ : Positive a ∨ Negative a)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a ∨ Negative a
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a ∨ Negative a
⊢ Nonzero a
Tactic:
match ‹Positive a ∨ Negative a› with
| Or.inl (_ : Positive a) =>
  have : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp ‹Positive a›
  exact Nonzero.mk ‹NonzeroWithSign a 1›
| Or.inr (_ : Negative a) =>
  have : NonzeroWithSign a (-1) := negative_iff_sign_neg1.mp ‹Negative a›
  exact Nonzero.mk ‹NonzeroWithSign a (-1)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a ∨ Negative a
h✝ : Positive a
⊢ Nonzero 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 ∨ Negative a
h✝ : Positive a
this : NonzeroWithSign a 1
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a ∨ Negative a
h✝ : Positive a
this : NonzeroWithSign a 1
⊢ Nonzero a
Tactic:
exact Nonzero.mk ‹NonzeroWithSign a 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a ∨ Negative a
h✝ : Negative a
⊢ Nonzero 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✝ : Positive a ∨ Negative a
h✝ : Negative a
this : NonzeroWithSign a (-1)
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.nonzero_iff_pos_or_neg
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a ∨ Negative a
h✝ : Negative a
this : NonzeroWithSign a (-1)
⊢ Nonzero a
Tactic:
exact Nonzero.mk ‹NonzeroWithSign a (-1)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_from_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a → Nonzero 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
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.nonzero_from_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
⊢ Nonzero a
Tactic:
have : Positive a ∨ Negative a := Or.inl ‹Positive a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
this : Positive a ∨ Negative a
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.nonzero_from_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
this : Positive a ∨ Negative a
⊢ Nonzero a
Tactic:
have : Nonzero a := nonzero_iff_pos_or_neg.mpr this
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
this✝ : Positive a ∨ Negative a
this : Nonzero a
⊢ Nonzero a
Theorem: Lean4Axiomatic.Integer.nonzero_from_positive
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
this✝ : Positive a ∨ Negative a
this : Nonzero a
⊢ Nonzero a
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.from_natural_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
⊢ n ≄ 0 → Nonzero (coe n)
Tactic:
intro (_ : n ≄ 0)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
⊢ Nonzero (coe n)
Theorem: Lean4Axiomatic.Integer.from_natural_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
⊢ Nonzero (coe n)
Tactic:
have : Positive n := Signed.positive_defn.mpr ‹n ≄ 0›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
this : Positive n
⊢ Nonzero (coe n)
Theorem: Lean4Axiomatic.Integer.from_natural_preserves_nonzero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
this : Positive n
⊢ Nonzero (coe n)
Tactic:
have : Positive (n : ℤ) := positive_intro_nat this Rel.refl
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
this✝ : Positive n
this : Positive (coe n)
⊢ Nonzero (coe n)