awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
⊢ LE.le.{u_2} (α := S) 0 1

Tactic:
simp only [← le, zero, one, zero_le_one]

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
rw : f a * f b ≤ f a * f c
⊢ a * b ≤ a * c

Tactic:
rw [← le, mul, mul]
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f a * f b ≤ f a * f c

Tactic:
mul_le_mul_of_nonneg_left (le.2 hbc) ?_

Premises used: Iff.mpr, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
refine : 0 ≤ f a
⊢ f a * f b ≤ f a * f c

Tactic:
refine mul_le_mul_of_nonneg_left (le.2 hbc) ?_

Premises used: Iff.mpr, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
rwa : f 0 ≤ f a
rwa₁ rwa₂ rwa₃ rwa₄ : 0 ≤ a
⊢ 0 ≤ f a

Tactic:
rwa [← zero, le]
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
rw : f b * f a ≤ f c * f a
⊢ b * a ≤ c * a

Tactic:
rw [← le, mul, mul]
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f b * f a ≤ f c * f a

Tactic:
mul_le_mul_of_nonneg_right (le.2 hbc) ?_

Premises used: Iff.mpr, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
refine : 0 ≤ f a
⊢ f b * f a ≤ f c * f a

Tactic:
refine mul_le_mul_of_nonneg_right (le.2 hbc) ?_

Premises used: Iff.mpr, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
rw : f a * f b < f a * f c
⊢ a * b < a * c

Tactic:
rw [← lt, mul, mul]
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ f a * f b < f a * f c

Tactic:
mul_lt_mul_of_pos_left (lt.2 hbc) ?_

Premises used: Iff.mpr, mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
refine : 0 < f a
⊢ f a * f b < f a * f c

Tactic:
refine mul_lt_mul_of_pos_left (lt.2 hbc) ?_

Premises used: Iff.mpr, mul_lt_mul_of_pos_left
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
rwa : f 0 < f a
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < a
⊢ 0 < f a

Tactic:
rwa [← zero, lt]
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
rw : f b * f a < f c * f a
⊢ b * a < c * a

Tactic:
rw [← lt, mul, mul]
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ f b * f a < f c * f a

Tactic:
mul_lt_mul_of_pos_right (lt.2 hbc) ?_

Premises used: Iff.mpr, mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.Ring.InjSurj
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Semiring S
inst_4 : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
refine : 0 < f a
⊢ f b * f a < f c * f a

Tactic:
refine mul_lt_mul_of_pos_right (lt.2 hbc) ?_

Premises used: Iff.mpr, mul_lt_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
⊢ IsStrictOrderedRing ℤ

Tactic:
.of_mul_pos @Int.mul_pos

Premises used: Int.mul_pos, IsStrictOrderedRing.of_mul_pos
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
⊢ IsCompl (α := Set ℤ) {n : ℤ | Even n} {n : ℤ | Odd n}

Tactic:
simp [← not_even_iff_odd, ← Set.compl_setOf, isCompl_compl]

Premises used: Int.not_even_iff_odd, isCompl_compl, Set.compl_setOf
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ℤ
rw : Eq.{u_1 + 1} (α := α) (↑n.natAbs : α) (↑(↑n.natAbs : ℤ) : α)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (↑n.natAbs : α) (↑n.natAbs : α)
⊢ Eq.{u_1 + 1} (α := α) (↑n.natAbs : α) (↑|n| : α)

Tactic:
rw [← natCast_natAbs, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.natCast_natAbs
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
m : ℤ
even : Even m
⊢ LT.lt (α := ℤ) 0 2

Tactic:
decide
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
m n : ℤ
even : Even (n - m)
⊢ m + 2 ≤ n ↔ m < n

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
p q n : ℕ
dvd : p.gcd q ∣ n
le : p.pred * q.pred ≤ n
zero : ∀ (dvd : gcd 0 q ∣ n) (le : pred 0 * q.pred ≤ n), ∃ (a : ℕ), ∃ (b : ℕ), a * 0 + b * q = n
succ :
  ∀ (p : ℕ) (dvd : (p + 1).gcd q ∣ n) (le : (p + 1).pred * q.pred ≤ n), ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * q = n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * p + b * q = n

Tactic:
obtain _ | p := p
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
zero : ∀ (b : ℕ) (eq : n = q * b), ∃ (a : ℕ), ∃ (b : ℕ), a * 0 + b * q = n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * 0 + b * q = n

Tactic:
have ⟨b, eq⟩ := q.gcd_zero_left ▸ dvd
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
b : ℕ
eq : n = q * b
⊢ HMul.hMul (α := ℕ) 0 0 + b * q = n

Tactic:
simpa [mul_comm, eq_comm] using eq

Premises used: eq_comm, mul_comm
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
b : ℕ
eq : n = q * b
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * 0 + b * q = n

Tactic:
exact ⟨0, b, by simpa [mul_comm, eq_comm] using eq⟩
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
q n p : ℕ
dvd : (p + 1).gcd q ∣ n
le : (p + 1).pred * q.pred ≤ n
succ : ∀ (dvd : (p + 1).gcd 0 ∣ n) (le : (p + 1).pred * pred 0 ≤ n), ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * 0 = n
succ₁ :
  ∀ (q : ℕ) (dvd : (p + 1).gcd (q + 1) ∣ n) (le : (p + 1).pred * (q + 1).pred ≤ n),
    ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * (q + 1) = n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * q = n

Tactic:
obtain _ | q := q
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
succ : ∀ (a : ℕ) (eq : n = (p.gcd 0 + 1).gcd 0 * a), ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * 0 = n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * 0 = n

Tactic:
have ⟨a, eq⟩ := p.gcd_zero_right ▸ dvd
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
a : ℕ
eq : n = (p.gcd 0 + 1).gcd 0 * a
⊢ a * (p + 1) + HMul.hMul (α := ℕ) 0 0 = n

Tactic:
simpa [mul_comm, eq_comm] using eq

Premises used: eq_comm, mul_comm
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
a : ℕ
eq : n = (p.gcd 0 + 1).gcd 0 * a
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * 0 = n

Tactic:
exact ⟨a, 0, by simpa [mul_comm, eq_comm] using eq⟩
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : (p + 1).gcd (q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y

Tactic:
rw [← Int.gcd_natCast_natCast, Int.gcd_dvd_iff] at dvd

Premises used: Int.gcd_dvd_iff, Int.gcd_natCast_natCast
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : (p + 1).gcd (q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
dvd₁ : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
⊢ (p + 1).pred * (q + 1).pred ≤ n

Tactic:
rw [← Int.gcd_natCast_natCast, Int.gcd_dvd_iff] at dvd

Premises used: Int.gcd_dvd_iff, Int.gcd_natCast_natCast
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
succ :
  ∀ (a_n b_n : ℤ) (eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n),
    ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * (q + 1) = n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * (q + 1) = n

Tactic:
have ⟨a_n, b_n, eq⟩ := dvd
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * (q + 1) = n

Tactic:
⟨a.toNat, b.toNat, Nat.cast_injective (R := ℤ) ?_⟩

Premises used: Exists.intro, Int.toNat, Nat.cast_injective
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
succ : Eq (α := ℤ) (↑(a.toNat * (p + 1) + b.toNat * (q + 1)) : ℤ) (↑n : ℤ)
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * (q + 1) = n

Tactic:
refine ⟨a.toNat, b.toNat, Nat.cast_injective (R := ℤ) ?_⟩
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
rw : a * (↑p.succ : ℤ) + (b_n * (↑q.succ : ℤ) + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ) * (↑q.succ : ℤ)) = (↑n : ℤ)
rw₁ : a * (↑p.succ : ℤ) + b_n * (↑q.succ : ℤ) + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ) * (↑q.succ : ℤ) = (↑n : ℤ)
rw₂ : a * (↑p.succ : ℤ) + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ) * (↑q.succ : ℤ) + b_n * (↑q.succ : ℤ) = (↑n : ℤ)
rw₃ : a * (↑p.succ : ℤ) + a_n / (↑q.succ : ℤ) * (↑q.succ : ℤ) * (↑p.succ : ℤ) + b_n * (↑q.succ : ℤ) = (↑n : ℤ)
rw₄ : (a + a_n / (↑q.succ : ℤ) * (↑q.succ : ℤ)) * (↑p.succ : ℤ) + b_n * (↑q.succ : ℤ) = (↑n : ℤ)
rw₅ : a_n * (↑p.succ : ℤ) + b_n * (↑q.succ : ℤ) = (↑n : ℤ)
rw₆ : a_n * (↑p.succ : ℤ) + b_n * (↑q.succ : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
rw₇ : (↑p.succ : ℤ) * a_n + b_n * (↑q.succ : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
rw₈ rw₉ : (↑p.succ : ℤ) * a_n + (↑q.succ : ℤ) * b_n = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)

Tactic:
rw [add_mul, ← add_assoc,
    add_right_comm, mul_right_comm, ← add_mul, Int.emod_add_ediv_mul, eq, mul_comm, mul_comm b_n]

Premises used: add_mul, add_assoc, Int.emod_add_ediv_mul, add_right_comm, mul_right_comm, mul_comm
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)

Tactic:
have : a * p.succ + b * q.succ = n := by rw [add_mul, ← add_assoc,
    add_right_comm, mul_right_comm, ← add_mul, Int.emod_add_ediv_mul, eq, mul_comm, mul_comm b_n]
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
⊢ Ne (α := ℤ) (↑q.succ : ℤ) 0

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
succ : 0 ≤ b
⊢ Eq (α := ℤ) (↑(a.toNat * (p + 1) + b.toNat * (q + 1)) : ℤ) (↑n : ℤ)

Tactic:
rw [Nat.cast_add, Nat.cast_mul, Nat.cast_mul, Int.natCast_toNat_eq_self.mpr
    (Int.emod_nonneg _ <| by lia), Int.natCast_toNat_eq_self.mpr, this]

Premises used: Iff.mpr, Int.natCast_toNat_eq_self, Nat.cast_add, Nat.cast_mul, Int.emod_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
succ : ∀ (hb : ¬0 ≤ b), False
⊢ 0 ≤ b

Tactic:
by_contra hb
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : ¬0 ≤ b
⊢ b ≤ -1

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : ¬0 ≤ b
⊢ b ≤ -1

Tactic:
replace hb : b ≤ -1 := by lia
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
succ : LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
⊢ False

Tactic:
apply lt_irrefl (n : ℤ)

Premises used: lt_irrefl, Nat.cast
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
⊢ Ne (α := ℤ) (↑q.succ : ℤ) 0

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
⊢ a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)

Tactic:
have ha := Int.emod_lt a_n (by lia : (q.succ : ℤ) ≠ 0)
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
succ :
  ∀ (le : p * q ≤ n) (a_n b_n : ℤ) (eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n),
    let a := a_n % (↑q.succ : ℤ);
    let b := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ);
    ∀ (this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)) (hb : b ≤ -1)
      (ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)), LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)
⊢ LT.lt (α := ℤ) (↑n : ℤ) (↑n : ℤ)

Tactic:
rw [p.pred_succ, q.pred_succ] at le

Premises used: Nat.pred_succ
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ (↑n : ℤ) = a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ)

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
h₁ : LE.le (α := ℤ) 0 (↑p.succ : ℤ)
h₂ : a ≤ (↑q : ℤ)
h₃ : LE.le (α := ℤ) 0 (↑q.succ : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) ≤
    HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ LE.le (α := ℤ) 0 (↑p.succ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ a ≤ (↑q : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ LE.le (α := ℤ) 0 (↑q.succ : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
simp_rw :
  HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) + HMul.hMul (α := ℤ) (↑q : ℤ) 1 +
      (HMul.hMul (α := ℤ) (↑q : ℤ) (-1) + HMul.hMul (α := ℤ) 1 (-1)) =
    HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1
⊢ HMul.hMul (α := ℤ) (↑q : ℤ) (↑p.succ : ℤ) + HMul.hMul (α := ℤ) (-1) (↑q.succ : ℤ) =
    HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1

Tactic:
simp_rw [Nat.cast_succ, mul_add, mul_comm]

Premises used: Nat.cast_succ, mul_comm, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Int
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n
a : ℤ := a_n % (↑q.succ : ℤ)
b : ℤ := b_n + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ)
this : a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
hb : b ≤ -1
ha : a_n % (↑q.succ : ℤ) < (↑(Int.natAbs (↑q.succ : ℤ)) : ℤ)
⊢ HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) + HMul.hMul (α := ℤ) (↑q : ℤ) 1 +
      (HMul.hMul (α := ℤ) (↑q : ℤ) (-1) + HMul.hMul (α := ℤ) 1 (-1)) =
    HMul.hMul (α := ℤ) (↑p : ℤ) (↑q : ℤ) - 1

Tactic:
lia