case mp =>
  intro (_ : Sqrt1 a)
  show a ≃ 1 ∨ a ≃ -1
  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 : ℤ
⊢ Sqrt1 a → a ≃ 1 ∨ a ≃ -1
no goals