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

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

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Sqrt1 (sgn a) → Nonzero a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → Sqrt1 (sgn a)
Tactic:
case mp =>
  intro (_ : Nonzero a)
  show Sqrt1 (sgn a)
  have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
  match this with
  | Or.inl (_ : Positive a) =>
    have : 1 ≃ sgn a := Rel.symm (sgn_positive.mp ‹Positive a›)
    have : Sqrt1 (1:ℤ) := sqrt1_one
    have : Sqrt1 (sgn a) := sqrt1_subst ‹1 ≃ sgn a› ‹Sqrt1 (1:ℤ)›
    exact this
  | Or.inr (_ : Negative a) =>
    have : -1 ≃ sgn a := Rel.symm (sgn_negative.mp ‹Negative a›)
    have : Sqrt1 (-1:ℤ) := sqrt1_neg_one
    have : Sqrt1 (sgn a) := sqrt1_subst ‹-1 ≃ sgn a› ‹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 (sgn a) → Nonzero a
Tactic:
case mpr =>
  intro (_ : Sqrt1 (sgn a))
  show Nonzero a
  have : sgn a ≃ 1 ∨ sgn a ≃ -1 := sqrt1_cases.mp ‹Sqrt1 (sgn a)›
  have : Positive a ∨ Negative a := match this with
  | Or.inl (_ : sgn a ≃ 1) =>
    have : Positive a := sgn_positive.mpr ‹sgn a ≃ 1›
    Or.inl this
  | Or.inr (_ : sgn a ≃ -1) =>
    have : Negative a := sgn_negative.mpr ‹sgn a ≃ -1›
    Or.inr this
  have : Nonzero a := nonzero_iff_pos_or_neg.mpr ‹Positive a ∨ Negative a›
  exact this
State after:
no goals

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ Sqrt1 (sgn a)
Tactic:
have : Positive a ∨ Negative a := nonzero_iff_pos_or_neg.mp ‹Nonzero a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ Sqrt1 (sgn a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this : Positive a ∨ Negative a
⊢ Sqrt1 (sgn a)
Tactic:
match this with
| Or.inl (_ : Positive a) =>
  have : 1 ≃ sgn a := Rel.symm (sgn_positive.mp ‹Positive a›)
  have : Sqrt1 (1:ℤ) := sqrt1_one
  have : Sqrt1 (sgn a) := sqrt1_subst ‹1 ≃ sgn a› ‹Sqrt1 (1:ℤ)›
  exact this
| Or.inr (_ : Negative a) =>
  have : -1 ≃ sgn a := Rel.symm (sgn_negative.mp ‹Negative a›)
  have : Sqrt1 (-1:ℤ) := sqrt1_neg_one
  have : Sqrt1 (sgn a) := sqrt1_subst ‹-1 ≃ sgn a› ‹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✝ : Nonzero a
this : Positive a ∨ Negative a
h✝ : Positive a
⊢ Sqrt1 (sgn a)
Tactic:
have : 1 ≃ sgn a := Rel.symm (sgn_positive.mp ‹Positive a›)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Positive a ∨ Negative a
h✝ : Positive a
this : 1 ≃ sgn a
⊢ Sqrt1 (sgn a)

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝¹ : Positive a ∨ Negative a
h✝ : Positive a
this✝ : 1 ≃ sgn a
this : Sqrt1 1
⊢ Sqrt1 (sgn a)
Tactic:
have : Sqrt1 (sgn a) := sqrt1_subst ‹1 ≃ sgn a› ‹Sqrt1 (1:ℤ)›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Positive a ∨ Negative a
h✝ : Positive a
this✝¹ : 1 ≃ sgn a
this✝ : Sqrt1 1
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn a)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Positive a ∨ Negative a
h✝ : Positive a
this✝¹ : 1 ≃ sgn a
this✝ : Sqrt1 1
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn 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✝ : Nonzero a
this : Positive a ∨ Negative a
h✝ : Negative a
⊢ Sqrt1 (sgn a)
Tactic:
have : -1 ≃ sgn a := Rel.symm (sgn_negative.mp ‹Negative a›)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝ : Positive a ∨ Negative a
h✝ : Negative a
this : -1 ≃ sgn a
⊢ Sqrt1 (sgn a)

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

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
this✝² : Positive a ∨ Negative a
h✝ : Negative a
this✝¹ : -1 ≃ sgn a
this✝ : Sqrt1 (-1)
this : Sqrt1 (sgn a)
⊢ Sqrt1 (sgn 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 : ℤ
⊢ Sqrt1 (sgn a) → Nonzero a
Tactic:
intro (_ : Sqrt1 (sgn a))
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
⊢ Nonzero a

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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this : sgn a ≃ 1 ∨ sgn a ≃ -1
⊢ Nonzero a
Tactic:
have : Positive a ∨ Negative a := match this with
| Or.inl (_ : sgn a ≃ 1) =>
  have : Positive a := sgn_positive.mpr ‹sgn a ≃ 1›
  Or.inl this
| Or.inr (_ : sgn a ≃ -1) =>
  have : Negative a := sgn_negative.mpr ‹sgn a ≃ -1›
  Or.inr this
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this✝ : sgn a ≃ 1 ∨ sgn a ≃ -1
this : Positive a ∨ Negative a
⊢ Nonzero a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this✝ : sgn a ≃ 1 ∨ sgn a ≃ -1
this : Positive a ∨ Negative a
⊢ Nonzero a
Tactic:
have : Nonzero a := nonzero_iff_pos_or_neg.mpr ‹Positive a ∨ Negative a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Sqrt1 (sgn a)
this✝¹ : sgn a ≃ 1 ∨ sgn a ≃ -1
this✝ : Positive a ∨ Negative a
this : Nonzero a
⊢ Nonzero a

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