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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
rwa [show (v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ t ∘ inl) ⊗ t ∘ inr 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
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 : ℤ)
simp : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ x ::ₒ t) : ℤ) (0 : ℤ)

Tactic:
simp only [Poly.map_apply]

Premises used: Poly.map_apply
-- 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 : ℤ)
s : Option α ⊕ β
inl :
  ∀ (a : Option α),
    ((v ⊗ x ::ₒ t) ∘ (Sum.inr none ::ₒ Sum.inl ⊗ Sum.inr ∘ some)) (Sum.inl a) = (x ::ₒ v ⊗ t) (Sum.inl a)
inr : ∀ (b : β), ((v ⊗ x ::ₒ t) ∘ (Sum.inr none ::ₒ Sum.inl ⊗ Sum.inr ∘ some)) (Sum.inr b) = (x ::ₒ v ⊗ t) (Sum.inr b)
⊢ ((v ⊗ x ::ₒ t) ∘ (Sum.inr none ::ₒ Sum.inl ⊗ Sum.inr ∘ some)) s = (x ::ₒ v ⊗ t) 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 : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₁ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (x ::ₒ v ⊗ t) (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 : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (x ::ₒ v ⊗ t) (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 : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
val : α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl (some val)) = (x ::ₒ v ⊗ t) (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 : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₁ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
inl₂ : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₃ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
inl₄ : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₅ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
inl₆ : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₇ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (x ::ₒ v ⊗ t) (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 : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₁ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
inl₂ : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₃ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
inl₄ : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₅ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
inl₆ : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
inl₇ :
  ∀ (val : α),
    ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (x ::ₒ v ⊗ t) (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 : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
b : β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (x ::ₒ v ⊗ t) (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 : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht rw : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)

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

Premises used: funext