case zero

⊢ ∃ a b, b ^ 2 * a = zero ∧ Squarefree a

case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = succ n ∧ Squarefree a
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n ∧ Squarefree a
cases' n with n
no goals
case zero

⊢ ∃ a b, b ^ 2 * a = zero ∧ Squarefree a
exact ⟨1, 0, by simp, squarefree_one⟩
no goals
⊢ 0 ^ 2 * 1 = zero
simp
case succ.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : b ^ 2 * a = succ n
h₂ : Squarefree a
⊢ ∃ a b, b ^ 2 * a = succ n ∧ Squarefree a
case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = succ n ∧ Squarefree a
obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)
no goals
case succ.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : b ^ 2 * a = succ n
h₂ : Squarefree a
⊢ ∃ a b, b ^ 2 * a = succ n ∧ Squarefree a
exact ⟨a, b, h₁, h₂⟩