Theorem: Lean4Axiomatic.Rational.Impl.Fraction.neg_subst (Lean4Axiomatic/Rational/Impl/Fraction/Negation.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁ p₂ : Fraction ℤ
⊢ p₁ ≃ p₂ → -p₁ ≃ -p₂
Tactic:
revert p₁
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → -p₁ ≃ -p₂

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
⊢ ∀ {p₁ : Fraction ℤ}, p₁ ≃ p₂ → -p₁ ≃ -p₂
Tactic:
intro (p₁n//p₁d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → -p₁n//p₁d ≃ -p₂

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₁d)
⊢ p₁n//p₁d ≃ p₂ → -p₁n//p₁d ≃ -p₂
Tactic:
revert p₂
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → -p₁n//p₁d ≃ -p₂

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₁d)
⊢ ∀ {p₂ : Fraction ℤ}, p₁n//p₁d ≃ p₂ → -p₁n//p₁d ≃ -p₂
Tactic:
intro (p₂n//p₂d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
⊢ p₁n//p₁d ≃ p₂n//p₂d → -p₁n//p₁d ≃ -p₂n//p₂d

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
⊢ p₁n//p₁d ≃ p₂n//p₂d → -p₁n//p₁d ≃ -p₂n//p₂d
Tactic:
intro (_ : p₁n//p₁d ≃ p₂n//p₂d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ -p₁n//p₁d ≃ -p₂n//p₂d

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ -p₁n//p₁d ≃ -p₂n//p₂d
Tactic:
show -p₁n * p₂d ≃ -p₂n * p₁d
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d
Tactic:
have : p₁n * p₂d ≃ p₂n * p₁d := ‹p₁n//p₁d ≃ p₂n//p₂d›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₁n p₁d : ℤ
denominator_positive✝¹ : Logic.AP (Signed.Positive p₁d)
p₂n p₂d : ℤ
denominator_positive✝ : Logic.AP (Signed.Positive p₂d)
x✝ : p₁n//p₁d ≃ p₂n//p₂d
this : p₁n * p₂d ≃ p₂n * p₁d
⊢ -p₁n * p₂d ≃ -p₂n * p₁d
Tactic:
calc
  (-p₁n) * p₂d   ≃ _ := Rel.symm AA.scompatL
  (-(p₁n * p₂d)) ≃ _ := AA.subst₁ ‹p₁n * p₂d ≃ p₂n * p₁d›
  (-(p₂n * p₁d)) ≃ _ := AA.scompatL
  (-p₂n) * p₁d   ≃ _ := Rel.refl
State after:
no goals