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

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a s : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)
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 : ℤ
sqrt1 : Sqrt1 s
x✝ : NonzeroWithSign a s
this : s ≃ 1 ∨ s ≃ -1
⊢ NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1)

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

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

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

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

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