awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n

Tactic:
exact (psub_eq_none.2 (not_le.1 h)).symm

Premises used: not_le, Iff.mpr, Nat.psub_eq_none, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
s : ℕ := n.sqrt
⊢ s * s + (n - s * s) = n

Tactic:
have sm : s * s + (n - s * s) = n := Nat.add_sub_cancel' (sqrt_le _)
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
pos : ∀ (h : n - n.sqrt * n.sqrt < n.sqrt), pair (n - n.sqrt * n.sqrt, n.sqrt).1 (n - n.sqrt * n.sqrt, n.sqrt).2 = n
neg :
  ∀ (h : ¬n - n.sqrt * n.sqrt < n.sqrt),
    pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : n - n.sqrt * n.sqrt < n.sqrt
⊢ pair (n - n.sqrt * n.sqrt, n.sqrt).1 (n - n.sqrt * n.sqrt, n.sqrt).2 = n

Tactic:
simp [s, pair, h, sm]

Premises used: Nat.pair
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
rw : n ≤ s * s + s + s
⊢ n ≤ s * s + (s + s)

Tactic:
rw [← Nat.add_assoc]

Premises used: Nat.add_assoc
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n ≤ s * s + s + s

Tactic:
apply sqrt_le_add

Premises used: Nat.sqrt_le_add
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ n - s * s - s ≤ s

Tactic:
have hl : n - s * s - s ≤ s := Nat.sub_le_iff_le_add.2
      (Nat.sub_le_iff_le_add'.2 <| by rw [← Nat.add_assoc]; apply sqrt_le_add)
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
hl : n - s * s - s ≤ s
⊢ pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n

Tactic:
simp [s, pair, hl.not_gt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]

Premises used: le_of_not_gt, Nat.pair, LE.le.not_gt, Nat.add_assoc, Nat.add_sub_cancel'
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n a b : ℕ
H : unpair n = (a, b)
⊢ pair a b = n

Tactic:
simpa [H] using pair_unpair n

Premises used: Nat.pair_unpair
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
pos : ∀ (h : a < b), unpair (b * b + a) = (a, b)
neg : ∀ (h : ¬a < b), unpair (a * a + a + b) = (a, b)
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : a < b
⊢ (b * b + a).sqrt = b

Tactic:
have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : a < b
be : (b * b + a).sqrt = b
⊢ unpair (b * b + a) = (a, b)

Tactic:
simp [unpair, be, Nat.add_sub_cancel_left, h]

Premises used: Nat.unpair, Nat.add_sub_cancel_left
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : ¬a < b
h₁ : a + b ≤ a + a
⊢ (a * a + (a + b)).sqrt = a

Tactic:
rw [sqrt_add_eq]

Premises used: Nat.sqrt_add_eq
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : ¬a < b
⊢ a + b ≤ a + a

Tactic:
Nat.add_le_add_left (le_of_not_gt h) _

Premises used: le_of_not_gt, Nat.add_le_add_left
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : ¬a < b
⊢ a + b ≤ a + a

Tactic:
exact Nat.add_le_add_left (le_of_not_gt h) _

Premises used: le_of_not_gt, Nat.add_le_add_left
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : ¬a < b
⊢ (a * a + (a + b)).sqrt = a

Tactic:
have ae : sqrt (a * a + (a + b)) = a := by
      rw [sqrt_add_eq]
      exact Nat.add_le_add_left (le_of_not_gt h) _
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : ¬a < b
ae : (a * a + (a + b)).sqrt = a
⊢ unpair (a * a + a + b) = (a, b)

Tactic:
simp [unpair, ae, Nat.add_assoc, Nat.add_sub_cancel_left]

Premises used: Nat.unpair, Nat.add_sub_cancel_left, Nat.add_assoc
-- Module: Mathlib.Data.Nat.Pairing
Goal:
⊢ Surjective unpair

Tactic:
pairEquiv.symm.surjective

Premises used: Nat.unpair, Equiv.surjective, Nat.pairEquiv, Equiv.symm, ite
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b c d : ℕ
⊢ pair a b = pair c d ↔ a = c ∧ b = d

Tactic:
pairEquiv.injective.eq_iff.trans (@Prod.ext_iff ℕ ℕ (a, b) (c, d))

Premises used: Function.Injective.eq_iff, Prod.ext_iff, Nat.pair, Iff.trans, Equiv.injective, Nat.pairEquiv, ite
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
pos :
  ∀ (h : n - s * s < s),
    (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 <
      n
neg :
  ∀ (h : ¬n - s * s < s),
    (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 <
      n
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n

Tactic:
by_cases h : n - s * s < s
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
pos : n - n.sqrt * n.sqrt < n
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n

Tactic:
simp only [h, ↓reduceIte, gt_iff_lt, s]

Premises used: gt_iff_lt, reduceIte
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
neg : n.sqrt < n
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n

Tactic:
simp only [h, ↓reduceIte, gt_iff_lt, s]

Premises used: gt_iff_lt, reduceIte
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ n - n.sqrt * n.sqrt < n

Tactic:
lt_of_lt_of_le h (sqrt_le_self _)

Premises used: Nat.sqrt_le_self, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ n - n.sqrt * n.sqrt < n

Tactic:
exact lt_of_lt_of_le h (sqrt_le_self _)

Premises used: Nat.sqrt_le_self, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ s ≤ n - s * s

Tactic:
simp only [not_lt] at h

Premises used: not_lt
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
⊢ 0 < s

Tactic:
have s0 : 0 < s := sqrt_pos.2 n1
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
s0 : 0 < s
⊢ n.sqrt < n

Tactic:
lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

Premises used: lt_of_le_of_lt, Nat.mul_pos, Nat.sub_lt
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
s0 : 0 < s
⊢ n.sqrt < n

Tactic:
exact lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

Premises used: lt_of_le_of_lt, Nat.mul_pos, Nat.sub_lt
-- Module: Mathlib.Data.Nat.Pairing
Goal:
⊢ (if 0 - sqrt 0 * sqrt 0 < sqrt 0 then (0 - sqrt 0 * sqrt 0, sqrt 0) else (sqrt 0, 0 - sqrt 0 * sqrt 0 - sqrt 0)) = 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Pairing
Goal:
⊢ (unpair 0).1 ≤ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
⊢ a ≤ pair a b

Tactic:
simpa using unpair_left_le (pair a b)

Premises used: Nat.pair, Nat.unpair_left_le
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
pos : ∀ (h : a < b), b ≤ pair a b
neg : ∀ (h : ¬a < b), b ≤ pair a b
⊢ b ≤ pair a b

Tactic:
by_cases h : a < b
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : a < b
⊢ b ≤ pair a b

Tactic:
simpa [pair, h] using le_trans (le_mul_self _) (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, Nat.pair, Nat.le_mul_self, le_trans
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b : ℕ
h : ¬a < b
⊢ b ≤ pair a b

Tactic:
simp [pair, h]

Premises used: Nat.pair
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
⊢ (unpair n).2 ≤ n

Tactic:
simpa using right_le_pair n.unpair.1 n.unpair.2

Premises used: Nat.unpair, Prod.fst, Nat.right_le_pair, Prod.snd
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
pos : ∀ (h₁ : a₁ < b), pair a₁ b < pair a₂ b
neg : ∀ (h₁ : ¬a₁ < b), pair a₁ b < pair a₂ b
⊢ pair a₁ b < pair a₂ b

Tactic:
by_cases h₁ : a₁ < b
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
pos : b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
⊢ pair a₁ b < pair a₂ b

Tactic:
simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]

Premises used: Nat.pair, Nat.add_assoc, reduceIte
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
neg : a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
⊢ pair a₁ b < pair a₂ b

Tactic:
simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]

Premises used: Nat.pair, Nat.add_assoc, reduceIte
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
pos : ∀ (h₂ : a₂ < b), b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
neg : ∀ (h₂ : ¬a₂ < b), b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
by_cases h₂ : a₂ < b
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp [h₂, h]
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
neg : b * b + a₁ < a₂ * a₂ + (a₂ + b)
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp only [h₂, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
neg : b * b ≤ a₂ * a₂
neg₁ : a₁ < a₂ + b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)

Tactic:
apply Nat.add_lt_add_of_le_of_lt

Premises used: Nat.add_lt_add_of_le_of_lt
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b ≤ a₂ * a₂

Tactic:
Nat.mul_self_le_mul_self (not_lt.mp h₂)

Premises used: Nat.mul_self_le_mul_self, not_lt, Iff.mp
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b ≤ a₂ * a₂

Tactic:
exact Nat.mul_self_le_mul_self (not_lt.mp h₂)

Premises used: Nat.mul_self_le_mul_self, not_lt, Iff.mp
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ a₁ < a₂ + b

Tactic:
Nat.lt_add_right _ h

Premises used: Nat.lt_add_right
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ a₁ < a₂ + b

Tactic:
exact Nat.lt_add_right _ h

Premises used: Nat.lt_add_right
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ b ≤ a₁

Tactic:
simp at h₁
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
neg : a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]

Premises used: lt_of_le_of_lt, ite_false, not_lt_of_gt
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
neg : a₁ * a₁ < a₂ * a₂
neg₁ : a₁ + b < a₂ + b
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)

Tactic:
apply add_lt_add

Premises used: Nat.add_lt_add
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂

Tactic:
Nat.mul_self_lt_mul_self h

Premises used: Nat.mul_self_lt_mul_self
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂

Tactic:
exact Nat.mul_self_lt_mul_self h

Premises used: Nat.mul_self_lt_mul_self
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
neg : a₁ < a₂
⊢ a₁ + b < a₂ + b

Tactic:
apply Nat.add_lt_add_right

Premises used: Nat.add_lt_add_right
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
pos : ∀ (h₁ : a < b₁), pair a b₁ < pair a b₂
neg : ∀ (h₁ : ¬a < b₁), pair a b₁ < pair a b₂
⊢ pair a b₁ < pair a b₂

Tactic:
by_cases h₁ : a < b₁
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ pair a b₁ < pair a b₂

Tactic:
simpa [pair, h₁, Nat.add_assoc, lt_trans h₁ h, h] using mul_self_lt_mul_self h

Premises used: lt_trans, Nat.mul_self_lt_mul_self, Nat.pair, Nat.add_assoc
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
neg : a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
⊢ pair a b₁ < pair a b₂

Tactic:
simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]

Premises used: Nat.pair, Nat.add_assoc, reduceIte
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
pos : ∀ (h₂ : a < b₂), a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
neg : ∀ (h₂ : ¬a < b₂), a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
by_cases h₂ : a < b₂
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
simp [h₂, h]
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
pos : a * a + (a + b₁) < b₂ * b₂ + a
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
simp only [h₂, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
pos : b₁ + a * a < b₂ * b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a

Tactic:
rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]

Premises used: Nat.add_lt_add_iff_left, Nat.add_assoc, Nat.add_comm
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
pos : b₁ ≤ a + a
⊢ b₁ + a * a < b₂ * b₂

Tactic:
rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]

Premises used: Nat.sqrt_lt, Nat.sqrt_add_eq, Nat.add_comm
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ b₁ ≤ a + a

Tactic:
le_trans (not_lt.mp h₁) (Nat.le_add_left _ _)

Premises used: Nat.le_add_left, not_lt, Iff.mp, le_trans
-- Module: Mathlib.Data.Nat.Pairing
Goal:
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ b₁ ≤ a + a

Tactic:
exact le_trans (not_lt.mp h₁) (Nat.le_add_left _ _)

Premises used: Nat.le_add_left, not_lt, Iff.mp, le_trans
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
simp : (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))
⊢ pair m n < HPow.hPow (β := ℕ) (max m n + 1) 2

Tactic:
simp only [pair, Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul, Nat.add_assoc]

Premises used: Nat.mul_one, Nat.pow_two, Nat.pair, Nat.add_assoc, Nat.mul_add, Nat.one_mul, Nat.add_mul
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
pos : m < n → n * n + m < max m n * max m n + (max m n + (max m n + 1))
neg : ¬m < n → m * m + (m + n) < max m n * max m n + (max m n + (max m n + 1))
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : m < n
pos : m < n + (n + 1)
⊢ n * n + m < max m n * max m n + (max m n + (max m n + 1))

Tactic:
simp [Nat.le_of_lt, not_lt.1, *]

Premises used: Nat.le_of_lt, not_lt, Iff.mp
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : ¬m < n
neg : n < m + 1
⊢ m * m + (m + n) < max m n * max m n + (max m n + (max m n + 1))

Tactic:
simp [Nat.le_of_lt, not_lt.1, *]

Premises used: Nat.le_of_lt, not_lt, Iff.mp
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : m < n
⊢ m < n + (n + 1)

Tactic:
lia
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : ¬m < n
⊢ n < m + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
inl : ∀ (h : m < n), HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
inr : ∀ (h : n ≤ m), HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
rcases lt_or_ge m n with h | h

Premises used: lt_or_ge
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : m < n
inl : HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ n * n + m
inl₁ : HPow.hPow (β := ℕ) n 2 + min m n ≤ n * n + m
inl₂ : HPow.hPow (β := ℕ) n 2 + m ≤ n * n + m
inl₃ inl₄ : n * n + m ≤ n * n + m
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]

Premises used: LT.lt.le, Nat.pow_two, if_pos, max_eq_right, min_eq_left
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : n ≤ m
inr : n ≤ m + n
⊢ HPow.hPow (β := ℕ) (max m n) 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
rw [if_neg h.not_gt, max_eq_left h, min_eq_right h, Nat.pow_two, Nat.add_assoc,
    Nat.add_le_add_iff_left]

Premises used: Nat.pow_two, max_eq_left, min_eq_right, LE.le.not_gt, Nat.add_le_add_iff_left, Nat.add_assoc, if_neg
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : n ≤ m
⊢ n ≤ m + n

Tactic:
Nat.le_add_left _ _

Premises used: Nat.le_add_left
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : n ≤ m
⊢ n ≤ m + n

Tactic:
exact Nat.le_add_left _ _

Premises used: Nat.le_add_left
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
simp : m + n ≤ if m < n then n * n + m else m * m + (m + n)
⊢ m + n ≤ pair m n

Tactic:
simp only [pair, Nat.add_assoc]

Premises used: Nat.pair, Nat.add_assoc
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
pos : m < n → m + n ≤ n * n + m
neg : ¬m < n → m + n ≤ m * m + (m + n)
⊢ m + n ≤ if m < n then n * n + m else m * m + (m + n)

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : m < n
⊢ n ≤ n * n

Tactic:
have := le_mul_self n
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : m < n
this : n ≤ n * n
⊢ m + n ≤ n * n + m

Tactic:
lia
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : ¬m < n
⊢ m + n ≤ m * m + (m + n)

Tactic:
Nat.le_add_left _ _

Premises used: Nat.le_add_left
-- Module: Mathlib.Data.Nat.Pairing
Goal:
m n : ℕ
h : ¬m < n
⊢ m + n ≤ m * m + (m + n)

Tactic:
exact Nat.le_add_left _ _

Premises used: Nat.le_add_left
-- Module: Mathlib.Data.Nat.Pairing
Goal:
n : ℕ
⊢ (unpair n).1 + (unpair n).2 ≤ n

Tactic:
(add_le_pair _ _).trans_eq (pair_unpair _)

Premises used: LE.le.trans_eq, Nat.pair_unpair, Nat.add_le_pair
-- Module: Mathlib.Data.Nat.Pairing
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → ℕ → α
rw : Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (unpair n).1 (unpair n).2) (⨆ (x : ℕ × ℕ), f x.1 x.2)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (unpair n).1 (unpair n).2) (⨆ (x : ℕ), f (unpair x).1 (unpair x).2)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (unpair n).1 (unpair n).2) (⨆ (i : ℕ), ⨆ (j : ℕ), f i j)

Tactic:
rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]

Premises used: Function.Surjective.iSup_comp, Nat.surjective_unpair, iSup_prod
-- Module: Mathlib.Data.Nat.Pairing
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → ℕ → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (n : ℕ), f (unpair n).1 (unpair n).2) (⨅ (i : ℕ), ⨅ (j : ℕ), f i j)

Tactic:
iSup_unpair (show ℕ → ℕ → αᵒᵈ from f)

Premises used: iInf, iSup_unpair, OrderDual
-- Module: Mathlib.Data.Nat.Pairing
Goal:
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
rw : Eq (α := Set (α × β)) (⋃ (n : ℕ), s (unpair n).1 ×ˢ t (unpair n).2) (⋃ (x : ℕ × ℕ), s x.1 ×ˢ t x.2)
⊢ ⋃ (n : ℕ), s (unpair n).1 ×ˢ t (unpair n).2 = SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), s n) (⋃ (n : ℕ), t n)

Tactic:
rw [← Set.iUnion_prod]

Premises used: Set.iUnion_prod
-- Module: Mathlib.Data.Nat.Pairing
Goal:
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ Eq (α := Set (α × β)) (⋃ (n : ℕ), s (unpair n).1 ×ˢ t (unpair n).2) (⋃ (x : ℕ × ℕ), s x.1 ×ˢ t x.2)

Tactic:
surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)

Premises used: SProd.sprod, Prod.fst, Nat.surjective_unpair, Function.Surjective.iUnion_comp, Prod.snd
-- Module: Mathlib.Data.Nat.Pairing
Goal:
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ Eq (α := Set (α × β)) (⋃ (n : ℕ), s (unpair n).1 ×ˢ t (unpair n).2) (⋃ (x : ℕ × ℕ), s x.1 ×ˢ t x.2)

Tactic:
exact surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)

Premises used: SProd.sprod, Prod.fst, Nat.surjective_unpair, Function.Surjective.iUnion_comp, Prod.snd
-- Module: Mathlib.Data.Nat.Pairing
Goal:
α : Type u_1
f : ℕ → ℕ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), f (unpair n).1 (unpair n).2) (⋃ (i : ℕ), ⋃ (j : ℕ), f i j)

Tactic:
iSup_unpair f

Premises used: iSup_unpair, Set.iUnion
-- Module: Mathlib.Data.Nat.Pairing
Goal:
α : Type u_1
f : ℕ → ℕ → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), f (unpair n).1 (unpair n).2) (⋂ (i : ℕ), ⋂ (j : ℕ), f i j)

Tactic:
iInf_unpair f

Premises used: iInf_unpair, Set.iInter
-- Module: Mathlib.Data.Nat.Periodic
Goal:
a : ℕ
⊢ Periodic a.gcd a

Tactic:
a.gcd_add_self_right

Premises used: Nat.gcd_add_self_right, Function.Periodic
-- Module: Mathlib.Data.Nat.Periodic
Goal:
a : ℕ
⊢ Periodic a.Coprime a

Tactic:
fun _ ↦ eq_iff_iff.mpr coprime_add_self_right

Premises used: Iff.mpr, Nat.coprime_add_self_right, Function.Periodic, eq_iff_iff
-- Module: Mathlib.Data.Nat.Periodic
Goal:
a : ℕ
⊢ Periodic (β := ℕ) (fun (n : ℕ) ↦ n % a) a

Tactic:
(add_mod_right · a)

Premises used: Nat.add_mod_right, Function.Periodic
-- Module: Mathlib.Data.Nat.Periodic
Goal:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
rw : f (n % a)
| f n

Tactic:
rw [← n.mod_add_div a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

Premises used: Function.Periodic.nsmul, Nat.nsmul_eq_mul, Nat.mod_add_div, mul_comm
-- Module: Mathlib.Data.Nat.Periodic
Goal:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
conv_rhs : f (n % a) = f n
conv_rhs₁ : f (n % a) = f (n % a)
⊢ f (n % a) = f n

Tactic:
conv_rhs => rw [← n.mod_add_div a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

Premises used: Function.Periodic.nsmul, Nat.nsmul_eq_mul, Nat.mod_add_div, mul_comm
-- Module: Mathlib.Data.Nat.Periodic
Goal:
n a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
rw :
  Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a) (Ico n (n + a)))
⊢ (filter p (Ico n (n + a))).card = count p a

Tactic:
rw [count_eq_card_filter_range, Finset.card, Finset.filter_val, Finset.range_val, ←
    multiset_Ico_map_mod n, ← map_count_True_eq_filter_card, ← map_count_True_eq_filter_card,
    map_map]

Premises used: Finset.range_val, Nat.count_eq_card_filter_range, Multiset.map_count_True_eq_filter_card, Finset.filter_val, Finset.card, Multiset.map_map, Nat.multiset_Ico_map_mod
-- Module: Mathlib.Data.Nat.Periodic
Goal:
n a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
e_a : p = (fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a) (Ico n (n + a)))

Tactic:
congr
-- Module: Mathlib.Data.Nat.Periodic
Goal:
n a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
e_a : ∀ (n : ℕ), p n = ((fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a) n
⊢ p = (fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a

Tactic:
funext n
-- Module: Mathlib.Data.Nat.Periodic
Goal:
n_1 a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
n : ℕ
⊢ p n = ((fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a) n

Tactic:
(pp.map_mod_nat n).symm

Premises used: Function.Periodic.map_mod_nat, Eq.symm
-- Module: Mathlib.Data.Nat.Periodic
Goal:
n_1 a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
n : ℕ
⊢ p n = ((fun (x : ℕ) ↦ p x) ∘ fun (x : ℕ) ↦ x % a) n

Tactic:
exact (pp.map_mod_nat n).symm

Premises used: Function.Periodic.map_mod_nat, Eq.symm
-- Module: Mathlib.Data.Nat.Periodic
Goal:
n a : ℕ
p : ℕ → Prop
inst : DecidablePred p
pp : Periodic p a
⊢ #(filter p (Ico n (n + a))) = count p a

Tactic:
n.filter_multiset_Ico_card_eq_of_periodic a p pp

Premises used: Multiset.ofList, Finset.card, Nat.filter_multiset_Ico_card_eq_of_periodic, Multiset.filter