awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : { a : R // IsIdempotentElem a }
simp_rw simp_rw₁ :
  1 - (↑a : R) * (1 - (↑b : R)) = (↑(b ⊔ Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) ⋯) : R)
simp_rw₂ :
  1 - (↑a : R) * (1 - (↑b : R)) =
    (↑(SemilatticeSup.sup b (Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) ⋯)) : R)
simp_rw₃ : 1 - (↑a : R) * (1 - (↑b : R)) = (↑b : R) + (1 - (↑a : R)) - (↑b : R) * (1 - (↑a : R))
simp_rw₄ : 1 - (↑a : R) * (1 - (↑b : R)) = 1 - (↑a : R) + (↑b : R) - (↑b : R) * (1 - (↑a : R))
simp_rw₅ : 1 - (↑a : R) * (1 - (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - (↑b : R) * (1 - (↑a : R)))
simp_rw₆ : 1 - ((↑a : R) * 1 - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - ((↑b : R) * 1 - (↑b : R) * (↑a : R)))
simp_rw₇ : 1 - ((↑a : R) - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + ((↑b : R) - ((↑b : R) - (↑b : R) * (↑a : R)))
simp_rw₈ : 1 - ((↑a : R) - (↑a : R) * (↑b : R)) = 1 - (↑a : R) + (↑b : R) * (↑a : R)
⊢ (↑(Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R) * (1 - (↑b : R))) ⋯) : R) =
    (↑(b ⊔ Subtype.mk (p := fun (a : R) ↦ IsIdempotentElem a) (1 - (↑a : R)) ⋯) : R)
have simp_rw₉ : 1 - ((↑a : R) - (↑a : R) * (↑b : R)) = 1 - ((↑a : R) - (↑b : R) * (↑a : R))
Tactic: simp_rw [(· ⊔ ·), SemilatticeSup.sup,
    add_comm b.1, add_sub_assoc, mul_sub, mul_one, sub_sub_cancel, sub_add, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
⊢ ((↑a : R), 1 - (↑a : R)).1 * ((↑a : R), 1 - (↑a : R)).2 = 0
have simp_rw : (↑a : R) * (1 - (↑a : R)) = 0
Tactic: simp_rw [mul_sub, mul_one, a.2.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
simp_rw simp_rw₁ : (↑a : R) * (1 - (↑a : R)) = 0
⊢ ((↑a : R), 1 - (↑a : R)).1 * ((↑a : R), 1 - (↑a : R)).2 = 0
have simp_rw₂ : (↑a : R) * 1 - (↑a : R) * (↑a : R) = 0
Tactic: simp_rw [mul_sub, mul_one, a.2.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
simp_rw simp_rw₁ : (↑a : R) * (1 - (↑a : R)) = 0
simp_rw₂ : (↑a : R) * 1 - (↑a : R) * (↑a : R) = 0
⊢ ((↑a : R), 1 - (↑a : R)).1 * ((↑a : R), 1 - (↑a : R)).2 = 0
have simp_rw₃ : (↑a : R) - (↑a : R) * (↑a : R) = 0
Tactic: simp_rw [mul_sub, mul_one, a.2.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
simp_rw simp_rw₁ : (↑a : R) * (1 - (↑a : R)) = 0
simp_rw₂ : (↑a : R) * 1 - (↑a : R) * (↑a : R) = 0
simp_rw₃ : (↑a : R) - (↑a : R) * (↑a : R) = 0
⊢ ((↑a : R), 1 - (↑a : R)).1 * ((↑a : R), 1 - (↑a : R)).2 = 0
have simp_rw₄ : (↑a : R) - (↑a : R) = 0
Tactic: simp_rw [mul_sub, mul_one, a.2.eq, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Idempotent (goal)
Goal:
R : Type u_1
inst : CommRing R
a : { a : R // IsIdempotentElem a }
⊢ ((↑a : R), 1 - (↑a : R)).1 + ((↑a : R), 1 - (↑a : R)).2 = 1
have rw : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
⊢ a * b ≤ a * c
have rw : f a * f b ≤ f a * f c
Tactic: rw [← le, mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
have refine : 0 ≤ f a
Tactic: refine mul_le_mul_of_nonneg_left (le.2 hbc) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
⊢ 0 ≤ f a
have rwa : f 0 ≤ f a
Tactic: rwa [← zero, le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
⊢ b * a ≤ c * a
have rw : f b * f a ≤ f c * f a
Tactic: rw [← le, mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
have refine : 0 ≤ f a
Tactic: refine mul_le_mul_of_nonneg_right (le.2 hbc) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
⊢ a * b < a * c
have rw : f a * f b < f a * f c
Tactic: rw [← lt, mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
have refine : 0 < f a
Tactic: refine mul_lt_mul_of_pos_left (lt.2 hbc) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
⊢ 0 < f a
have rwa : f 0 < f a
Tactic: rwa [← zero, lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
⊢ b * a < c * a
have rw : f b * f a < f c * f a
Tactic: rw [← lt, mul, mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.InjSurj (goal)
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
have refine : 0 < f a
Tactic: refine mul_lt_mul_of_pos_right (lt.2 hbc) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ℤ
⊢ Eq.{u_1 + 1} (α := α) (↑n.natAbs : α) (↑|n| : α)
have rw : Eq.{u_1 + 1} (α := α) (↑n.natAbs : α) (↑(↑n.natAbs : ℤ) : α)
Tactic: rw [← natCast_natAbs, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ℤ
rw : Eq.{u_1 + 1} (α := α) (↑n.natAbs : α) (↑(↑n.natAbs : ℤ) : α)
⊢ Eq.{u_1 + 1} (α := α) (↑n.natAbs : α) (↑|n| : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑n.natAbs : α) (↑n.natAbs : α)
Tactic: rw [← natCast_natAbs, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
p q n : ℕ
dvd : p.gcd q ∣ n
le : p.pred * q.pred ≤ n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * p + b * q = n
have zero : ∀ (dvd : gcd 0 q ∣ n) (le : pred 0 * q.pred ≤ n), ∃ (a : ℕ), ∃ (b : ℕ), a * 0 + b * q = n
Tactic: obtain _ | p := p
Cleared hypotheses: p, dvd, le
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * p + b * q = n
have succ : ∀ (p : ℕ) (dvd : (p + 1).gcd q ∣ n) (le : (p + 1).pred * q.pred ≤ n), ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * q = n
Tactic: obtain _ | p := p
Cleared hypotheses: p, dvd, le
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * 0 + b * q = n
have zero : ∀ (b : ℕ) (eq : n = q * b), ∃ (a : ℕ), ∃ (b : ℕ), a * 0 + b * q = n
Tactic: have ⟨b, eq⟩ := q.gcd_zero_left ▸ dvd
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
q n p : ℕ
dvd : (p + 1).gcd q ∣ n
le : (p + 1).pred * q.pred ≤ n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * q = n
have succ : ∀ (dvd : (p + 1).gcd 0 ∣ n) (le : (p + 1).pred * pred 0 ≤ n), ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * 0 = n
Tactic: obtain _ | q := q
Cleared hypotheses: q, dvd, le
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * q = n
have 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
Tactic: obtain _ | q := q
Cleared hypotheses: q, dvd, le
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * 0 = n
have succ : ∀ (a : ℕ) (eq : n = (p.gcd 0 + 1).gcd 0 * a), ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * 0 = n
Tactic: have ⟨a, eq⟩ := p.gcd_zero_right ▸ dvd
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (hypothesis)
Goal:
n p 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
have dvd₁ : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
Tactic: rw [← Int.gcd_natCast_natCast, Int.gcd_dvd_iff] at dvd
Cleared hypotheses: dvd, le
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
Goal:
n p q : ℕ
dvd : ∃ (x : ℤ), ∃ (y : ℤ), (↑n : ℤ) = (↑(p + 1) : ℤ) * x + (↑(q + 1) : ℤ) * y
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * (q + 1) = n
have succ : ∀ (a_n b_n : ℤ) (eq : (↑n : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_n),
  ∃ (a : ℕ), ∃ (b : ℕ), a * (p + 1) + b * (q + 1) = n
Tactic: have ⟨a_n, b_n, eq⟩ := dvd
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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
have succ : Eq (α := ℤ) (↑(a.toNat * (p + 1) + b.toNat * (q + 1)) : ℤ) (↑n : ℤ)
Tactic: refine ⟨a.toNat, b.toNat, Nat.cast_injective (R := ℤ) ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
have rw : a * (↑p.succ : ℤ) + (b_n * (↑q.succ : ℤ) + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ) * (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
have rw₁ : a * (↑p.succ : ℤ) + b_n * (↑q.succ : ℤ) + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ) * (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
have rw₂ : a * (↑p.succ : ℤ) + a_n / (↑q.succ : ℤ) * (↑p.succ : ℤ) * (↑q.succ : ℤ) + b_n * (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
have rw₃ : a * (↑p.succ : ℤ) + a_n / (↑q.succ : ℤ) * (↑q.succ : ℤ) * (↑p.succ : ℤ) + b_n * (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
have rw₄ : (a + a_n / (↑q.succ : ℤ) * (↑q.succ : ℤ)) * (↑p.succ : ℤ) + b_n * (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
have rw₅ : a_n * (↑p.succ : ℤ) + b_n * (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
have rw₆ : a_n * (↑p.succ : ℤ) + b_n * (↑q.succ : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
have rw₇ : (↑p.succ : ℤ) * a_n + b_n * (↑q.succ : ℤ) = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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
⊢ a * (↑p.succ : ℤ) + b * (↑q.succ : ℤ) = (↑n : ℤ)
have rw₈ : (↑p.succ : ℤ) * a_n + (↑q.succ : ℤ) * b_n = (↑(p + 1) : ℤ) * a_n + (↑(q + 1) : ℤ) * b_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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (hypothesis)
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 : ℤ)
⊢ Eq (α := ℤ) (↑(a.toNat * (p + 1) + b.toNat * (q + 1)) : ℤ) (↑n : ℤ)
have this : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
⊢ Eq (α := ℤ) (↑(a.toNat * (p + 1) + b.toNat * (q + 1)) : ℤ) (↑n : ℤ)
have succ : 0 ≤ b
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (goal)
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 : ℤ)
⊢ 0 ≤ b
have succ : ∀ (hb : ¬0 ≤ b), False
Tactic: by_contra hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.Int (hypothesis)
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
⊢ False
have hb₁ : b ≤ -1
Tactic: replace hb : b ≤ -1 := by lia
Cleared hypotheses: hb