Theorem: Lean4Axiomatic.Rational.sgn_sqrt1_iff_nonzero (Lean4Axiomatic/Rational/Sign.lean)

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
⊢ Integer.Sqrt1 (sgn p) ↔ p ≄ 0
Tactic:
have : Integer.Sqrt1 (sgn (sgn p)) ↔ Integer.Sqrt1 (sgn p) :=
  Rel.iff_subst_eqv Integer.sqrt1_subst sgn_idemp
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
this : Integer.Sqrt1 (sgn (sgn p)) ↔ Integer.Sqrt1 (sgn p)
⊢ Integer.Sqrt1 (sgn p) ↔ p ≄ 0

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
this : Integer.Sqrt1 (sgn (sgn p)) ↔ Integer.Sqrt1 (sgn p)
⊢ Integer.Sqrt1 (sgn p) ↔ p ≄ 0
Tactic:
calc
  _ ↔ Integer.Sqrt1 (sgn p)       := Rel.refl
  _ ↔ Integer.Sqrt1 (sgn (sgn p)) := this.symm
  _ ↔ Integer.Nonzero (sgn p)     := Integer.sgn_nonzero.symm
  _ ↔ sgn p ≄ 0                   := Integer.nonzero_iff_neqv_zero
  _ ↔ p ≄ 0                       := Logic.iff_subst_contra mt sgn_zero.symm
State after:
no goals