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

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
⊢ False
Tactic:
have two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a) :=
  AA.TwoOfThree.twoAndThree ‹Positive a› ‹Negative a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ False

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ False
Tactic:
have not_two : ¬ AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a) :=
  (sign_trichotomy a).atMostOne
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
not_two : ¬AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ False

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
left✝ : Positive a
right✝ : Negative a
two : AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
not_two : ¬AA.TwoOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ False
Tactic:
exact absurd two not_two
State after:
no goals