awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
⊢ VectorAllP DiophFn (f :: fl) → Dioph (α := α) {v : α → ℕ | (v ⊗ fun (i : Fin2 n.succ) ↦ (f :: fl) i v) ∈ S}
have simp : DiophFn f → VectorAllP DiophFn fl → Dioph (α := α) {v : α → ℕ | (v ⊗ fun (i : Fin2 n.succ) ↦ (f :: fl) i v) ∈ S}
Tactic: simp only [vectorAllP_cons, and_imp]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ Membership.mem (γ := Set (α ⊕ Fin2 n → ℕ))
      {v : α ⊕ Fin2 n → ℕ |
        Membership.mem (γ := Set (Option (α ⊕ Fin2 n) → ℕ))
          {v : Option (α ⊕ Fin2 n) → ℕ | v ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S} (f (v ∘ inl) ::ₒ v)}
      v ↔
    Membership.mem (γ := Set (α ⊕ Fin2 n → ℕ)) {v : α ⊕ Fin2 n → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S} v
have dsimp : (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S ↔ (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S ↔ (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S
have a : (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) = v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) = v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr
have a : ∀ (x : α ⊕ Fin2 (n + 1)),
  ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) x = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
x : α ⊕ Fin2 (n + 1)
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) x = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) x
have a : ∀ (val : α),
  ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inl val) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inl val)
Tactic: obtain _ | _ | _ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
x : α ⊕ Fin2 (n + 1)
a :
  ∀ (val : α),
    ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inl val) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inl val)
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) x = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) x
have a₁ : ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inr fz) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inr fz)
Tactic: obtain _ | _ | _ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
x : α ⊕ Fin2 (n + 1)
a :
  ∀ (val : α),
    ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inl val) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inl val)
a₁ : ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inr fz) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inr fz)
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) x = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) x
have a₂ : ∀ (a : Fin2 n),
  ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inr a.fs) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inr a.fs)
Tactic: obtain _ | _ | _ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this_1 : Dioph (α := α ⊕ Fin2 n) {v : α ⊕ Fin2 n → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph (α := α) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S}
v : α → ℕ
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S} v ↔
    Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | (v ⊗ fun (i : Fin2 n.succ) ↦ (f :: fl) i v) ∈ S} v
have dsimp : (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S ↔ (v ⊗ fun (i : Fin2 (n + 1)) ↦ (f :: fl) i v) ∈ S
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this_1 : Dioph (α := α ⊕ Fin2 n) {v : α ⊕ Fin2 n → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph (α := α) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S}
v : α → ℕ
⊢ (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S ↔ (v ⊗ fun (i : Fin2 (n + 1)) ↦ (f :: fl) i v) ∈ S
have a : ∀ (x : Fin2 (n + 1)), (f v :: fun (i : Fin2 n) ↦ fl i v) x = (f :: fl) x v
Tactic: congr! 3 with x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this_1 : Dioph (α := α ⊕ Fin2 n) {v : α ⊕ Fin2 n → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph (α := α) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S}
v : α → ℕ
x : Fin2 (n + 1)
⊢ (f v :: fun (i : Fin2 n) ↦ fl i v) x = (f :: fl) x v
have a : cons (n := n) (f v) (fun (i : Fin2 n) ↦ fl i v) fz = (f :: fl) fz v
Tactic: obtain _ | _ | _ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this_1 : Dioph (α := α ⊕ Fin2 n) {v : α ⊕ Fin2 n → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph (α := α) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S}
v : α → ℕ
x : Fin2 (n + 1)
a : cons (n := n) (f v) (fun (i : Fin2 n) ↦ fl i v) fz = (f :: fl) fz v
⊢ (f v :: fun (i : Fin2 n) ↦ fl i v) x = (f :: fl) x v
have a₁ : ∀ {n : ℕ} (S : Set (α ⊕ Fin2 (n + 1).succ → ℕ)) (d : Dioph S) (f_2 : Vector3 ((α → ℕ) → ℕ) (n + 1).succ)
  (fl : Vector3 ((α → ℕ) → ℕ) (n + 1)) (dfl : VectorAllP DiophFn fl)
  (this : Dioph (α := α ⊕ Fin2 (n + 1)) {v : α ⊕ Fin2 (n + 1) → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S})
  (this : Dioph (α := α) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 (n + 1)) ↦ fl i v) ∈ S}),
  cons (n := n + 1) (f v) (fun (i : Fin2 (n + 1)) ↦ fl i v) (fs fz) = (f :: fl) (fs fz) v
Tactic: obtain _ | _ | _ := x
Cleared hypotheses: n, S, d, f_1, fl, dfl, this_1, this, x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this_1 : Dioph (α := α ⊕ Fin2 n) {v : α ⊕ Fin2 n → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph (α := α) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S}
v : α → ℕ
x : Fin2 (n + 1)
a : cons (n := n) (f v) (fun (i : Fin2 n) ↦ fl i v) fz = (f :: fl) fz v
a₁ :
  ∀ {n : ℕ} (S : Set (α ⊕ Fin2 (n + 1).succ → ℕ)) (d : Dioph S) (f_2 : Vector3 ((α → ℕ) → ℕ) (n + 1).succ)
    (fl : Vector3 ((α → ℕ) → ℕ) (n + 1)) (dfl : VectorAllP DiophFn fl)
    (this : Dioph (α := α ⊕ Fin2 (n + 1)) {v : α ⊕ Fin2 (n + 1) → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S})
    (this : Dioph (α := α) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 (n + 1)) ↦ fl i v) ∈ S}),
    cons (n := n + 1) (f v) (fun (i : Fin2 (n + 1)) ↦ fl i v) (fs fz) = (f :: fl) (fs fz) v
⊢ (f v :: fun (i : Fin2 n) ↦ fl i v) x = (f :: fl) x v
have a₂ : ∀ {n : ℕ} (a : Fin2 n) (S : Set (α ⊕ Fin2 (n + 1).succ → ℕ)) (d : Dioph S) (f_2 : Vector3 ((α → ℕ) → ℕ) (n + 1).succ)
  (fl : Vector3 ((α → ℕ) → ℕ) (n + 1)) (dfl : VectorAllP DiophFn fl)
  (this : Dioph (α := α ⊕ Fin2 (n + 1)) {v : α ⊕ Fin2 (n + 1) → ℕ | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S})
  (this : Dioph (α := α) {v : α → ℕ | (v ⊗ f v :: fun (i : Fin2 (n + 1)) ↦ fl i v) ∈ S}),
  (f v :: fun (i : Fin2 (n + 1)) ↦ fl i v) a.fs.fs = (f :: fl) a.fs.fs v
Tactic: obtain _ | _ | _ := x
Cleared hypotheses: n, S, d, f_1, fl, dfl, this_1, this, x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
⊢ VectorAllP (α := (Option α → ℕ) → ℕ) (n := n + 1) DiophFn
    ((fun (v : Option α → ℕ) ↦ v none) :: fun (i : Fin2 n) (v : Option α → ℕ) ↦ g i (v ∘ some))
have simp : (DiophFn (α := Option α) fun (v : Option α → ℕ) ↦ v none) ∧
  VectorAllP (α := (Option α → ℕ) → ℕ) (n := n) DiophFn fun (i : Fin2 n) (v : Option α → ℕ) ↦ g i (v ∘ some)
Tactic: simp only [vectorAllP_cons]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ (x : ℕ), v &0 + v &2 * x = v &1}
z x y : ℕ
h_1 : (y = 0 ∨ z < y) ∧ ∃ (c : ℕ), z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ x % y = z
have rw : (z + y * c) % y = z
Tactic: rw [← hc]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ (x : ℕ), v &0 + v &2 * x = v &1}
z x y : ℕ
h_1 : (y = 0 ∨ z < y) ∧ ∃ (c : ℕ), z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ (z + y * c) % y = z
have simp : z % y = z
Tactic: simp only [add_mul_mod_self_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ (x : ℕ), v &0 + v &2 * x = v &1}
z x y : ℕ
h_1 : (y = 0 ∨ z < y) ∧ ∃ (c : ℕ), z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ z % y = z
have inl : ∀ (x0 : y = 0), z % y = z
Tactic: rcases h with x0 | hl
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ (x : ℕ), v &0 + v &2 * x = v &1}
z x y : ℕ
h_1 : (y = 0 ∨ z < y) ∧ ∃ (c : ℕ), z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
inl : ∀ (x0 : y = 0), z % y = z
⊢ z % y = z
have inr : ∀ (hl : z < y), z % y = z
Tactic: rcases h with x0 | hl
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ (x : ℕ), v &0 + v &2 * x = v &1}
z x y : ℕ
h : (y = 0 ∨ z < y) ∧ ∃ (c : ℕ), z + y * c = x
c : ℕ
hc : z + y * c = x
x0 : y = 0
⊢ z % y = z
have inl : z % 0 = z
Tactic: rw [x0, mod_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ (x : ℕ), v &0 + v &2 * x = v &1}
z x y : ℕ
h : (y = 0 ∨ z < y) ∧ ∃ (c : ℕ), z + y * c = x
c : ℕ
hc : z + y * c = x
x0 : y = 0
inl : z % 0 = z
⊢ z % y = z
have inl₁ : z = z
Tactic: rw [x0, mod_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ (x : ℕ), v &0 + v &2 * x = v &1}
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ z < y) ∧ ∃ (c : ℕ), z + y * c = x
have rw : (y = 0 ∨ x % y < y) ∧ ∃ (c : ℕ), x % y + y * c = x
Tactic: rw [← e]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
have inl : Eq (α := ℕ) 0 0 ∧ z = 0 ∨ z * 0 ≤ x ∧ x < (z + 1) * 0 ↔ x / 0 = z
Tactic: rcases y.eq_zero_or_pos with rfl | hy
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
inl : Eq (α := ℕ) 0 0 ∧ z = 0 ∨ z * 0 ≤ x ∧ x < (z + 1) * 0 ↔ x / 0 = z
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
have inr : ∀ (hy : y > 0), y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
Tactic: rcases y.eq_zero_or_pos with rfl | hy
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph (α := Fin2 3) {v : Vector3 ℕ 3 | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
hy : y > 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
have inr : y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < z * y + y ↔ z * y ≤ x ∧ x ≤ z * y + y - 1
Tactic: rw [Nat.div_eq_iff hy, Nat.succ_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (hypothesis)
Goal:
⊢ Dioph (α := Fin2 4) {v : Vector3 ℕ 4 | ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3}
have this : Dioph (α := Fin2 4)
  {v : Vector3 ℕ 4 |
    1 < v &0 ∧
      v &1 ≤ v &3 ∧
        (v &2 = 1 ∧ v &3 = 0 ∨
          ∃ (u : ℕ) (w : ℕ) (s : ℕ) (t : ℕ) (b : ℕ),
            v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
              u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
                s * s - (b * b - 1) * t * t = 1 ∧
                  1 < b ∧
                    b ≡ 1 [MOD 4 * v &3] ∧
                      b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])}
Tactic: have : Dioph {v : Vector3 ℕ 4 |
    1 < v &0 ∧ v &1 ≤ v &3 ∧
    (v &2 = 1 ∧ v &3 = 0 ∨
    ∃ u w s t b : ℕ,
      v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
      u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
      s * s - (b * b - 1) * t * t = 1 ∧
      1 < b ∧ b ≡ 1 [MOD 4 * v &3] ∧ b ≡ v &0 [MOD u] ∧
      0 < w ∧ v &3 * v &3 ∣ w ∧
      s ≡ v &2 [MOD u] ∧
      t ≡ v &1 [MOD 4 * v &3])} :=
  (D.1 D< D&0 D∧ D&1 D≤ D&3 D∧
    ((D&2 D= D.1 D∧ D&3 D= D.0) D∨
    ((D∃) 4 <| (D∃) 5 <| (D∃) 6 <| (D∃) 7 <| (D∃) 8 <|
    D&7 D* D&7 D- (D&5 D* D&5 D- D.1) D* D&8 D* D&8 D= D.1 D∧
    D&4 D* D&4 D- (D&5 D* D&5 D- D.1) D* D&3 D* D&3 D= D.1 D∧
    D&2 D* D&2 D- (D&0 D* D&0 D- D.1) D* D&1 D* D&1 D= D.1 D∧
    D.1 D< D&0 D∧ (D≡ (D&0) (D.1) (D.4 D* D&8)) D∧ (D≡ (D&0) (D&5) (D&4)) D∧
    D.0 D< D&3 D∧ D&8 D* D&8 D∣ D&3 D∧
    (D≡ (D&2) (D&7) (D&4)) D∧
    (D≡ (D&1) (D&6) (D.4 D* (D&8))))) :)
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (hypothesis)
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ DiophFn (α := α) fun (v : α → ℕ) ↦ f v ^ g v
have this : Dioph (α := Fin2 3)
  {v : Vector3 ℕ 3 |
    v &2 = 0 ∧ v &0 = 1 ∨
      0 < v &2 ∧
        (v &1 = 0 ∧ v &0 = 0 ∨
          0 < v &1 ∧
            ∃ (w : ℕ) (a : ℕ) (t : ℕ) (z : ℕ) (x : ℕ) (y : ℕ),
              (∃ (a1 : 1 < a), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
                x ≡ y * (a - v &1) + v &0 [MOD t] ∧
                  2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
                    v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)}
Tactic: have : Dioph {v : Vector3 ℕ 3 |
    v &2 = 0 ∧ v &0 = 1 ∨ 0 < v &2 ∧
    (v &1 = 0 ∧ v &0 = 0 ∨ 0 < v &1 ∧
    ∃ w a t z x y : ℕ,
      (∃ a1 : 1 < a, xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
      x ≡ y * (a - v &1) + v &0 [MOD t] ∧
      2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧
      a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)} :=
  (D&2 D= D.0 D∧ D&0 D= D.1) D∨ (D.0 D< D&2 D∧
    ((D&1 D= D.0 D∧ D&0 D= D.0) D∨ (D.0 D< D&1 D∧
    ((D∃) 3 <| (D∃) 4 <| (D∃) 5 <| (D∃) 6 <| (D∃) 7 <| (D∃) 8 <|
    pell_dioph.reindex_dioph (Fin2 9) [&4, &8, &1, &0] D∧
    (D≡ (D&1) (D&0 D* (D&4 D- D&7) D+ D&6) (D&3)) D∧
    D.2 D* D&4 D* D&7 D= D&3 D+ (D&7 D* D&7 D+ D.1) D∧
    D&6 D< D&3 D∧ D&7 D≤ D&5 D∧ D&8 D≤ D&5 D∧
    D&4 D* D&4 D- ((D&5 D+ D.1) D* (D&5 D+ D.1) D- D.1) D* (D&5 D* D&2) D* (D&5 D* D&2) D= D.1))) :)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: have hn : 0 < (n : ℝ) + 1 := mod_cast Nat.succ_pos _
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: have hfu := fun m : ℤ => mul_lt_of_lt_one_left hn <| fract_lt_one (ξ * ↑m)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
j k : ℤ
| |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rw : |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: rw [mul_comm, le_div_iff₀ hn, ← abs_of_pos hn, ← abs_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have conv : ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: conv in |_| ≤ _ => rw [mul_comm, le_div_iff₀ hn, ← abs_of_pos hn, ← abs_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have pos : ∀ (H : ∃ m ∈ D, f m = (↑n : ℤ)),
  ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: by_cases! H : ∃ m ∈ D, f m = n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
pos :
  ∀ (H : ∃ m ∈ D, f m = (↑n : ℤ)),
    ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have neg : ∀ (H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)),
  ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: by_cases! H : ∃ m ∈ D, f m = n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∃ m ∈ D, f m = (↑n : ℤ)
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have pos : ∀ (m : ℤ) (hm : m ∈ D) (hf : f m = (↑n : ℤ)),
  ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
Tactic: obtain ⟨m, hm, hf⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: have hf' : ((n : ℤ) : ℝ) ≤ fract (ξ * m) * (n + 1) := hf ▸ floor_le (fract (ξ * m) * (n + 1))
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ 0 < m
have hf₀ : f 0 = 0
Tactic: have hf₀ : f 0 = 0 := by
        simp only [f, cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hf₀ : f 0 = 0
⊢ 0 < m
have refine : ∀ (h : 0 = m), 0 = n
Tactic: refine Ne.lt_of_le (fun h => n_pos.ne ?_) (mem_Icc.mp hm).1
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
m : ℤ
hm : m ∈ D
hf : f m = (↑n : ℤ)
hf' : (↑(↑n : ℤ) : ℝ) ≤ fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
have hm₀ : 0 < m
Tactic: have hm₀ : 0 < m := by
      have hf₀ : f 0 = 0 := by
        simp only [f, cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
      refine Ne.lt_of_le (fun h => n_pos.ne ?_) (mem_Icc.mp hm).1
      exact mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)