awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)

Tactic:
ht
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)

Tactic:
exact ht
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (Sum.inr none ::ₒ Sum.inl ⊗ Sum.inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ)
      (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (Sum.inr none ::ₒ Sum.inl ⊗ Sum.inr ∘ some)) : ℤ) (0 : ℤ)
s : Option α ⊕ β
inl :
  ∀ (a : Option α),
    ((v ⊗ t) ∘ (Sum.inr none ::ₒ Sum.inl ⊗ Sum.inr ∘ some)) (Sum.inl a) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl a)
inr :
  ∀ (b : β), ((v ⊗ t) ∘ (Sum.inr none ::ₒ Sum.inl ⊗ Sum.inr ∘ some)) (Sum.inr b) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inr b)
⊢ ((v ⊗ t) ∘ (Sum.inr none ::ₒ Sum.inl ⊗ Sum.inr ∘ some)) s = (t none ::ₒ v ⊗ t ∘ some) s

Tactic:
rcases s with a | b
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ Sum.inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₁ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
⊢ ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl a)

Tactic:
cases a
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (t none ::ₒ v ⊗ t ∘ some) (inl none)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
val : α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl (some val)) = (t none ::ₒ v ⊗ t ∘ some) (inl (some val))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ Sum.inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₁ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
inl₂ : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₃ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
inl₄ : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₅ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
inl₆ : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₇ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
⊢ ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl a)

Tactic:
{ cases a <;> rfl }
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ Sum.inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₁ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
inl₂ : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₃ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
inl₄ : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₅ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
inl₆ : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
inl₇ :
  ∀ (val : α),
    ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) =
      (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
⊢ ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl a)

Tactic:
try { cases a <;> rfl }
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (t none ::ₒ v ⊗ t ∘ some) : ℤ) (0 : ℤ)),
    Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (t none ::ₒ v ⊗ t ∘ some) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (t none ::ₒ v ⊗ t ∘ some) : ℤ) (0 : ℤ)

Tactic:
rwa [show (v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = t none ::ₒ v ⊗ t ∘ some from
                funext fun s => by rcases s with a | b <;> try { cases a <;> rfl }; rfl] at ht

Premises used: funext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
f : (α → ℕ) →. ℕ
d : DiophPFun f
⊢ Dioph f.Dom

Tactic:
cast (congr_arg Dioph <| Set.ext fun _ => (PFun.dom_iff_graph _ _).symm) (ex1_dioph d)

Premises used: Set.ext, Dioph, cast, congr_arg, Dioph.ex1_dioph, PFun.dom_iff_graph, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
f : (α → ℕ) → ℕ
⊢ DiophFn f = DiophPFun (↑f : (α → ℕ) →. ℕ)

Tactic:
congr_arg Dioph (Set.ext fun v => ?_)

Premises used: Set.ext, Dioph, congr_arg, Dioph.DiophPFun, Dioph.DiophFn
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
f : (α → ℕ) → ℕ
refine :
  ∀ (v : Option α → ℕ),
    Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | f (v ∘ some) = v none} v ↔
      Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | (v ∘ some, v none) ∈ (↑f : (α → ℕ) →. ℕ).graph} v
⊢ DiophFn f = DiophPFun (↑f : (α → ℕ) →. ℕ)

Tactic:
refine congr_arg Dioph (Set.ext fun v => ?_)

Premises used: Set.ext, Dioph, congr_arg
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
f : (α → ℕ) → ℕ
v : Option α → ℕ
⊢ Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | f (v ∘ some) = v none} v ↔
    Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | (v ∘ some, v none) ∈ (↑f : (α → ℕ) →. ℕ).graph} v

Tactic:
PFun.lift_graph.symm

Premises used: Part.Mem, PFun.graph, Set.Mem, setOf, PFun.lift_graph, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
f : (α → ℕ) → ℕ
v : Option α → ℕ
⊢ Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | f (v ∘ some) = v none} v ↔
    Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | (v ∘ some, v none) ∈ (↑f : (α → ℕ) →. ℕ).graph} v

Tactic:
exact PFun.lift_graph.symm

Premises used: PFun.lift_graph, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
p : Poly α
v : Option α → ℕ
dsimp :
  Int.natAbs ((p : (a : α → ℕ) → ℤ) (v ∘ some)) = v none ↔
    HSub.hSub (α := ℤ) (β := ℤ) ((p : (a : α → ℕ) → ℤ) (v ∘ some) : ℤ) ((↑(v none) : ℤ) : ℤ) *
        HAdd.hAdd (α := ℤ) (β := ℤ) ((p : (a : α → ℕ) → ℤ) (v ∘ some) : ℤ) ((↑(v none) : ℤ) : ℤ) =
      0
⊢ Membership.mem (γ := Set (Option α → ℕ))
      {v : Option α → ℕ | (fun (v : α → ℕ) ↦ Int.natAbs ((p : (a : α → ℕ) → ℤ) v)) (v ∘ some) = v none} v ↔
    Eq (α := ℤ)
      (((Poly.map some p - Poly.proj none) * (Poly.map some p + Poly.proj none) : (a : Option α → ℕ) → ℤ) v : ℤ) (0 : ℤ)

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
p : Poly α
v : Option α → ℕ
⊢ Int.natAbs ((p : (a : α → ℕ) → ℤ) (v ∘ some)) = v none ↔
    HSub.hSub (α := ℤ) (β := ℤ) ((p : (a : α → ℕ) → ℤ) (v ∘ some) : ℤ) ((↑(v none) : ℤ) : ℤ) *
        HAdd.hAdd (α := ℤ) (β := ℤ) ((p : (a : α → ℕ) → ℤ) (v ∘ some) : ℤ) ((↑(v none) : ℤ) : ℤ) =
      0

Tactic:
Int.natAbs_eq_iff_mul_eq_zero

Premises used: Int.natAbs_eq_iff_mul_eq_zero
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
p : Poly α
v : Option α → ℕ
⊢ Int.natAbs ((p : (a : α → ℕ) → ℤ) (v ∘ some)) = v none ↔
    HSub.hSub (α := ℤ) (β := ℤ) ((p : (a : α → ℕ) → ℤ) (v ∘ some) : ℤ) ((↑(v none) : ℤ) : ℤ) *
        HAdd.hAdd (α := ℤ) (β := ℤ) ((p : (a : α → ℕ) → ℤ) (v ∘ some) : ℤ) ((↑(v none) : ℤ) : ℤ) =
      0

Tactic:
exact Int.natAbs_eq_iff_mul_eq_zero

Premises used: Int.natAbs_eq_iff_mul_eq_zero
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
i : α
⊢ DiophFn.{u} (α := α) fun (v : α → ℕ) ↦ v i

Tactic:
abs_poly_dioph (Poly.proj i)

Premises used: Poly.proj, Int.natAbs, Dioph.abs_poly_dioph
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
h :
  ∃ (h : (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).Dom),
    (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).get h = ((x ::ₒ v) ∘ some, (x ::ₒ v) none).2
⊢ ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2

Tactic:
rw [show (x ::ₒ v) ∘ some = v from funext fun s => rfl] at h

Premises used: funext, rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
⊢ (f (v, (x ::ₒ v) none).1).Dom

Tactic:
obtain ⟨hf, h⟩ := h
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
hf : (f (v, (x ::ₒ v) none).1).Dom
⊢ (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2

Tactic:
obtain ⟨hf, h⟩ := h
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v

Tactic:
⟨hf, ?_⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
refine : f.fn v hf ::ₒ v ∈ S
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v

Tactic:
refine ⟨hf, ?_⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
rw : (v, (x ::ₒ v) none).2 ::ₒ v ∈ S
⊢ f.fn v hf ::ₒ v ∈ S

Tactic:
rw [PFun.fn, h]

Premises used: PFun.fn
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ (v, (x ::ₒ v) none).2 ::ₒ v ∈ S

Tactic:
hS

Premises used: Option.elim', Set.Mem
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ (v, (x ::ₒ v) none).2 ::ₒ v ∈ S

Tactic:
exact hS
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v
x : f.Dom v
hS : f.fn v x ::ₒ v ∈ S
rw : ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2
⊢ ∃ (h : (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).Dom),
    (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).get h = ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).2

Tactic:
rw [show (f.fn v x ::ₒ v) ∘ some = v from funext fun s => rfl]

Premises used: funext, rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v
x : f.Dom v
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2

Tactic:
⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v
x : f.Dom v
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) → ℕ
df : DiophFn f
⊢ Dioph.{u} (α := α) {v : α → ℕ | f v ::ₒ v ∈ S}

Tactic:
ext (diophPFun_comp1 d <| cast (diophFn_iff_pFun f) df)
    fun _ => ⟨fun ⟨_, h⟩ => h, fun h => ⟨trivial, h⟩⟩

Premises used: Option.elim', Dioph.ext, trivial, setOf, cast, Membership.mem, Dioph.diophFn_iff_pFun, Iff.intro, Exists.intro, Dioph.diophPFun_comp1, _private.0.Dioph.diophFn_comp1.match_1
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
dsimp : ((f v ::ₒ v) ∘ none :: some) ∈ S ↔ Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v
⊢ Membership.mem (γ := Set (Fin2 n → ℕ))
      {v : Fin2 n → ℕ |
        Membership.mem (γ := Set (Option (Fin2 n) → ℕ)) {v : Option (Fin2 n) → ℕ | (v ∘ none :: some) ∈ S} (f v ::ₒ v)}
      v ↔
    Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
a : (((f v ::ₒ v) ∘ none :: some) ∈ S) = Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v
⊢ ((f v ::ₒ v) ∘ none :: some) ∈ S ↔ Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v

Tactic:
apply iff_of_eq

Premises used: iff_of_eq
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
a : ((f v ::ₒ v) ∘ none :: some) = f v :: v
⊢ (((f v ::ₒ v) ∘ none :: some) ∈ S) = Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
a : ∀ (x : Fin2 (n + 1)), ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x
⊢ ((f v ::ₒ v) ∘ none :: some) = f v :: v

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
x : Fin2 (n + 1)
a : ((f v ::ₒ v) ∘ none :: some) fz = (f v :: v) fz
a₁ : ∀ (a : Fin2 n), ((f v ::ₒ v) ∘ none :: some) a.fs = (f v :: v) a.fs
⊢ ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x

Tactic:
cases x
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) fz = (f v :: v) fz

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
a : Fin2 n
⊢ ((f v ::ₒ v) ∘ none :: some) a.fs = (f v :: v) a.fs

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
dsimp : ((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S
⊢ Membership.mem (γ := Set (Option (Fin2 n) → ℕ)) {v : Option (Fin2 n) → ℕ | (v ∘ none :: some) ∈ S} (x ::ₒ v) ↔
    (x :: v) ∈ S

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
s : Fin2 (n + 1)
fz : ((x ::ₒ v) ∘ none :: some) Fin2.fz = (x :: v) Fin2.fz
fs : ∀ (b : Fin2 n), ((x ::ₒ v) ∘ none :: some) b.fs = (x :: v) b.fs
⊢ ((x ::ₒ v) ∘ none :: some) s = (x :: v) s

Tactic:
rcases s with a | b
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ ((x ::ₒ v) ∘ none :: some) fz = (x :: v) fz

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
b : Fin2 n
⊢ ((x ::ₒ v) ∘ none :: some) b.fs = (x :: v) b.fs

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
rw rw₁ : (x :: v) ∈ S ↔ (x :: v) ∈ S
⊢ ((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S

Tactic:
rw [show Option.elim' x v ∘ cons none some = x :: v from
          funext fun s => by rcases s with a | b <;> rfl]

Premises used: funext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
f : Vector3 ℕ n → ℕ
⊢ DiophFn f ↔ Dioph (α := Fin2 (n + 1)) {v : Fin2 (n + 1) → ℕ | f (v ∘ fs) = v fz}

Tactic:
⟨reindex_dioph _ (fz ::ₒ fs), reindex_dioph _ (none::some)⟩

Premises used: Option.elim', Fin2.fz, Option.some, Dioph.reindex_dioph, Fin2.fs, Option.none, Vector3.cons, Iff.intro
-- Module: Mathlib.NumberTheory.Dioph
Goal:
n : ℕ
f : Vector3 ℕ n →. ℕ
⊢ DiophPFun f ↔ Dioph (α := Fin2 (n + 1)) {v : Fin2 (n + 1) → ℕ | (v ∘ fs, v fz) ∈ f.graph}

Tactic:
⟨reindex_dioph _ (fz ::ₒ fs), reindex_dioph _ (none::some)⟩

Premises used: Option.elim', Fin2.fz, Option.some, Dioph.reindex_dioph, Fin2.fs, Option.none, Vector3.cons, Iff.intro
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
h : VectorAllP DiophFn f
v : α → ℕ
dsimp : v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α)) ∈ S ↔ (v ⊗ fun (i : Fin2 0) ↦ f i v) ∈ S
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α)) ∈ S} v ↔
    Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | (v ⊗ fun (i : Fin2 0) ↦ f i v) ∈ S} v

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

Tactic:
congr! 1
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
h : VectorAllP DiophFn f
v : α → ℕ
a : ∀ (x : α ⊕ Fin2 0), (v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α))) x = (v ⊗ fun (i : Fin2 0) ↦ f i v) x
⊢ v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α)) = v ⊗ fun (i : Fin2 0) ↦ f i v

Tactic:
ext x