Theorem: Lean4Axiomatic.Integer.from_natural_preserves_nonzero (Lean4Axiomatic/Integer/Sign.lean)

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)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
n : ℕ
x✝ : n ≄ 0
⊢ Nonzero (coe n)

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›
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)

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
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)

State before:
ℕ : 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)
Tactic:
have : Nonzero (n : ℤ) := nonzero_from_positive this
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)
this : Nonzero (coe n)
⊢ Nonzero (coe n)

State before:
ℕ : 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)
this : Nonzero (coe n)
⊢ Nonzero (coe n)
Tactic:
exact this
State after:
no goals