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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 a ↔ a ≃ 1 ∨ a ≃ -1
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 a → a ≃ 1 ∨ a ≃ -1

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ a ≃ 1 ∨ a ≃ -1 → Sqrt1 a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 a → a ≃ 1 ∨ a ≃ -1
Tactic:
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
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ a ≃ 1 ∨ a ≃ -1 → Sqrt1 a
Tactic:
case mpr =>
  intro (_ : a ≃ 1 ∨ a ≃ -1)
  show Sqrt1 a
  match ‹a ≃ 1 ∨ a ≃ -1› with
  | Or.inl (_ : a ≃ 1) =>
    have : Sqrt1 (1 : ℤ) := sqrt1_one
    have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ 1›) ‹Sqrt1 (1 : ℤ)›
    exact this
  | Or.inr (_ : a ≃ -1) =>
    have : Sqrt1 (-1 : ℤ) := sqrt1_neg_one
    have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ -1›) ‹Sqrt1 (-1 : ℤ)›
    exact this
State after:
no goals

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
⊢ a ≃ 1 ∨ a ≃ -1
Tactic:
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
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
⊢ a ≃ 1 ∨ a ≃ -1
Tactic:
apply False.elim
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
⊢ False

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
⊢ False
Tactic:
have : (1 : ℤ) ≃ 0 := calc
  1     ≃ _ := Rel.symm ‹Sqrt1 a›.elim
  a * a ≃ _ := AA.substL ‹a ≃ 0›
  0 * a ≃ _ := AA.absorbL
  0     ≃ _ := Rel.refl
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
this : 1 ≃ 0
⊢ False

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
a✝ : a ≃ 0
this : 1 ≃ 0
⊢ False
Tactic:
exact absurd ‹(1 : ℤ) ≃ 0› one_neqv_zero
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
⊢ a ≃ 1 ∨ a ≃ -1
Tactic:
apply Or.inl
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
⊢ a ≃ 1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
⊢ a ≃ 1
Tactic:
have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ (n : ℤ)))) :=
  positive_elim_nat ‹Positive a›
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
⊢ a ≃ 1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
⊢ a ≃ 1
Tactic:
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
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this : coe (n * n) ≃ 1
⊢ a ≃ 1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this : coe (n * n) ≃ 1
⊢ a ≃ 1
Tactic:
have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ 1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ 1
Tactic:
have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ 1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
b✝ : Positive a
n : ℕ
left✝ : Positive n
right✝ : a ≃ coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ 1
Tactic:
calc
  a       ≃ _ := ‹a ≃ (n : ℤ)›
  (n : ℤ) ≃ _ := AA.subst₁ ‹n ≃ 1›
  (1 : ℤ) ≃ _ := Rel.refl
  (1 : ℤ) ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
⊢ a ≃ 1 ∨ a ≃ -1
Tactic:
apply Or.inr
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
⊢ a ≃ -1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
⊢ a ≃ -1
Tactic:
have (Exists.intro (n : ℕ) (And.intro _ (_ : a ≃ -(n : ℤ)))) :=
  negative_elim_nat ‹Negative a›
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
⊢ a ≃ -1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
⊢ a ≃ -1
Tactic:
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
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this : coe (n * n) ≃ 1
⊢ a ≃ -1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this : coe (n * n) ≃ 1
⊢ a ≃ -1
Tactic:
have : n * n ≃ 1 := AA.inject ‹((n * n : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ)›
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ -1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝ : coe (n * n) ≃ 1
this : n * n ≃ 1
⊢ a ≃ -1
Tactic:
have : n ≃ 1 := Natural.sqrt1.mp ‹n * n ≃ 1›
State after:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ -1

State before:
case h
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 a
c✝ : Negative a
n : ℕ
left✝ : Positive n
right✝ : a ≃ -coe n
this✝¹ : coe (n * n) ≃ 1
this✝ : n * n ≃ 1
this : n ≃ 1
⊢ a ≃ -1
Tactic:
calc
  a          ≃ _ := ‹a ≃ -(n : ℤ)›
  (-(n : ℤ)) ≃ _ := AA.subst₁ (AA.subst₁ ‹n ≃ 1›)
  (-(1 : ℤ)) ≃ _ := Rel.refl
  (-1)       ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
⊢ Sqrt1 a
Tactic:
match ‹a ≃ 1 ∨ a ≃ -1› with
| Or.inl (_ : a ≃ 1) =>
  have : Sqrt1 (1 : ℤ) := sqrt1_one
  have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ 1›) ‹Sqrt1 (1 : ℤ)›
  exact this
| Or.inr (_ : a ≃ -1) =>
  have : Sqrt1 (-1 : ℤ) := sqrt1_neg_one
  have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ -1›) ‹Sqrt1 (-1 : ℤ)›
  exact this
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
⊢ Sqrt1 a
Tactic:
have : Sqrt1 (1 : ℤ) := sqrt1_one
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
this : Sqrt1 1
⊢ Sqrt1 a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
this : Sqrt1 1
⊢ Sqrt1 a
Tactic:
have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ 1›) ‹Sqrt1 (1 : ℤ)›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
this✝ : Sqrt1 1
this : Sqrt1 a
⊢ Sqrt1 a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ 1
this✝ : Sqrt1 1
this : Sqrt1 a
⊢ Sqrt1 a
Tactic:
exact this
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ -1
⊢ Sqrt1 a
Tactic:
have : Sqrt1 (-1 : ℤ) := sqrt1_neg_one
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ -1
this : Sqrt1 (-1)
⊢ Sqrt1 a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ -1
this : Sqrt1 (-1)
⊢ Sqrt1 a
Tactic:
have : Sqrt1 a := AA.substFn (Rel.symm ‹a ≃ -1›) ‹Sqrt1 (-1 : ℤ)›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : a ≃ 1 ∨ a ≃ -1
h✝ : a ≃ -1
this✝ : Sqrt1 (-1)
this : Sqrt1 a
⊢ Sqrt1 a

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