Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_positive (Lean4Axiomatic/Rational/Impl/Fraction/Reciprocation.lean)

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
⊢ (a//b)⁻¹ ≃ b//a
Tactic:
have : sgn a ≃ 1 := Integer.sgn_positive.mp ‹AP (Positive a)›.ev
State after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
⊢ (a//b)⁻¹ ≃ b//a

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
⊢ (a//b)⁻¹ ≃ b//a
Tactic:
have x_sgn_a {x : ℤ} : x * sgn a ≃ x := calc
  x * sgn a ≃ _ := AA.substR ‹sgn a ≃ 1›
  x * 1     ≃ _ := AA.identR
  x         ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
x_sgn_a : ∀ {x : ℤ}, x * sgn a ≃ x
⊢ (a//b)⁻¹ ≃ b//a

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
x_sgn_a : ∀ {x : ℤ}, x * sgn a ≃ x
⊢ (a//b)⁻¹ ≃ b//a
Tactic:
calc
  (a//b)⁻¹                 ≃ _ := eqv_refl
  (b * sgn a)//(a * sgn a) ≃ _ := substN x_sgn_a
  b//(a * sgn a)           ≃ _ := substD x_sgn_a
  b//a                     ≃ _ := eqv_refl
State after:
no goals