Theorem: Lean4Axiomatic.Integer.zero? (Lean4Axiomatic/Integer/Sign.lean)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ AA.ExactlyOneOfTwo (a ≃ 0) (Nonzero a)
Tactic:
have tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a) :=
  Signed.trichotomy a
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ AA.ExactlyOneOfTwo (a ≃ 0) (Nonzero a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ AA.ExactlyOneOfTwo (a ≃ 0) (Nonzero a)
Tactic:
apply And.intro
State after:
case left
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ a ≃ 0 ∨ Nonzero a

case right
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ ¬(a ≃ 0 ∧ Nonzero a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
case left =>
  show a ≃ 0 ∨ Nonzero a
  match tri.atLeastOne with
  | AA.OneOfThree.first (_ : a ≃ 0) =>
    exact Or.inl ‹a ≃ 0›
  | AA.OneOfThree.second (_ : Positive a) =>
    have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inl ‹Positive a›)
    exact Or.inr ‹Nonzero a›
  | AA.OneOfThree.third (_ : Negative a) =>
    have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inr ‹Negative a›)
    exact Or.inr ‹Nonzero a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ ¬(a ≃ 0 ∧ Nonzero a)
Tactic:
case right =>
  intro (And.intro (_ : a ≃ 0) (_ : Nonzero a))
  show False
  apply tri.atMostOne
  show AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
  have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
  match ‹Positive a ∨ Negative a› with
  | Or.inl (_ : Positive a) =>
    exact AA.TwoOfThree.oneAndTwo ‹a ≃ 0› ‹Positive a›
  | Or.inr (_ : Negative a) =>
    exact AA.TwoOfThree.oneAndThree ‹a ≃ 0› ‹Negative a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
match tri.atLeastOne with
| AA.OneOfThree.first (_ : a ≃ 0) =>
  exact Or.inl ‹a ≃ 0›
| AA.OneOfThree.second (_ : Positive a) =>
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inl ‹Positive a›)
  exact Or.inr ‹Nonzero a›
| AA.OneOfThree.third (_ : Negative a) =>
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inr ‹Negative a›)
  exact Or.inr ‹Nonzero a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
a✝ : a ≃ 0
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
exact Or.inl ‹a ≃ 0›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inl ‹Positive a›)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
this : Nonzero a
⊢ a ≃ 0 ∨ Nonzero a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
this : Nonzero a
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
exact Or.inr ‹Nonzero a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
have : Nonzero a := nonzero_iff_pos_or_neg.mpr (Or.inr ‹Negative a›)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
this : Nonzero a
⊢ a ≃ 0 ∨ Nonzero a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
this : Nonzero a
⊢ a ≃ 0 ∨ Nonzero a
Tactic:
exact Or.inr ‹Nonzero a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ ¬(a ≃ 0 ∧ Nonzero a)
Tactic:
intro (And.intro (_ : a ≃ 0) (_ : Nonzero a))
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
⊢ False

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
⊢ False
Tactic:
apply tri.atMostOne
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
match ‹Positive a ∨ Negative a› with
| Or.inl (_ : Positive a) =>
  exact AA.TwoOfThree.oneAndTwo ‹a ≃ 0› ‹Positive a›
| Or.inr (_ : Negative a) =>
  exact AA.TwoOfThree.oneAndThree ‹a ≃ 0› ‹Negative a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
this : Positive a ∨ Negative a
h✝ : Positive a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
exact AA.TwoOfThree.oneAndTwo ‹a ≃ 0› ‹Positive a›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
tri : AA.ExactlyOneOfThree (a ≃ 0) (Positive a) (Negative a)
left✝ : a ≃ 0
right✝ : Nonzero a
this : Positive a ∨ Negative a
h✝ : Negative a
⊢ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
Tactic:
exact AA.TwoOfThree.oneAndThree ‹a ≃ 0› ‹Negative a›
State after:
no goals