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

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
⊢ s₁ ≃ s₂
Tactic:
have : s₁ ≃ 1 ∨ s₁ ≃ -1 := sqrt1_cases.mp ‹Sqrt1 s₁›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this : s₁ ≃ 1 ∨ s₁ ≃ -1
⊢ s₁ ≃ s₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this : s₁ ≃ 1 ∨ s₁ ≃ -1
⊢ s₁ ≃ s₂
Tactic:
have : s₂ ≃ 1 ∨ s₂ ≃ -1 := sqrt1_cases.mp ‹Sqrt1 s₂›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝ : s₁ ≃ 1 ∨ s₁ ≃ -1
this : s₂ ≃ 1 ∨ s₂ ≃ -1
⊢ s₁ ≃ s₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝ : s₁ ≃ 1 ∨ s₁ ≃ -1
this : s₂ ≃ 1 ∨ s₂ ≃ -1
⊢ s₁ ≃ s₂
Tactic:
have : s₁ ≃ s₂ ∨ (NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)) :=
  match ‹s₁ ≃ 1 ∨ s₁ ≃ -1› with
  | Or.inl (_ : s₁ ≃ 1) =>
    match ‹s₂ ≃ 1 ∨ s₂ ≃ -1› with
    | Or.inl (_ : s₂ ≃ 1) =>
      have : s₁ ≃ s₂ := Rel.trans ‹s₁ ≃ 1› (Rel.symm ‹s₂ ≃ 1›)
      Or.inl ‹s₁ ≃ s₂›
    | Or.inr (_ : s₂ ≃ -1) =>
      have : NonzeroWithSign a 1 :=
        NonzeroWithSign.subst_sign ‹s₁ ≃ 1› ‹NonzeroWithSign a s₁›
      have : NonzeroWithSign a (-1) :=
        NonzeroWithSign.subst_sign ‹s₂ ≃ -1› ‹NonzeroWithSign a s₂›
      Or.inr (And.intro ‹NonzeroWithSign a 1› ‹NonzeroWithSign a (-1)›)
  | Or.inr (_ : s₁ ≃ -1) =>
    match ‹s₂ ≃ 1 ∨ s₂ ≃ -1› with
    | Or.inl (_ : s₂ ≃ 1) =>
      have : NonzeroWithSign a (-1) :=
        NonzeroWithSign.subst_sign ‹s₁ ≃ -1› ‹NonzeroWithSign a s₁›
      have : NonzeroWithSign a 1 :=
        NonzeroWithSign.subst_sign ‹s₂ ≃ 1› ‹NonzeroWithSign a s₂›
      Or.inr (And.intro ‹NonzeroWithSign a 1› ‹NonzeroWithSign a (-1)›)
    | Or.inr (_ : s₂ ≃ -1) =>
      have : s₁ ≃ s₂ := Rel.trans ‹s₁ ≃ -1› (Rel.symm ‹s₂ ≃ -1›)
      Or.inl ‹s₁ ≃ s₂›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
⊢ s₁ ≃ s₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
⊢ s₁ ≃ s₂
Tactic:
match this with
| Or.inl (_ : s₁ ≃ s₂) =>
  exact ‹s₁ ≃ s₂›
| Or.inr (And.intro (_ : NonzeroWithSign a 1) (_ : NonzeroWithSign a (-1))) =>
  have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
  have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
  have : Positive a ∧ Negative a := And.intro ‹Positive a› ‹Negative a›
  exact absurd ‹Positive a ∧ Negative a› not_positive_and_negative
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
h✝ : s₁ ≃ s₂
⊢ s₁ ≃ s₂
Tactic:
exact ‹s₁ ≃ s₂›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝¹ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝ : s₂ ≃ 1 ∨ s₂ ≃ -1
this : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
⊢ s₁ ≃ s₂
Tactic:
have : Positive a := positive_iff_sign_pos1.mpr ‹NonzeroWithSign a 1›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝² : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝¹ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this : Positive a
⊢ s₁ ≃ s₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝² : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝¹ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this : Positive a
⊢ s₁ ≃ s₂
Tactic:
have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝³ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝² : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝¹ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this✝ : Positive a
this : Negative a
⊢ s₁ ≃ s₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝³ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝² : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝¹ : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this✝ : Positive a
this : Negative a
⊢ s₁ ≃ s₂
Tactic:
have : Positive a ∧ Negative a := And.intro ‹Positive a› ‹Negative a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝⁴ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝³ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝² : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this✝¹ : Positive a
this✝ : Negative a
this : Positive a ∧ Negative a
⊢ s₁ ≃ s₂

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s₁ s₂ : ℤ
x✝³ : Sqrt1 s₁
x✝² : Sqrt1 s₂
x✝¹ : NonzeroWithSign a s₁
x✝ : NonzeroWithSign a s₂
this✝⁴ : s₁ ≃ 1 ∨ s₁ ≃ -1
this✝³ : s₂ ≃ 1 ∨ s₂ ≃ -1
this✝² : s₁ ≃ s₂ ∨ NonzeroWithSign a 1 ∧ NonzeroWithSign a (-1)
left✝ : NonzeroWithSign a 1
right✝ : NonzeroWithSign a (-1)
this✝¹ : Positive a
this✝ : Negative a
this : Positive a ∧ Negative a
⊢ s₁ ≃ s₂
Tactic:
exact absurd ‹Positive a ∧ Negative a› not_positive_and_negative
State after:
no goals