awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
h : VectorAllP DiophFn f
v : α → ℕ
x : α ⊕ Fin2 0
a : ∀ (val : α), (v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α))) (inl val) = (v ⊗ fun (i : Fin2 0) ↦ f i v) (inl val)
⊢ (v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α))) x = (v ⊗ fun (i : Fin2 0) ↦ f i v) x

Tactic:
obtain _ | _ | _ := x
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
h : VectorAllP DiophFn f
v : α → ℕ
val : α
⊢ (v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α))) (inl val) = (v ⊗ fun (i : Fin2 0) ↦ f i v) (inl val)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
simp : DiophFn f → VectorAllP DiophFn fl → Dioph (α := α) {v : α → ℕ | (v ⊗ fun (i : Fin2 n.succ) ↦ (f :: fl) i v) ∈ S}
⊢ VectorAllP DiophFn (f :: fl) → Dioph (α := α) {v : α → ℕ | (v ⊗ fun (i : Fin2 n.succ) ↦ (f :: fl) i v) ∈ S}

Tactic:
simp only [vectorAllP_cons, and_imp]

Premises used: and_imp, vectorAllP_cons
-- Module: Mathlib.NumberTheory.Dioph
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 → ℕ
dsimp : (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S ↔ (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.Dioph
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 → ℕ
a : (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) = v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) ∈ S ↔ (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S

Tactic:
congr! 1
-- Module: Mathlib.NumberTheory.Dioph
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 → ℕ
a :
  ∀ (x : α ⊕ Fin2 (n + 1)),
    ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) x = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) x
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) = v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Dioph
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)
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)
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) x = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) x

Tactic:
obtain _ | _ | _ := x
-- Module: Mathlib.NumberTheory.Dioph
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 → ℕ
val : α
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) (inl val) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inl val)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
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)) (inr fz) = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) (inr fz)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
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 → ℕ
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:
rfl
-- Module: Mathlib.NumberTheory.Dioph
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 : α → ℕ
dsimp : (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S ↔ (v ⊗ fun (i : Fin2 (n + 1)) ↦ (f :: fl) i v) ∈ S
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.Dioph
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 : α → ℕ
a : ∀ (x : Fin2 (n + 1)), (f v :: fun (i : Fin2 n) ↦ fl i v) x = (f :: fl) x v
⊢ (v ⊗ f v :: fun (i : Fin2 n) ↦ fl i v) ∈ S ↔ (v ⊗ fun (i : Fin2 (n + 1)) ↦ (f :: fl) i v) ∈ S

Tactic:
congr! 3 with x
-- Module: Mathlib.NumberTheory.Dioph
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
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
⊢ (f v :: fun (i : Fin2 n) ↦ fl i v) x = (f :: fl) x v

Tactic:
obtain _ | _ | _ := x
-- Module: Mathlib.NumberTheory.Dioph
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 : α → ℕ
⊢ cons (n := n) (f v) (fun (i : Fin2 n) ↦ fl i v) fz = (f :: fl) fz v

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f_1 : (α → ℕ) → ℕ
df : DiophFn f_1
v : α → ℕ
n : ℕ
S : Set (α ⊕ Fin2 (n + 1).succ → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) (n + 1).succ
fl : Vector3 ((α → ℕ) → ℕ) (n + 1)
dfl : VectorAllP DiophFn fl
this_1 : Dioph (α := α ⊕ Fin2 (n + 1)) {v : α ⊕ Fin2 (n + 1) → ℕ | (v ∘ inl ⊗ f_1 (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph (α := α) {v : α → ℕ | (v ⊗ f_1 v :: fun (i : Fin2 (n + 1)) ↦ fl i v) ∈ S}
⊢ cons (n := n + 1) (f_1 v) (fun (i : Fin2 (n + 1)) ↦ fl i v) (fs fz) = (f_1 :: fl) (fs fz) v

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f_1 : (α → ℕ) → ℕ
df : DiophFn f_1
v : α → ℕ
n : ℕ
a : Fin2 n
S : Set (α ⊕ Fin2 (n + 1).succ → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) (n + 1).succ
fl : Vector3 ((α → ℕ) → ℕ) (n + 1)
dfl : VectorAllP DiophFn fl
this_1 : Dioph (α := α ⊕ Fin2 (n + 1)) {v : α ⊕ Fin2 (n + 1) → ℕ | (v ∘ inl ⊗ f_1 (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph (α := α) {v : α → ℕ | (v ⊗ f_1 v :: fun (i : Fin2 (n + 1)) ↦ fl i v) ∈ S}
⊢ (f_1 v :: fun (i : Fin2 (n + 1)) ↦ fl i v) a.fs.fs = (f_1 :: fl) a.fs.fs v

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f_1 : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
⊢ DiophFn f → VectorAllP DiophFn fl → Dioph (α := α) {v : α → ℕ | (v ⊗ fun (i : Fin2 n.succ) ↦ (f :: fl) i v) ∈ S}

Tactic:
exact fun df dfl =>
          have : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl)::v ∘ inr) ∈ S} :=
            ext (diophFn_comp1 (reindex_dioph _ (some ∘ inl ⊗ none :: some ∘ inr) d) <|
                reindex_diophFn inl df)
              fun v => by
                dsimp
                -- TODO: `congr! 1; ext` should be equivalent to `congr! 1 with x`
                -- but that does not work.
                congr! 1
                ext x; obtain _ | _ | _ := x <;> rfl
          have : Dioph {v | (v ⊗ f v::fun i : Fin2 n => fl i v) ∈ S} :=
            @diophFn_compn n (fun v => (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S) this _ dfl
          ext this fun v => by
            dsimp
            congr! 3 with x
            obtain _ | _ | _ := x <;> rfl

Premises used: Dioph.ext, Option.some, Function.comp, Sum, Sum.inl, Dioph.reindex_dioph, Option.none, Vector3.cons, Sum.inr, Dioph.reindex_diophFn, Dioph.diophFn_comp1, Sum.elim, Fin2, Option
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
n : ℕ
S : Set (Vector3 ℕ n)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) n
df : VectorAllP DiophFn f
⊢ Dioph (α := α) {v : α → ℕ | (fun (i : Fin2 n) ↦ f i v) ∈ S}

Tactic:
diophFn_compn (reindex_dioph _ inr d) df

Premises used: Set.Mem, setOf, Dioph.reindex_dioph, Sum.inr, Dioph.diophFn_compn, Sum.elim
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
simp :
  (DiophFn (α := Option α) fun (v : Option α → ℕ) ↦ v none) ∧
    VectorAllP (α := (Option α → ℕ) → ℕ) (n := n) DiophFn fun (i : Fin2 n) (v : Option α → ℕ) ↦ g i (v ∘ some)
⊢ VectorAllP (α := (Option α → ℕ) → ℕ) (n := n + 1) DiophFn
    ((fun (v : Option α → ℕ) ↦ v none) :: fun (i : Fin2 n) (v : Option α → ℕ) ↦ g i (v ∘ some))

Tactic:
simp only [vectorAllP_cons]

Premises used: vectorAllP_cons
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
⊢ (DiophFn (α := Option α) fun (v : Option α → ℕ) ↦ v none) ∧
    VectorAllP (α := (Option α → ℕ) → ℕ) (n := n) DiophFn fun (i : Fin2 n) (v : Option α → ℕ) ↦ g i (v ∘ some)

Tactic:
⟨proj_dioph none, (vectorAllP_iff_forall _ _).2 fun i =>
          reindex_diophFn _ <| (vectorAllP_iff_forall _ _).1 dg _⟩

Premises used: Iff.mpr, Option.some, Dioph.proj_dioph, Option.none, Dioph.reindex_diophFn, And.intro, Iff.mp, Dioph.DiophFn, vectorAllP_iff_forall
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
n : ℕ
f : Vector3 ℕ n → ℕ
df : DiophFn f
g : Vector3 ((α → ℕ) → ℕ) n
dg : VectorAllP DiophFn g
⊢ (DiophFn (α := Option α) fun (v : Option α → ℕ) ↦ v none) ∧
    VectorAllP (α := (Option α → ℕ) → ℕ) (n := n) DiophFn fun (i : Fin2 n) (v : Option α → ℕ) ↦ g i (v ∘ some)

Tactic:
exact ⟨proj_dioph none, (vectorAllP_iff_forall _ _).2 fun i =>
          reindex_diophFn _ <| (vectorAllP_iff_forall _ _).1 dg _⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n m : ℕ
inst : IsLT m n
⊢ DiophFn (α := Fin2 n) fun (v : Vector3 ℕ n) ↦ v &m

Tactic:
proj_dioph &m

Premises used: Fin2.ofNat', Dioph.proj_dioph, Vector3
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
n : ℕ
⊢ DiophFn (α := α) (const (α → ℕ) n)

Tactic:
abs_poly_dioph (Poly.const n)

Premises used: Nat.cast, Poly.const, Int.natAbs, Dioph.abs_poly_dioph
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
S : ℕ → ℕ → Prop
d : Dioph (α := Fin2 2) {v : Vector3 ℕ 2 | S (v &0) (v &1)}
⊢ Dioph (α := α) {v : α → ℕ | S (f v) (g v)}

Tactic:
dioph_comp d [f, g] ⟨df, dg⟩

Premises used: Set.Mem, setOf, Fin2.ofNat', Vector3.nil, Vector3.cons, And.intro, Fin2.cases', Dioph.dioph_comp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
h : ℕ → ℕ → ℕ
d : DiophFn (α := Fin2 2) fun (v : Vector3 ℕ 2) ↦ h (v &0) (v &1)
⊢ DiophFn (α := α) fun (v : α → ℕ) ↦ h (f v) (g v)

Tactic:
diophFn_comp d [f, g] ⟨df, dg⟩

Premises used: Dioph.diophFn_comp, Fin2.ofNat', Vector3.nil, Vector3.cons, And.intro, Fin2.cases'
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : Fin2 2 → ℕ
⊢ Membership.mem (γ := Set (Fin2 2 → ℕ)) {v : Vector3 ℕ 2 | v &0 = v &1} v ↔
    Eq (α := ℤ) ((HSub.hSub (α := Poly (Fin2 2)) (Poly.proj &0) (Poly.proj &1) : (a : Fin2 2 → ℕ) → ℤ) v : ℤ) (0 : ℤ)

Tactic:
Int.ofNat_inj.symm.trans ⟨@sub_eq_zero_of_eq ℤ _ (v &0) (v &1), eq_of_sub_eq_zero⟩

Premises used: Set.Mem, setOf, Int.ofNat_inj, eq_of_sub_eq_zero, sub_eq_zero_of_eq, Iff.intro, Iff.trans, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : Fin2 2 → ℕ
⊢ Membership.mem (γ := Set (Fin2 2 → ℕ)) {v : Vector3 ℕ 2 | v &0 = v &1} v ↔
    Eq (α := ℤ) ((HSub.hSub (α := Poly (Fin2 2)) (Poly.proj &0) (Poly.proj &1) : (a : Fin2 2 → ℕ) → ℤ) v : ℤ) (0 : ℤ)

Tactic:
exact Int.ofNat_inj.symm.trans ⟨@sub_eq_zero_of_eq ℤ _ (v &0) (v &1), eq_of_sub_eq_zero⟩

Premises used: Int.ofNat_inj, eq_of_sub_eq_zero, sub_eq_zero_of_eq, Iff.intro, Iff.trans, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ DiophFn (α := α) fun (v : α → ℕ) ↦ f v + g v

Tactic:
diophFn_comp2 df dg <| abs_poly_dioph (@Poly.proj (Fin2 2) &0 + @Poly.proj (Fin2 2) &1)

Premises used: Fin2.ofNat', Poly.proj, HAdd.hAdd, Dioph.abs_poly_dioph, OfNat.ofNat, Dioph.diophFn_comp2
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ DiophFn (α := α) fun (v : α → ℕ) ↦ f v * g v

Tactic:
diophFn_comp2 df dg <| abs_poly_dioph (@Poly.proj (Fin2 2) &0 * @Poly.proj (Fin2 2) &1)

Premises used: HMul.hMul, Fin2.ofNat', Poly.proj, Dioph.abs_poly_dioph, OfNat.ofNat, Dioph.diophFn_comp2
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ Dioph (α := α) {v : α → ℕ | f v ≤ g v}

Tactic:
dioph_comp2 df dg <|
    ext ((D∃) 2 <| D&1 D+ D&0 D= D&2) fun _ => ⟨fun ⟨_, hx⟩ => le.intro hx, le.dest⟩

Premises used: Dioph.ext, Dioph.dioph_comp2, setOf, Dioph.vec_ex1_dioph, _private.0.Dioph.le_dioph.match_1, Dioph.eq_dioph, Fin2.ofNat', Membership.mem, Nat.le.intro, LE.le, Iff.intro, Dioph.proj_dioph_of_nat, Nat.le.dest, OfNat.ofNat, Dioph.add_dioph
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ Dioph (α := α) {v : α → ℕ | f v < g v}

Tactic:
df D+ D.1 D≤ dg

Premises used: Dioph.le_dioph, setOf, Dioph.const_dioph, OfNat.ofNat, Dioph.add_dioph, Nat.lt
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ Membership.mem (γ := Set (α → ℕ)) ({v : α → ℕ | f v < g v} ∪ {v : α → ℕ | g v < f v}) v ↔ ¬f v = g v

Tactic:
lt_or_lt_iff_ne (α := ℕ)

Premises used: Set.union, Set.Mem, setOf, lt_or_lt_iff_ne, Nat.lt
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ Membership.mem (γ := Set (α → ℕ)) ({v : α → ℕ | f v < g v} ∪ {v : α → ℕ | g v < f v}) v ↔ ¬f v = g v

Tactic:
exact lt_or_lt_iff_ne (α := ℕ)

Premises used: lt_or_lt_iff_ne
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
x y z : ℕ
⊢ y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x

Tactic:
grind
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ Dioph (α := α) {v : α → ℕ | f v ∣ g v}

Tactic:
dioph_comp ((D∃) 2 <| D&2 D= D&1 D* D&0) [f, g] ⟨df, dg⟩

Premises used: Set.Mem, Dioph.mul_dioph, setOf, Dioph.vec_ex1_dioph, Dioph.eq_dioph, Fin2.ofNat', Vector3.nil, Vector3.cons, And.intro, Dioph.proj_dioph_of_nat, Fin2.cases', OfNat.ofNat, Dioph.dioph_comp
-- Module: Mathlib.NumberTheory.Dioph
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
rw : (z + y * c) % y = z
⊢ x % y = z

Tactic:
rw [← hc]
-- Module: Mathlib.NumberTheory.Dioph
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
simp : z % y = z
⊢ (z + y * c) % y = z

Tactic:
simp only [add_mul_mod_self_left]

Premises used: Nat.add_mul_mod_self_left
-- Module: Mathlib.NumberTheory.Dioph
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
inr : ∀ (hl : z < y), z % y = z
⊢ z % y = z

Tactic:
rcases h with x0 | hl
-- Module: Mathlib.NumberTheory.Dioph
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
inl₁ inl₂ : z = z
⊢ z % y = z

Tactic:
rw [x0, mod_zero]

Premises used: Nat.mod_zero
-- Module: Mathlib.NumberTheory.Dioph
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
hl : z < y
⊢ z % y = z

Tactic:
mod_eq_of_lt hl

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.Dioph
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
hl : z < y
⊢ z % y = z

Tactic:
exact mod_eq_of_lt hl

Premises used: Nat.mod_eq_of_lt
-- Module: Mathlib.NumberTheory.Dioph
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
rw : (y = 0 ∨ x % y < y) ∧ ∃ (c : ℕ), x % y + y * c = x
⊢ (y = 0 ∨ z < y) ∧ ∃ (c : ℕ), z + y * c = x

Tactic:
rw [← e]
-- Module: Mathlib.NumberTheory.Dioph
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 ∨ x % y < y) ∧ ∃ (c : ℕ), x % y + y * c = x

Tactic:
⟨or_iff_not_imp_left.2 fun h => mod_lt _ (Nat.pos_of_ne_zero h), x / y,
                  mod_add_div _ _⟩

Premises used: Iff.mpr, HDiv.hDiv, Nat.mod_lt, Nat.mod_add_div, Nat.pos_of_ne_zero, Classical.or_iff_not_imp_left, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Dioph
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 ∨ x % y < y) ∧ ∃ (c : ℕ), x % y + y * c = x

Tactic:
exact ⟨or_iff_not_imp_left.2 fun h => mod_lt _ (Nat.pos_of_ne_zero h), x / y,
                  mod_add_div _ _⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
h : (α → ℕ) → ℕ
dh : DiophFn h
⊢ Dioph (α := α) {v : α → ℕ | f v ≡ g v [MOD h v]}

Tactic:
df D% dh D= dg D% dh

Premises used: setOf, Dioph.eq_dioph, Nat.ModEq, Dioph.mod_dioph
-- Module: Mathlib.NumberTheory.Dioph
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
inr : ∀ (hy : y > 0), y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z

Tactic:
rcases y.eq_zero_or_pos with rfl | hy

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Dioph
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 : ℕ
⊢ Eq (α := ℕ) 0 0 ∧ z = 0 ∨ z * 0 ≤ x ∧ x < (z + 1) * 0 ↔ x / 0 = z

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.NumberTheory.Dioph
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
inr : y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < z * y + y ↔ z * y ≤ x ∧ x ≤ z * y + y - 1
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z

Tactic:
rw [Nat.div_eq_iff hy, Nat.succ_mul]

Premises used: Nat.div_eq_iff, Nat.succ_mul
-- Module: Mathlib.NumberTheory.Dioph
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 * y + y ↔ z * y ≤ x ∧ x ≤ z * y + y - 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Dioph
Goal:
⊢ 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))))) :)