Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_zero_only_for_zero (Lean4Axiomatic/Rational/Impl/Fraction/Sign.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ sgn p ≃ 0 → p ≃ 0
Tactic:
intro (_ : sgn p ≃ 0)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
⊢ p ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
⊢ p ≃ 0
Tactic:
have : sgn p.numerator ≃ 0 := ‹sgn p ≃ 0›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this : sgn p.numerator ≃ 0
⊢ p ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this : sgn p.numerator ≃ 0
⊢ p ≃ 0
Tactic:
have : p.numerator ≃ 0 := Integer.sgn_zero.mpr this
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝ : sgn p.numerator ≃ 0
this : p.numerator ≃ 0
⊢ p ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝ : sgn p.numerator ≃ 0
this : p.numerator ≃ 0
⊢ p ≃ 0
Tactic:
have : p ≃ 0 := eqv_zero_iff_numerator_eqv_zero.mpr this
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝¹ : sgn p.numerator ≃ 0
this✝ : p.numerator ≃ 0
this : p ≃ 0
⊢ p ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝¹ : sgn p.numerator ≃ 0
this✝ : p.numerator ≃ 0
this : p ≃ 0
⊢ p ≃ 0
Tactic:
exact this
State after:
no goals