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

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

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›
State after:
no goals

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)›
State after:
no goals

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)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ Positive a ∨ Negative a

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

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

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

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›
State after:
no goals

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

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›
State after:
no goals

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

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›
State after:
no goals

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)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a ∨ Negative a
⊢ Nonzero a

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)›
State after:
no goals

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

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›
State after:
no goals

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

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)›
State after:
no goals