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

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b : ℤ
⊢ Nonzero a → Nonzero b → Nonzero (a * b)
Tactic:
intro (Nonzero.intro as (_ : Sqrt1 as) nwsa)
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝ : Sqrt1 as
nwsa : NonzeroWithSign a as
⊢ Nonzero b → Nonzero (a * b)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝ : Sqrt1 as
nwsa : NonzeroWithSign a as
⊢ Nonzero b → Nonzero (a * b)
Tactic:
intro (Nonzero.intro bs (_ : Sqrt1 bs) nwsb)
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
⊢ Nonzero (a * b)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
⊢ Nonzero (a * b)
Tactic:
have : NonzeroWithSign a as := nwsa
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this : NonzeroWithSign a as
⊢ Nonzero (a * b)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this : NonzeroWithSign a as
⊢ Nonzero (a * b)
Tactic:
have : NonzeroWithSign b bs := nwsb
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this✝ : NonzeroWithSign a as
this : NonzeroWithSign b bs
⊢ Nonzero (a * b)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this✝ : NonzeroWithSign a as
this : NonzeroWithSign b bs
⊢ Nonzero (a * b)
Tactic:
have : NonzeroWithSign (a * b) (as * bs) :=
  mul_preserves_nonzeroWithSign ‹NonzeroWithSign a as› ‹NonzeroWithSign b bs›
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this✝¹ : NonzeroWithSign a as
this✝ : NonzeroWithSign b bs
this : NonzeroWithSign (a * b) (as * bs)
⊢ Nonzero (a * b)

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
this✝¹ : NonzeroWithSign a as
this✝ : NonzeroWithSign b bs
this : NonzeroWithSign (a * b) (as * bs)
⊢ Nonzero (a * b)
Tactic:
exact Nonzero.mk ‹NonzeroWithSign (a * b) (as * bs)›
State after:
no goals