Theorem: Lean4Axiomatic.Integer.sgn_subst (Lean4Axiomatic/Integer/Sign.lean)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → sgn a₁ ≃ sgn a₂
Tactic:
intro (_ : a₁ ≃ a₂)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ sgn a₁ ≃ sgn a₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ sgn a₁ ≃ sgn a₂
Tactic:
have : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁) :=
  (sign_trichotomy a₁).atLeastOne
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
⊢ sgn a₁ ≃ sgn a₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
⊢ sgn a₁ ≃ sgn a₂
Tactic:
match this with
| AA.OneOfThree.first (_ : a₁ ≃ 0) =>
  have : a₂ ≃ 0 := AA.substLFn ‹a₁ ≃ a₂› ‹a₁ ≃ 0›
  calc
    sgn a₁ ≃ _ := sgn_zero.mp ‹a₁ ≃ 0›
    0      ≃ _ := Rel.symm (sgn_zero.mp ‹a₂ ≃ 0›)
    sgn a₂ ≃ _ := Rel.refl
| AA.OneOfThree.second (_ : Positive a₁) =>
  have : Positive a₂ := positive_subst ‹a₁ ≃ a₂› ‹Positive a₁›
  calc
    sgn a₁ ≃ _ := sgn_positive.mp ‹Positive a₁›
    1      ≃ _ := Rel.symm (sgn_positive.mp ‹Positive a₂›)
    sgn a₂ ≃ _ := Rel.refl
| AA.OneOfThree.third (_ : Negative a₁) =>
  have : Negative a₂ := negative_subst ‹a₁ ≃ a₂› ‹Negative a₁›
  calc
    sgn a₁ ≃ _ := sgn_negative.mp ‹Negative a₁›
    (-1)   ≃ _ := Rel.symm (sgn_negative.mp ‹Negative a₂›)
    sgn a₂ ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
a✝ : a₁ ≃ 0
⊢ sgn a₁ ≃ sgn a₂
Tactic:
have : a₂ ≃ 0 := AA.substLFn ‹a₁ ≃ a₂› ‹a₁ ≃ 0›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
a✝ : a₁ ≃ 0
this : a₂ ≃ 0
⊢ sgn a₁ ≃ sgn a₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
a✝ : a₁ ≃ 0
this : a₂ ≃ 0
⊢ sgn a₁ ≃ sgn a₂
Tactic:
calc
  sgn a₁ ≃ _ := sgn_zero.mp ‹a₁ ≃ 0›
  0      ≃ _ := Rel.symm (sgn_zero.mp ‹a₂ ≃ 0›)
  sgn a₂ ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
b✝ : Positive a₁
⊢ sgn a₁ ≃ sgn a₂
Tactic:
have : Positive a₂ := positive_subst ‹a₁ ≃ a₂› ‹Positive a₁›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
b✝ : Positive a₁
this : Positive a₂
⊢ sgn a₁ ≃ sgn a₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
b✝ : Positive a₁
this : Positive a₂
⊢ sgn a₁ ≃ sgn a₂
Tactic:
calc
  sgn a₁ ≃ _ := sgn_positive.mp ‹Positive a₁›
  1      ≃ _ := Rel.symm (sgn_positive.mp ‹Positive a₂›)
  sgn a₂ ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
c✝ : Negative a₁
⊢ sgn a₁ ≃ sgn a₂
Tactic:
have : Negative a₂ := negative_subst ‹a₁ ≃ a₂› ‹Negative a₁›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
c✝ : Negative a₁
this : Negative a₂
⊢ sgn a₁ ≃ sgn a₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
this✝ : AA.OneOfThree (a₁ ≃ 0) (Positive a₁) (Negative a₁)
c✝ : Negative a₁
this : Negative a₂
⊢ sgn a₁ ≃ sgn a₂
Tactic:
calc
  sgn a₁ ≃ _ := sgn_negative.mp ‹Negative a₁›
  (-1)   ≃ _ := Rel.symm (sgn_negative.mp ‹Negative a₂›)
  sgn a₂ ≃ _ := Rel.refl
State after:
no goals