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

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Tactic:
have nws_a : NonzeroWithSign a (sgn a) := sgn_nonzeroWithSign
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Tactic:
have nws_b : NonzeroWithSign b (sgn b) := sgn_nonzeroWithSign
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
nws_b : NonzeroWithSign b (sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
nws_b : NonzeroWithSign b (sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Tactic:
have : NonzeroWithSign (a * b) (sgn a * sgn b) :=
  mul_preserves_nonzeroWithSign nws_a nws_b
State after:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
nws_b : NonzeroWithSign b (sgn b)
this : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)

State before:
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Sign ℤ
a b : ℤ
inst✝¹ : Sqrt1 (sgn a)
inst✝ : Sqrt1 (sgn b)
nws_a : NonzeroWithSign a (sgn a)
nws_b : NonzeroWithSign b (sgn b)
this : NonzeroWithSign (a * b) (sgn a * sgn b)
⊢ NonzeroWithSign (a * b) (sgn a * sgn b)
Tactic:
exact this
State after:
no goals