match (sign_trichotomy a).atLeastOne with
| AA.OneOfThree.first (_ : a ≃ 0) =>
  apply False.elim
  show False
  have : (1 : ℤ) ≃ 0 := calc
    1     ≃ _ := Rel.symm ‹Sqrt1 a›.elim
    a * a ≃ _ := AA.substL ‹a ≃ 0›
    0 * a ≃ _ := AA.absorbL
    0     ≃ _ := Rel.refl
  exact absurd ‹(1 : ℤ) ≃ 0› one_neqv_zero
| AA.OneOfThree.second (_ : Positive a) =>
  apply Or.inl
  show a ≃ 1
  have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ (n : ℤ)))) :=
    positive_elim_nat ‹Positive a›
  have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
    ((n * n : ℕ) : ℤ) ≃ _ := AA.compat₂
    (n : ℤ) * (n : ℤ) ≃ _ := AA.substL (Rel.symm ‹a ≃ (n : ℤ)›)
    a * (n : ℤ)       ≃ _ := AA.substR (Rel.symm ‹a ≃ (n : ℤ)›)
    a * a             ≃ _ := ‹Sqrt1 a›.elim
    1                 ≃ _ := Rel.refl
  have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
  have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
  show a ≃ 1
  calc
    a       ≃ _ := ‹a ≃ (n : ℤ)›
    (n : ℤ) ≃ _ := AA.subst₁ ‹n ≃ 1›
    (1 : ℤ) ≃ _ := Rel.refl
    (1 : ℤ) ≃ _ := Rel.refl
| AA.OneOfThree.third (_ : Negative a) =>
  apply Or.inr
  show a ≃ -1
  have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ -(n : ℤ)))) :=
    negative_elim_nat ‹Negative a›
  have : ((n * n : ℕ) : ℤ) ≃ (1 : ℤ) := calc
    ((n * n : ℕ) : ℤ)         ≃ _ := AA.compat₂
    (n : ℤ) * (n : ℤ)         ≃ _ := Rel.symm neg_involutive
    (-(-((n : ℤ) * (n : ℤ)))) ≃ _ := AA.subst₁ AA.scompatR
    (-((n : ℤ) * -(n : ℤ)))   ≃ _ := AA.scompatL
    (-(n : ℤ)) * (-(n : ℤ))   ≃ _ := AA.substL (Rel.symm ‹a ≃ -(n : ℤ)›)
    a * (-(n : ℤ))            ≃ _ := AA.substR (Rel.symm ‹a ≃ -(n : ℤ)›)
    a * a                     ≃ _ := ‹Sqrt1 a›.elim
    1                         ≃ _ := Rel.refl
  have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
  have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
  show a ≃ -1
  calc
    a          ≃ _ := ‹a ≃ -(n : ℤ)›
    (-(n : ℤ)) ≃ _ := AA.subst₁ (AA.subst₁ ‹n ≃ 1›)
    (-(1 : ℤ)) ≃ _ := Rel.refl
    (-1)       ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
⊢ a ≃ 1 ∨ a ≃ -1
no goals