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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
intro (_ : Nonzero a)
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
have (Nonzero.intro (sa : ℤ) (_ : Sqrt1 sa) nws) := ‹Nonzero a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
have (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : a ≃ sa * n)) := nws
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
have : a * a ≃ (n * n : ℕ) := calc
  a * a               ≃ _ := AA.substL ‹a ≃ sa * n›
  (sa * n) * a        ≃ _ := AA.substR ‹a ≃ sa * n›
  (sa * n) * (sa * n) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (sa * sa) * (n * n) ≃ _ := AA.substL ‹Sqrt1 sa›.elim
  (1 : ℤ) * (n * n)   ≃ _ := AA.identL
  (n : ℤ) * n         ≃ _ := Rel.symm AA.compat₂
  ((n * n : ℕ) : ℤ)   ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
this : a * a ≃ coe (n * n)
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
this : a * a ≃ coe (n * n)
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
exact Exists.intro n (And.intro ‹Positive n› ‹a * a ≃ (n * n : ℕ)›)
State after:
no goals