awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
⊢ (↑m : ℕ).Coprime (↑k : ℕ) → n.Coprime k → (m * n).Coprime k
have rw : (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → (m * n).Coprime k
Tactic: rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
⊢ (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → (m * n).Coprime k
have rw : (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → (↑(m * n) : ℕ).Coprime (↑k : ℕ)
Tactic: rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
⊢ m.Coprime k → n.Coprime k → (m * n).Coprime k
have repeat : (↑m : ℕ).Coprime (↑k : ℕ) → (↑n : ℕ).Coprime (↑k : ℕ) → (↑(m * n) : ℕ).Coprime (↑k : ℕ)
Tactic: repeat rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
⊢ k.Coprime m → k.Coprime n → k.Coprime (m * n)
have rw : (↑k : ℕ).Coprime (↑m : ℕ) → k.Coprime n → k.Coprime (m * n)
Tactic: rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
⊢ (↑k : ℕ).Coprime (↑m : ℕ) → k.Coprime n → k.Coprime (m * n)
have rw : (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → k.Coprime (m * n)
Tactic: rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
⊢ (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → k.Coprime (m * n)
have rw : (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑k : ℕ).Coprime (↑(m * n) : ℕ)
Tactic: rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
⊢ k.Coprime m → k.Coprime n → k.Coprime (m * n)
have repeat : (↑k : ℕ).Coprime (↑m : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑k : ℕ).Coprime (↑(m * n) : ℕ)
Tactic: repeat rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n : ℕ+
⊢ m.gcd n = n.gcd m
have a : (↑(m.gcd n) : ℕ) = (↑(n.gcd m) : ℕ)
Tactic: apply eq
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n : ℕ+
⊢ m.gcd n = m ↔ m ∣ n
have rw : (↑(m.gcd n) : ℕ) = (↑m : ℕ) ↔ (↑m : ℕ).gcd (↑n : ℕ) = (↑m : ℕ)
Tactic: rw [dvd_iff, ← Nat.gcd_eq_left_iff_dvd, ← coe_inj]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n : ℕ+
⊢ n.gcd m = m ↔ m ∣ n
have rw : m.gcd n = m ↔ m ∣ n
Tactic: rw [gcd_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
h : k.Coprime n
⊢ (k * m).gcd n = m.gcd n
have a : (↑((k * m).gcd n) : ℕ) = (↑(m.gcd n) : ℕ)
Tactic: apply eq
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
h : k.Coprime n
⊢ ((↑k : ℕ) * (↑m : ℕ)).gcd (↑n : ℕ) = (↑m : ℕ).gcd (↑n : ℕ)
have a : (↑k : ℕ).Coprime (↑n : ℕ)
Tactic: apply Nat.Coprime.gcd_mul_left_cancel
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
⊢ k.Coprime n → (m * k).gcd n = m.gcd n
have rw : k.Coprime n → (k * m).gcd n = m.gcd n
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
h : k.Coprime m
⊢ m.gcd (k * n) = m.gcd n
have rw : (k * n).gcd m = m.gcd n
Tactic: rw [gcd_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
h : k.Coprime m
⊢ (k * n).gcd m = m.gcd n
have symm : m.gcd n = (k * n).gcd m
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
h : k.Coprime m
⊢ m.gcd n = (k * n).gcd m
have rw : n.gcd m = (k * n).gcd m
Tactic: rw [gcd_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
h : k.Coprime m
⊢ n.gcd m = (k * n).gcd m
have symm : (k * n).gcd m = n.gcd m
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
h : k.Coprime m
⊢ m.gcd (k * n) = m.gcd n
have iterate : (k * n).gcd m = n.gcd m
Tactic: iterate 2 rw [gcd_comm]; symm
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n k : ℕ+
⊢ k.Coprime m → m.gcd (n * k) = m.gcd n
have rw : k.Coprime m → m.gcd (k * n) = m.gcd n
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
n : ℕ+
⊢ gcd 1 n = 1
have rw : 1 ∣ n
Tactic: rw [gcd_eq_left_iff_dvd]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
n : ℕ+
⊢ n.gcd 1 = 1
have rw : gcd 1 n = 1
Tactic: rw [gcd_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m n : ℕ+
⊢ m.gcd n = 1 → n.gcd m = 1
have rw : n.gcd m = 1 → n.gcd m = 1
Tactic: rw [gcd_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m k n : ℕ+
⊢ m ∣ k → k.Coprime n → m.Coprime n
have rw : (↑m : ℕ) ∣ (↑k : ℕ) → k.Coprime n → m.Coprime n
Tactic: rw [dvd_iff]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m k n : ℕ+
⊢ (↑m : ℕ) ∣ (↑k : ℕ) → k.Coprime n → m.Coprime n
have rw : (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → m.Coprime n
Tactic: rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m k n : ℕ+
⊢ (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → m.Coprime n
have rw : (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑m : ℕ).Coprime (↑n : ℕ)
Tactic: rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
m k n : ℕ+
⊢ (↑m : ℕ) ∣ (↑k : ℕ) → k.Coprime n → m.Coprime n
have repeat : (↑m : ℕ) ∣ (↑k : ℕ) → (↑k : ℕ).Coprime (↑n : ℕ) → (↑m : ℕ).Coprime (↑n : ℕ)
Tactic: repeat rw [← coprime_coe]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (hypothesis)
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m
have am₁ : a.gcd m = a
Tactic: rw [← gcd_eq_left_iff_dvd] at am
Cleared hypotheses: am, bn
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
| a
have rw : a.gcd m
Tactic: rw [← am]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a = (a * b).gcd m
have conv_lhs : a.gcd m = (a * b).gcd m
Tactic: conv_lhs => rw [← am]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ a.gcd m = (a * b).gcd m
have rw : (a * b).gcd m = a.gcd m
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a.gcd m = a
bn : b ∣ n
⊢ (a * b).gcd m = a.gcd m
have apply : b.Coprime m
Tactic: apply Coprime.gcd_mul_right_cancel a
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m
have rw : a = (a * b).gcd m
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = m.gcd (a * b)
have rw : a = (a * b).gcd m
Tactic: rw [gcd_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = m.gcd (b * a)
have rw : a = (b * a).gcd m
Tactic: rw [gcd_comm]
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (hypothesis)
Goal:
k m n : ℕ+
h : m.Coprime n
⊢ k.gcd (m * n) = k.gcd m * k.gcd n
have h₁ : (↑m : ℕ).Coprime (↑n : ℕ)
Tactic: rw [← coprime_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (goal)
Goal:
k m n : ℕ+
h : (↑m : ℕ).Coprime (↑n : ℕ)
⊢ k.gcd (m * n) = k.gcd m * k.gcd n
have a : (↑(k.gcd (m * n)) : ℕ) = (↑(k.gcd m * k.gcd n) : ℕ)
Tactic: apply eq
-- Lean 4 proof step from Mathlib.Data.PNat.Prime (hypothesis)
Goal:
m n : ℕ+
k l : ℕ
h : m.Coprime n
⊢ ((↑m : ℕ) ^ k).Coprime ((↑n : ℕ) ^ l)
have h₁ : (↑m : ℕ).Coprime (↑n : ℕ)
Tactic: rw [← coprime_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
⊢ u.v = succ₂ u.vp
have fst : u.v.1 = (succ₂ u.vp).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
fst : u.v.1 = (succ₂ u.vp).1
⊢ u.v = succ₂ u.vp
have snd : u.v.2 = (succ₂ u.vp).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
⊢ u.wp + u.zp + u.wp * u.zp = u.x * u.y ↔ u.w * u.z = (u.x * u.y).succPNat
have let : ∀ (wp x y zp ap bp : ℕ),
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y ↔
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
Tactic: let ⟨wp, x, y, zp, ap, bp⟩ := u
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y ↔
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
have mp : { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y →
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
mp :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y →
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y ↔
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
have mpr : { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat →
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
have mp : Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (wp + 1) sorry * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (zp + 1) sorry =
  Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (x * y + 1) sorry
Tactic: simp only [w, succPNat, succ_eq_add_one, z] at *
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y).succPNat
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp : XgcdType }.y
have mpr : wp + zp + wp * zp = x * y
Tactic: simp only [w, succPNat, succ_eq_add_one, z] at *
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (wp + 1) ⋯ * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (zp + 1) ⋯ =
    Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (x * y + 1) ⋯
have mp : (wp + 1) * (zp + 1) = x * y + 1
Tactic: simp only [← coe_inj, mul_coe, mk_coe] at *
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h :
  Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (wp + 1) ⋯ * Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (zp + 1) ⋯ =
    Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (x * y + 1) ⋯
⊢ wp + zp + wp * zp = x * y
have h₁ : (wp + 1) * (zp + 1) = x * y + 1
Tactic: simp only [← coe_inj, mul_coe, mk_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h : wp + zp + wp * zp = x * y
⊢ (wp + 1) * (zp + 1) = x * y + 1
have mp : (wp + 1) * (zp + 1) = wp + zp + wp * zp + 1
Tactic: simp_all [← h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h : (wp + 1) * (zp + 1) = x * y + 1
⊢ wp + zp + wp * zp = x * y
have h₁ : wp * zp + zp + wp = x * y
Tactic: simp only [Nat.mul_add, Nat.add_mul, one_mul, mul_one, ← Nat.add_assoc,
      Nat.add_right_cancel_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y
have mpr : wp + zp + wp * zp = wp * zp + zp + wp
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
⊢ u.flip.IsReduced ↔ u.IsReduced
have dsimp : u.bp = u.ap ↔ u.ap = u.bp
Tactic: dsimp [IsReduced, flip]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
⊢ u.bp = u.ap ↔ u.ap = u.bp
have mp : u.bp = u.ap → u.ap = u.bp
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
mp : u.bp = u.ap → u.ap = u.bp
⊢ u.bp = u.ap ↔ u.ap = u.bp
have mpr : u.ap = u.bp → u.bp = u.ap
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
⊢ u.flip.IsSpecial ↔ u.IsSpecial
have dsimp : u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
Tactic: dsimp [IsSpecial, flip]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
have rw : u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
Tactic: rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
rw : u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
have rw₁ : u.zp + u.wp + u.wp * u.zp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
Tactic: rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
rw : u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
rw₁ : u.zp + u.wp + u.wp * u.zp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
⊢ u.zp + u.wp + u.zp * u.wp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.x * u.y
have rw₂ : u.wp + u.zp + u.wp * u.zp = u.y * u.x ↔ u.wp + u.zp + u.wp * u.zp = u.y * u.x
Tactic: rw [mul_comm u.x, mul_comm u.zp, add_comm u.zp]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
⊢ u.flip.v = u.v.swap
have dsimp : ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)) =
  (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ))
Tactic: dsimp [v]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
⊢ ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)) =
    (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ))
have fst : ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)).1 =
  (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
fst :
  ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)).1 =
    (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)).1
⊢ ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)) =
    (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ))
have snd : ((↑u.z : ℕ) * (↑u.b : ℕ) + u.y * (↑u.a : ℕ), u.x * (↑u.b : ℕ) + (↑u.w : ℕ) * (↑u.a : ℕ)).2 =
  (u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ), (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hr : u.r = 0
⊢ u.q = u.qp + 1
have pos : ∀ (hq : u.q = 0), u.q = u.qp + 1
Tactic: by_cases hq : u.q = 0
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hr : u.r = 0
pos : ∀ (hq : u.q = 0), u.q = u.qp + 1
⊢ u.q = u.qp + 1
have neg : ∀ (hq : ¬u.q = 0), u.q = u.qp + 1
Tactic: by_cases hq : u.q = 0
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : u.r + (u.bp + 1) * u.q = u.ap + 1 := ⋯
⊢ u.q = u.qp + 1
have h₁ : 0 = u.ap + 1
Tactic: rw [hr, hq, mul_zero, add_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
⊢ (1 * ((↑a : ℕ) - 1 + 1) + 0 * ((↑b : ℕ) - 1 + 1), 0 * ((↑a : ℕ) - 1 + 1) + 1 * ((↑b : ℕ) - 1 + 1)) =
    ((↑a : ℕ), (↑b : ℕ))
have this : 0 < (↑a : ℕ)
Tactic: have := a.pos
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
a b : ℕ+
this : 0 < (↑a : ℕ)
⊢ (1 * ((↑a : ℕ) - 1 + 1) + 0 * ((↑b : ℕ) - 1 + 1), 0 * ((↑a : ℕ) - 1 + 1) + 1 * ((↑b : ℕ) - 1 + 1)) =
    ((↑a : ℕ), (↑b : ℕ))
have this₁ : 0 < (↑b : ℕ)
Tactic: have := b.pos
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hs : u.IsSpecial
⊢ u.finish.IsSpecial
have dsimp : u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y
Tactic: dsimp [IsSpecial, finish] at hs ⊢
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y
⊢ u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = ((u.wp + 1) * u.qp + u.x) * u.y
have rw : u.wp + (u.y * u.qp + u.zp) + u.wp * (u.y * u.qp + u.zp) = u.wp + u.zp + u.wp * u.zp + (u.wp + 1) * u.qp * u.y
Tactic: rw [add_mul _ _ u.y, add_comm _ (u.x * u.y), ← hs]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
u : XgcdType
hr : u.r = 0
ha : u.r + (↑u.b : ℕ) * u.q = (↑u.a : ℕ) := ⋯
⊢ u.finish.v = u.v
have ha₁ : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
Tactic: rw [hr, zero_add] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
⊢ u.finish.v = u.v
have fst : u.finish.v.1 = u.v.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
fst : u.finish.v.1 = u.v.1
⊢ u.finish.v = u.v
have snd : u.finish.v.2 = u.v.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
⊢ u.finish.v.1 = u.v.1
have fst : (u.wp + 1) * (↑u.b : ℕ) + ((u.wp + 1) * u.qp + u.x) * (↑u.b : ℕ) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)
Tactic: change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (hypothesis)
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
⊢ (u.wp + 1) * (↑u.b : ℕ) + ((u.wp + 1) * u.qp + u.x) * (↑u.b : ℕ) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)
have this : u.wp + 1 = (↑u.w : ℕ)
Tactic: have : u.wp + 1 = u.w := rfl
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
this : u.wp + 1 = (↑u.w : ℕ)
⊢ (u.wp + 1) * (↑u.b : ℕ) + ((u.wp + 1) * u.qp + u.x) * (↑u.b : ℕ) = (↑u.w : ℕ) * (↑u.a : ℕ) + u.x * (↑u.b : ℕ)
have fst : (↑u.w : ℕ) * (↑u.b : ℕ) + ((↑u.w : ℕ) * u.qp + u.x) * (↑u.b : ℕ) =
  (↑u.w : ℕ) * ((↑u.b : ℕ) * (u.qp + 1)) + u.x * (↑u.b : ℕ)
Tactic: rw [this, ← ha, u.qp_eq hr]
-- Lean 4 proof step from Mathlib.Data.PNat.Xgcd (goal)
Goal:
u : XgcdType
hr : u.r = 0
ha : (↑u.b : ℕ) * u.q = (↑u.a : ℕ)
⊢ u.finish.v.2 = u.v.2
have snd : u.y * (↑u.b : ℕ) + (u.y * u.qp + (↑u.z : ℕ)) * (↑u.b : ℕ) = u.y * (↑u.a : ℕ) + (↑u.z : ℕ) * (↑u.b : ℕ)
Tactic: change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b