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

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s ↔ NonzeroWithSign a (-s)
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s → NonzeroWithSign a (-s)

case mpr
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign a (-s) → NonzeroWithSign (-a) s

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s → NonzeroWithSign a (-s)
Tactic:
case mp =>
  intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : -a ≃ s * coe n))
  show NonzeroWithSign a (-s)
  have : a ≃ -s * coe n := calc
    a              ≃ _ := Rel.symm neg_involutive
    (-(-a))        ≃ _ := AA.subst₁ ‹-a ≃ s * coe n›
    (-(s * coe n)) ≃ _ := AA.scompatL
    (-s) * coe n   ≃ _ := Rel.refl
  exact NonzeroWithSign.intro n ‹Positive n› ‹a ≃ -s * coe n›
State after:
no goals

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign a (-s) → NonzeroWithSign (-a) s
Tactic:
case mpr =>
  intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : a ≃ -s * coe n))
  show NonzeroWithSign (-a) s
  have : -a ≃ s * coe n := calc
    (-a)            ≃ _ := AA.subst₁ ‹a ≃ -s * coe n›
    (-(-s * coe n)) ≃ _ := AA.scompatL
    (-(-s)) * coe n ≃ _ := AA.substL neg_involutive
    s * coe n       ≃ _ := Rel.refl
  exact NonzeroWithSign.intro n ‹Positive n› ‹-a ≃ s * coe n›
State after:
no goals

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign (-a) s → NonzeroWithSign a (-s)
Tactic:
intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : -a ≃ s * coe n))
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : -a ≃ s * coe n
⊢ NonzeroWithSign a (-s)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : -a ≃ s * coe n
⊢ NonzeroWithSign a (-s)
Tactic:
have : a ≃ -s * coe n := calc
  a              ≃ _ := Rel.symm neg_involutive
  (-(-a))        ≃ _ := AA.subst₁ ‹-a ≃ s * coe n›
  (-(s * coe n)) ≃ _ := AA.scompatL
  (-s) * coe n   ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : -a ≃ s * coe n
this : a ≃ -s * coe n
⊢ NonzeroWithSign a (-s)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : -a ≃ s * coe n
this : a ≃ -s * coe n
⊢ NonzeroWithSign a (-s)
Tactic:
exact NonzeroWithSign.intro n ‹Positive n› ‹a ≃ -s * coe n›
State after:
no goals

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
⊢ NonzeroWithSign a (-s) → NonzeroWithSign (-a) s
Tactic:
intro (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : a ≃ -s * coe n))
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ -s * coe n
⊢ NonzeroWithSign (-a) s

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ -s * coe n
⊢ NonzeroWithSign (-a) s
Tactic:
have : -a ≃ s * coe n := calc
  (-a)            ≃ _ := AA.subst₁ ‹a ≃ -s * coe n›
  (-(-s * coe n)) ≃ _ := AA.scompatL
  (-(-s)) * coe n ≃ _ := AA.substL neg_involutive
  s * coe n       ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ -s * coe n
this : -a ≃ s * coe n
⊢ NonzeroWithSign (-a) s

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a s : ℤ
x✝ : Sqrt1 s
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ -s * coe n
this : -a ≃ s * coe n
⊢ NonzeroWithSign (-a) s
Tactic:
exact NonzeroWithSign.intro n ‹Positive n› ‹-a ≃ s * coe n›
State after:
no goals