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

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → Nonzero a₁ → Nonzero a₂
Tactic:
intro (_ : a₁ ≃ a₂) (Nonzero.intro (s : ℤ) (_ : Sqrt1 s) nws)
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws : NonzeroWithSign a₁ s
⊢ Nonzero a₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws : NonzeroWithSign a₁ s
⊢ Nonzero a₂
Tactic:
have : NonzeroWithSign a₁ s := nws
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this : NonzeroWithSign a₁ s
⊢ Nonzero a₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this : NonzeroWithSign a₁ s
⊢ Nonzero a₂
Tactic:
have : NonzeroWithSign a₂ s :=
  NonzeroWithSign.subst_nonzero ‹a₁ ≃ a₂› ‹NonzeroWithSign a₁ s›
State after:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this✝ : NonzeroWithSign a₁ s
this : NonzeroWithSign a₂ s
⊢ Nonzero a₂

State before:
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
s : ℤ
sqrt1✝ : Sqrt1 s
nws this✝ : NonzeroWithSign a₁ s
this : NonzeroWithSign a₂ s
⊢ Nonzero a₂
Tactic:
exact Nonzero.mk ‹NonzeroWithSign a₂ s›
State after:
no goals