awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S S' : Set (α → ℕ)
d : Dioph S
H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S'
rwa rwa₁ rwa₂ rwa₃ : Dioph S
⊢ Dioph S'

Tactic:
rwa [← Set.ext H]

Premises used: Set.ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
p : Poly α
h : ∀ (v : α → ℕ), v ∈ S ↔ Eq (α := ℤ) ((p : (a : α → ℕ) → ℤ) v : ℤ) (0 : ℤ)
⊢ Dioph S

Tactic:
⟨PEmpty, ⟨p.map inl, fun v => (h v).trans ⟨fun h => ⟨PEmpty.elim, h⟩, fun ⟨_, ht⟩ => ht⟩⟩⟩

Premises used: Dioph, PEmpty, Sum.inl, PEmpty.elim, _private.0.Dioph.of_no_dummies.match_1, Iff.intro, Exists.intro, Iff.trans, Poly.map, OfNat.ofNat, Eq, DFunLike.coe
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
dsimp :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
⊢ (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((Poly.map (inl ⊗ inr ∘ f) p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
⊢ (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)

Tactic:
⟨fun t => ?_, fun t => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
refine_1 :
  ∀ (t : ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)),
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
refine_2 :
  ∀ (t : ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)),
    ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
⊢ (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)

Tactic:
refine ⟨fun t => ?_, fun t => ?_⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
refine_1 :
  ∀ (t : β → ℕ) (ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)),
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
⊢ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)

Tactic:
obtain ⟨t, ht⟩ := t
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
refine_2 :
  ∀ (t : γ → ℕ) (ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)),
    ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
⊢ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)

Tactic:
obtain ⟨t, ht⟩ := t
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
s : α ⊕ β
inl : ∀ (a : α), ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (Sum.inl ⊗ Sum.inr ∘ f)) (Sum.inl a) = (v ⊗ t) (Sum.inl a)
inr : ∀ (b : β), ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (Sum.inl ⊗ Sum.inr ∘ f)) (Sum.inr b) = (v ⊗ t) (Sum.inr b)
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (Sum.inl ⊗ Sum.inr ∘ f)) s = (v ⊗ t) s

Tactic:
rcases s with a | b
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
a : α
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inl a) = (v ⊗ t) (inl a)

Tactic:
dsimp [(· ∘ ·)]

Premises used: Function.comp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
b : β
inr : (0 ::ₒ t) (g (f b)) = t b
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ Sum.inr ∘ f)) (Sum.inr b) = (v ⊗ t) (Sum.inr b)

Tactic:
dsimp [(· ∘ ·)]

Premises used: Function.comp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
b : β
inr : (0 ::ₒ t) (some b) = t b
⊢ (0 ::ₒ t) (g (f b)) = t b

Tactic:
rw [inv]
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
b : β
⊢ (0 ::ₒ t) (some b) = t b

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
b : β
inr inr₁ inr₂ inr₃ : (0 ::ₒ t) (some b) = t b
⊢ (0 ::ₒ t) (g (f b)) = t b

Tactic:
try rw [inv]; rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
⊢ (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t

Tactic:
have : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t :=
      funext fun s => by rcases s with a | b <;> dsimp [(· ∘ ·)]; try rw [inv]; rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
this : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t
rwa rwa₁ rwa₂ rwa₃ : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)

Tactic:
rwa [this]
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
this : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t
⊢ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)

Tactic:
exact ⟨(0 ::ₒ t) ∘ g, by rwa [this]⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (Sum.inl ⊗ Sum.inr ∘ f)) : ℤ) (0 : ℤ)
s : α ⊕ β
inl : ∀ (a : α), (v ⊗ t ∘ f) (Sum.inl a) = ((v ⊗ t) ∘ (Sum.inl ⊗ Sum.inr ∘ f)) (Sum.inl a)
inr : ∀ (b : β), (v ⊗ t ∘ f) (Sum.inr b) = ((v ⊗ t) ∘ (Sum.inl ⊗ Sum.inr ∘ f)) (Sum.inr b)
⊢ (v ⊗ t ∘ f) s = ((v ⊗ t) ∘ (Sum.inl ⊗ Sum.inr ∘ f)) s

Tactic:
rcases s with a | b
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
a : α
⊢ (v ⊗ t ∘ f) (inl a) = ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) (inl a)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
b : β
⊢ (v ⊗ t ∘ f) (inr b) = ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) (inr b)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
⊢ v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f)

Tactic:
have : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f) := funext fun s => by rcases s with a | b <;> rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
this : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f)
rwa rwa₁ rwa₂ rwa₃ : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t ∘ f) : ℤ) (0 : ℤ)

Tactic:
rwa [this]
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
this : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f)
⊢ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)

Tactic:
exact ⟨t ∘ f, by rwa [this]⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β γ : Type u
S : Set (α → ℕ)
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
h : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
⊢ ∃ (q : Poly (α ⊕ γ)),
    ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)

Tactic:
⟨p.map (inl ⊗ inr ∘ f), fun v => (h v).trans <| inject_dummies_lem f g inv _ _⟩

Premises used: Dioph.inject_dummies_lem, Function.comp, Sum.inl, Sum.inr, Exists.intro, Iff.trans, Poly.map, Sum.elim
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : β → ℕ
t : γ → ℕ
s : α ⊕ γ
inl : ∀ (a : α), (v ∘ f ⊗ t) (Sum.inl a) = ((v ⊗ t) ∘ (Sum.inl ∘ f ⊗ Sum.inr)) (Sum.inl a)
inr : ∀ (b : γ), (v ∘ f ⊗ t) (Sum.inr b) = ((v ⊗ t) ∘ (Sum.inl ∘ f ⊗ Sum.inr)) (Sum.inr b)
⊢ (v ∘ f ⊗ t) s = ((v ⊗ t) ∘ (Sum.inl ∘ f ⊗ Sum.inr)) s

Tactic:
rcases s with a | b
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : β → ℕ
t : γ → ℕ
a : α
⊢ (v ∘ f ⊗ t) (inl a) = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) (inl a)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : β → ℕ
t : γ → ℕ
b : γ
⊢ (v ∘ f ⊗ t) (inr b) = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) (inr b)

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

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
l : List (Set (α → ℕ))
d : List.Forall Dioph l
suffices :
  ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
    ∀ (v : α → ℕ),
      List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
        ∃ (t : β → ℕ),
          List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
⊢ Dioph.{u} (α := α) {v : α → ℕ | List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l}

Tactic:
suffices ∃ (β : _) (pl : List (Poly (α ⊕ β))), ∀ v, List.Forall (fun S : Set _ => v ∈ S) l ↔
          ∃ t, List.Forall (fun p : Poly (α ⊕ β) => p (v ⊗ t) = 0) pl
    from
    let ⟨β, pl, h⟩ := this
    ⟨β, Poly.sumsq pl, fun v => (h v).trans <| exists_congr fun t => (Poly.sumsq_eq_zero _ _).symm⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
d : List.Forall.{u} (α := Set (α → ℕ)) Dioph []
x : α → ℕ
⊢ List.Forall (fun (S : Set (α → ℕ)) ↦ x ∈ S) [] ↔
    ∃ (t : ULift.{u, 0} Empty → ℕ),
      List.Forall
        (fun (p : Poly (α ⊕ ULift.{u, 0} Empty)) ↦
          Eq (α := ℤ) ((p : (a : α ⊕ ULift.{u, 0} Empty → ℕ) → ℤ) (x ⊗ t) : ℤ) (0 : ℤ))
        []

Tactic:
simp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
d : List.Forall.{u} (α := Set (α → ℕ)) Dioph []
⊢ ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
    ∀ (v : α → ℕ),
      List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) [] ↔
        ∃ (t : β → ℕ),
          List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl

Tactic:
exact ⟨ULift Empty, [], fun _ => by simp⟩
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  ∀ (d : List.Forall Dioph l),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
d : List.Forall Dioph (S :: l)
cons :
  ∀ (dl : List.Forall Dioph l) (β : Type u) (p : Poly (α ⊕ β))
    (pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) (S :: l) ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
⊢ ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
    ∀ (v : α → ℕ),
      List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) (S :: l) ↔
        ∃ (t : β → ℕ),
          List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl

Tactic:
obtain ⟨⟨β, p, pe⟩, dl⟩ := (List.forall_cons _ _ _).mp d

Premises used: List.forall_cons, Iff.mp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  ∀ (d : List.Forall Dioph l),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
pl : List (Poly (α ⊕ γ))
ple :
  ∀ (v : α → ℕ),
    List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
      ∃ (t : γ → ℕ),
        List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
v : α → ℕ
h :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∧
    ∃ (t : γ → ℕ), List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
m : β → ℕ
hm : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)
n : γ → ℕ
hn : List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)) pl
s : α ⊕ β
inl : ∀ (a : α), ((v ⊗ m ⊗ n) ∘ (Sum.inl ⊗ Sum.inr ∘ Sum.inl)) (Sum.inl a) = (v ⊗ m) (Sum.inl a)
inr : ∀ (b : β), ((v ⊗ m ⊗ n) ∘ (Sum.inl ⊗ Sum.inr ∘ Sum.inl)) (Sum.inr b) = (v ⊗ m) (Sum.inr b)
⊢ ((v ⊗ m ⊗ n) ∘ (Sum.inl ⊗ Sum.inr ∘ Sum.inl)) s = (v ⊗ m) s

Tactic:
rcases s with a | b
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  ∀ (d : List.Forall Dioph l),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
pl : List (Poly (α ⊕ γ))
ple :
  ∀ (v : α → ℕ),
    List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
      ∃ (t : γ → ℕ),
        List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
v : α → ℕ
h :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∧
    ∃ (t : γ → ℕ), List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
m : β → ℕ
hm : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)
n : γ → ℕ
hn : List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)) pl
a : α
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) (inl a) = (v ⊗ m) (inl a)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  ∀ (d : List.Forall Dioph l),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
pl : List (Poly (α ⊕ γ))
ple :
  ∀ (v : α → ℕ),
    List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
      ∃ (t : γ → ℕ),
        List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
v : α → ℕ
h :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∧
    ∃ (t : γ → ℕ), List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
m : β → ℕ
hm : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)
n : γ → ℕ
hn : List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)) pl
b : β
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) (inr b) = (v ⊗ m) (inr b)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  ∀ (d : List.Forall Dioph l),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
pl : List (Poly (α ⊕ γ))
ple :
  ∀ (v : α → ℕ),
    List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
      ∃ (t : γ → ℕ),
        List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
v : α → ℕ
h :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∧
    ∃ (t : γ → ℕ), List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
m : β → ℕ
hm : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)
n : γ → ℕ
hn : List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)) pl
rw : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ)

Tactic:
rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from
                    funext fun s => by rcases s with a | b <;> rfl]

Premises used: funext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  ∀ (d : List.Forall Dioph l),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
pl : List (Poly (α ⊕ γ))
ple :
  ∀ (v : α → ℕ),
    List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
      ∃ (t : γ → ℕ),
        List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
v : α → ℕ
h :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∧
    ∃ (t : γ → ℕ), List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
m : β → ℕ
hm : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)
n : γ → ℕ
hn : List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)) pl
⊢ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)

Tactic:
hm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  ∀ (d : List.Forall Dioph l),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
pl : List (Poly (α ⊕ γ))
ple :
  ∀ (v : α → ℕ),
    List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
      ∃ (t : γ → ℕ),
        List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
v : α → ℕ
h :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∧
    ∃ (t : γ → ℕ), List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
m : β → ℕ
hm : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)
n : γ → ℕ
hn : List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)) pl
⊢ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)

Tactic:
exact hm
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  ∀ (d : List.Forall Dioph l),
    ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
      ∀ (v : α → ℕ),
        List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
          ∃ (t : β → ℕ),
            List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
pl : List (Poly (α ⊕ γ))
ple :
  ∀ (v : α → ℕ),
    List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
      ∃ (t : γ → ℕ),
        List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
v : α → ℕ
h :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∧
    ∃ (t : γ → ℕ), List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
m : β → ℕ
hm : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ m) : ℤ) (0 : ℤ)
n : γ → ℕ
hn : List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)) pl
⊢ List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ m ⊗ n) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
    pl

Tactic:
List.Forall.imp (fun q hq => ?_) hn

Premises used: List.Forall.imp