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

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
⊢ NonzeroWithSign a as → NonzeroWithSign b bs → NonzeroWithSign (a * b) (as * bs)
Tactic:
intro
  (NonzeroWithSign.intro (am : ℕ) (_ : Positive am) (_ : a ≃ as * coe am))
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝ : Positive am
eqv✝ : a ≃ as * coe am
⊢ NonzeroWithSign b bs → NonzeroWithSign (a * b) (as * bs)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝ : Positive am
eqv✝ : a ≃ as * coe am
⊢ NonzeroWithSign b bs → NonzeroWithSign (a * b) (as * bs)
Tactic:
intro
  (NonzeroWithSign.intro (bm : ℕ) (_ : Positive bm) (_ : b ≃ bs * coe bm))
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
⊢ NonzeroWithSign (a * b) (as * bs)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
⊢ NonzeroWithSign (a * b) (as * bs)
Tactic:
have : Positive (am * bm) := Natural.mul_positive ‹Positive am› ‹Positive bm›
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
this : Positive (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
this : Positive (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)
Tactic:
have : a * b ≃ (as * bs) * coe (am * bm) := calc
  a * b                         ≃ _ := AA.substL ‹a ≃ as * coe am›
  (as * coe am) * b             ≃ _ := AA.substR ‹b ≃ bs * coe bm›
  (as * coe am) * (bs * coe bm) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (as * bs) * (coe am * coe bm) ≃ _ := AA.substR (Rel.symm AA.compat₂)
  (as * bs) * coe (am * bm)     ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
this✝ : Positive (am * bm)
this : a * b ≃ as * bs * coe (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝¹ : Positive am
eqv✝¹ : a ≃ as * coe am
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
this✝ : Positive (am * bm)
this : a * b ≃ as * bs * coe (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)
Tactic:
exact NonzeroWithSign.intro
  (am * bm) ‹Positive (am * bm)› ‹a * b ≃ (as * bs) * coe (am * bm)›
State after:
no goals