Theorem: Lean4Axiomatic.Rational.sgn_idemp (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 : ℚ
⊢ sgn (sgn p) ≃ sgn p
Tactic:
have (AsRatio.intro (a : ℤ) (b : ℤ) (_ : Integer.Nonzero b) eqv) :=
  as_ratio p
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
eqv : p ≃ from_integer a / from_integer b
⊢ sgn (sgn p) ≃ sgn p

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
eqv : p ≃ from_integer a / from_integer b
⊢ sgn (sgn p) ≃ sgn p
Tactic:
have : p ≃ a/b := eqv
State after:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
eqv this : p ≃ from_integer a / from_integer b
⊢ sgn (sgn p) ≃ sgn p

State before:
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p : ℚ
a b : ℤ
b_nonzero✝ : Integer.Nonzero b
eqv this : p ≃ from_integer a / from_integer b
⊢ sgn (sgn p) ≃ sgn p
Tactic:
calc
  sgn (sgn p)               ≃ _ := Integer.sgn_subst (sgn_subst ‹p ≃ a/b›)
  sgn (sgn ((a : ℚ)/b))     ≃ _ := Integer.sgn_subst sgn_div_integers
  sgn (sgn a * sgn b)       ≃ _ := Integer.sgn_compat_mul
  sgn (sgn a) * sgn (sgn b) ≃ _ := AA.substL Integer.sgn_idemp
  sgn a * sgn (sgn b)       ≃ _ := AA.substR Integer.sgn_idemp
  sgn a * sgn b             ≃ _ := Rel.symm sgn_div_integers
  sgn ((a : ℚ)/b)           ≃ _ := sgn_subst (eqv_symm ‹p ≃ a/b›)
  sgn p                     ≃ _ := Rel.refl
State after:
no goals