Theorem: Lean4Axiomatic.Integer.positive_iff_negated_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:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a → Negative (-a)

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative (-a) → Positive a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive a → Negative (-a)
Tactic:
case mp =>
  intro (_ : Positive a)
  show Negative (-a)
  have nwsa : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp ‹Positive a›
  have : NonzeroWithSign a (-(-1)) :=
    NonzeroWithSign.subst_sign (Rel.symm neg_involutive) nwsa
  have : NonzeroWithSign (-a) (-1) :=
    nonzeroWithSign_swap_neg.mpr ‹NonzeroWithSign a (-(-1))›
  have : Negative (-a) :=
    negative_iff_sign_neg1.mpr ‹NonzeroWithSign (-a) (-1)›
  exact this
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative (-a) → Positive a
Tactic:
case mpr =>
  intro (_ : Negative (-a))
  show Positive a
  have : NonzeroWithSign (-a) (-1) :=
    negative_iff_sign_neg1.mp ‹Negative (-a)›
  have : NonzeroWithSign a (-(-1)) :=
    nonzeroWithSign_swap_neg.mp ‹NonzeroWithSign (-a) (-1)›
  have : NonzeroWithSign a 1 :=
    NonzeroWithSign.subst_sign neg_involutive ‹NonzeroWithSign a (-(-1))›
  have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
  exact this
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)
Tactic:
intro (_ : Positive a)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
⊢ Negative (-a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
⊢ Negative (-a)
Tactic:
have nwsa : 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
nwsa : NonzeroWithSign a 1
⊢ Negative (-a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
⊢ Negative (-a)
Tactic:
have : NonzeroWithSign a (-(-1)) :=
  NonzeroWithSign.subst_sign (Rel.symm neg_involutive) nwsa
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this : NonzeroWithSign a (- -1)
⊢ Negative (-a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this : NonzeroWithSign a (- -1)
⊢ Negative (-a)
Tactic:
have : NonzeroWithSign (-a) (-1) :=
  nonzeroWithSign_swap_neg.mpr ‹NonzeroWithSign a (-(-1))›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this✝ : NonzeroWithSign a (- -1)
this : NonzeroWithSign (-a) (-1)
⊢ Negative (-a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this✝ : NonzeroWithSign a (- -1)
this : NonzeroWithSign (-a) (-1)
⊢ 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✝ : Positive a
nwsa : NonzeroWithSign a 1
this✝¹ : NonzeroWithSign a (- -1)
this✝ : NonzeroWithSign (-a) (-1)
this : Negative (-a)
⊢ Negative (-a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a
nwsa : NonzeroWithSign a 1
this✝¹ : NonzeroWithSign a (- -1)
this✝ : NonzeroWithSign (-a) (-1)
this : Negative (-a)
⊢ Negative (-a)
Tactic:
exact this
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Negative (-a) → Positive a
Tactic:
intro (_ : Negative (-a))
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
⊢ Positive a

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this : NonzeroWithSign (-a) (-1)
⊢ Positive a
Tactic:
have : NonzeroWithSign a (-(-1)) :=
  nonzeroWithSign_swap_neg.mp ‹NonzeroWithSign (-a) (-1)›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝ : NonzeroWithSign (-a) (-1)
this : NonzeroWithSign a (- -1)
⊢ Positive a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝ : NonzeroWithSign (-a) (-1)
this : NonzeroWithSign a (- -1)
⊢ Positive a
Tactic:
have : NonzeroWithSign a 1 :=
  NonzeroWithSign.subst_sign neg_involutive ‹NonzeroWithSign a (-(-1))›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝¹ : NonzeroWithSign (-a) (-1)
this✝ : NonzeroWithSign a (- -1)
this : NonzeroWithSign a 1
⊢ Positive a

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Negative (-a)
this✝² : NonzeroWithSign (-a) (-1)
this✝¹ : NonzeroWithSign a (- -1)
this✝ : NonzeroWithSign a 1
this : Positive a
⊢ Positive a
Tactic:
exact this
State after:
no goals