awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
l : List (Set (α → ℕ))
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
have nil : ∀ (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: induction l with | nil => exact ⟨ULift Empty, [], fun _ => by simp⟩ | cons S l IH =>
  obtain ⟨⟨β, p, pe⟩, dl⟩ := (List.forall_cons _ _ _).mp d
  exact
    let ⟨γ, pl, ple⟩ := IH dl
    ⟨β ⊕ γ, p.map (inl ⊗ inr ∘ inl)::pl.map fun q => q.map (inl ⊗ inr ∘ inr),
      fun v => by
      simpa using
        Iff.trans (and_congr (pe v) (ple v))
          ⟨fun ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ =>
            ⟨m ⊗ n, by
              rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from
                    funext fun s => by rcases s with a | b <;> rfl]; exact hm, by
              refine List.Forall.imp (fun q hq => ?_) hn; dsimp [Function.comp_def]
              rw [show
                    (fun x : α ⊕ γ => (v ⊗ m ⊗ n) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ n
                    from funext fun s => by rcases s with a | b <;> rfl]; exact hq⟩,
            fun ⟨t, hl, hr⟩ =>
            ⟨⟨t ∘ inl, by
                rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
                    funext fun s => by rcases s with a | b <;> rfl] at hl⟩,
              ⟨t ∘ inr, by
                refine List.Forall.imp (fun q hq => ?_) hr; dsimp [Function.comp_def] at hq
                rwa [show
                    (fun x : α ⊕ γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) =
                      v ⊗ t ∘ inr
                    from funext fun s => by rcases s with a | b <;> rfl] at hq ⟩⟩⟩⟩
Cleared hypotheses: l, d
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
l : List (Set (α → ℕ))
d : List.Forall Dioph l
nil :
  ∀ (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
⊢ ∃ (β : 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
have cons : ∀ (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)),
  ∃ (β : 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: induction l with | nil => exact ⟨ULift Empty, [], fun _ => by simp⟩ | cons S l IH =>
  obtain ⟨⟨β, p, pe⟩, dl⟩ := (List.forall_cons _ _ _).mp d
  exact
    let ⟨γ, pl, ple⟩ := IH dl
    ⟨β ⊕ γ, p.map (inl ⊗ inr ∘ inl)::pl.map fun q => q.map (inl ⊗ inr ∘ inr),
      fun v => by
      simpa using
        Iff.trans (and_congr (pe v) (ple v))
          ⟨fun ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ =>
            ⟨m ⊗ n, by
              rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from
                    funext fun s => by rcases s with a | b <;> rfl]; exact hm, by
              refine List.Forall.imp (fun q hq => ?_) hn; dsimp [Function.comp_def]
              rw [show
                    (fun x : α ⊕ γ => (v ⊗ m ⊗ n) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ n
                    from funext fun s => by rcases s with a | b <;> rfl]; exact hq⟩,
            fun ⟨t, hl, hr⟩ =>
            ⟨⟨t ∘ inl, by
                rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
                    funext fun s => by rcases s with a | b <;> rfl] at hl⟩,
              ⟨t ∘ inr, by
                refine List.Forall.imp (fun q hq => ?_) hr; dsimp [Function.comp_def] at hq
                rwa [show
                    (fun x : α ⊕ γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) =
                      v ⊗ t ∘ inr
                    from funext fun s => by rcases s with a | b <;> rfl] at hq ⟩⟩⟩⟩
Cleared hypotheses: l, d
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), v ∈ S' ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
⊢ v ∈ S ∪ S' ↔
    ∃ (t : β ⊕ γ → ℕ),
      Eq (α := ℤ) ((Poly.map (inl ⊗ inr ∘ inl) p * Poly.map (inl ⊗ inr ∘ inr) q : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ)
        (0 : ℤ)
have refine_1 : (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
  ∃ (x : β ⊕ γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ x) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ)
Tactic: refine
        Iff.trans (or_congr ((pe v).trans ?_) ((qe v).trans ?_))
          (exists_or.symm.trans
            (exists_congr fun t =>
              (@mul_eq_zero _ _ _ (p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)))
                  (q ((v ⊗ t) ∘ (inl ⊗ inr ∘ inr)))).symm))
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), v ∈ S' ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
refine_1 :
  (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (x : β ⊕ γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ x) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ)
⊢ v ∈ S ∪ S' ↔
    ∃ (t : β ⊕ γ → ℕ),
      Eq (α := ℤ) ((Poly.map (inl ⊗ inr ∘ inl) p * Poly.map (inl ⊗ inr ∘ inr) q : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ)
        (0 : ℤ)
have refine_2 : (∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
  ∃ (x : β ⊕ γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) ((v ⊗ x) ∘ (inl ⊗ inr ∘ inr)) : ℤ) (0 : ℤ)
Tactic: refine
        Iff.trans (or_congr ((pe v).trans ?_) ((qe v).trans ?_))
          (exists_or.symm.trans
            (exists_congr fun t =>
              (@mul_eq_zero _ _ _ (p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)))
                  (q ((v ⊗ t) ∘ (inl ⊗ inr ∘ inr)))).symm))
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), v ∈ S' ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
⊢ (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (x : β ⊕ γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ x) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ)
have refine_1 : ∀ (x : β), (some ⊗ fun (x : γ) ↦ none) (inl x) = some x
Tactic: refine inject_dummies_lem _ (some ⊗ fun _ => none) ?_ _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), v ∈ S' ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
⊢ (∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (x : β ⊕ γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) ((v ⊗ x) ∘ (inl ⊗ inr ∘ inr)) : ℤ) (0 : ℤ)
have refine_2 : ∀ (x : γ), ((fun (x : β) ↦ none) ⊗ some) (inr x) = some x
Tactic: refine inject_dummies_lem _ ((fun _ => none) ⊗ some) ?_ _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 (α := ℤ) ((Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ x ⊗ t) : ℤ) (0 : ℤ)
have simp : Eq (α := ℤ) ((p : (a : (α ⊕ β) ⊕ γ → ℕ) → ℤ) ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) : ℤ) (0 : ℤ)
Tactic: simp only [Poly.map_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : ℤ)
s : (α ⊕ β) ⊕ γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) s = ((v ⊗ x) ⊗ t) s
have inl : ∀ (a : α ⊕ β), ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : ℤ)
s : (α ⊕ β) ⊕ γ
inl : ∀ (a : α ⊕ β), ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl a) = ((v ⊗ x) ⊗ t) (Sum.inl a)
⊢ ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) s = ((v ⊗ x) ⊗ t) s
have inr : ∀ (b : γ), ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)
have inl : ∀ (val : α), ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val)) = ((v ⊗ x) ⊗ t) (inl (inl val))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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))
⊢ ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl a) = ((v ⊗ x) ⊗ t) (Sum.inl a)
have inl₁ : ∀ (val : β),
  ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl (inr val)) = ((v ⊗ x) ⊗ t) (Sum.inl (inr val))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)
have inl : ∀ (val : α), ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val)) = ((v ⊗ x) ⊗ t) (inl (inl val))
Tactic: { cases a <;> rfl }
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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))
⊢ ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl a) = ((v ⊗ x) ⊗ t) (Sum.inl a)
have inl₁ : ∀ (val : β),
  ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl (inr val)) = ((v ⊗ x) ⊗ t) (Sum.inl (inr val))
Tactic: { cases a <;> rfl }
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)
have inl : ∀ (val : α), ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val)) = ((v ⊗ x) ⊗ t) (inl (inl val))
Tactic: try { cases a <;> rfl }
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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))
⊢ ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl a) = ((v ⊗ x) ⊗ t) (Sum.inl a)
have inl₁ : ∀ (val : β),
  ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl (inr val)) = ((v ⊗ x) ⊗ t) (Sum.inl (inr val))
Tactic: try { cases a <;> rfl }
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : ℤ)
s : (α ⊕ β) ⊕ γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) s = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) s
have inl : ∀ (a : α ⊕ β), ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl a)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : ℤ)
s : (α ⊕ β) ⊕ γ
inl :
  ∀ (a : α ⊕ β),
    ((v ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl a) = ((v ⊗ t ∘ Sum.inl) ⊗ t ∘ inr) (Sum.inl a)
⊢ ((v ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) s = ((v ⊗ t ∘ Sum.inl) ⊗ t ∘ inr) s
have inr : ∀ (b : γ), ((v ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ t ∘ Sum.inl) ⊗ t ∘ inr) (inr b)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : ℤ)
a : α ⊕ β
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl a)
have inl : ∀ (val : α), ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val)) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl (inl val))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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))
⊢ ((v ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl a) = ((v ⊗ t ∘ Sum.inl) ⊗ t ∘ inr) (Sum.inl a)
have 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))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : ℤ)
a : α ⊕ β
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl a)
have inl : ∀ (val : α), ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val)) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl (inl val))
Tactic: { cases a <;> rfl }
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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))
⊢ ((v ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl a) = ((v ⊗ t ∘ Sum.inl) ⊗ t ∘ inr) (Sum.inl a)
have 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))
Tactic: { cases a <;> rfl }
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : ℤ)
a : α ⊕ β
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl a)
have inl : ∀ (val : α), ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val)) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl (inl val))
Tactic: try { cases a <;> rfl }
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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))
⊢ ((v ⊗ t) ∘ ((Sum.inl ⊗ inr ∘ Sum.inl) ⊗ inr ∘ inr)) (Sum.inl a) = ((v ⊗ t ∘ Sum.inl) ⊗ t ∘ inr) (Sum.inl a)
have 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))
Tactic: try { cases a <;> rfl }
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : (α ⊕ β) ⊕ γ → ℕ) → ℤ) ((v ⊗ t ∘ inl) ⊗ t ∘ inr) : ℤ) (0 : ℤ)
have rwa : ∀ (ht : 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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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 (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ x ::ₒ t) : ℤ) (0 : ℤ)
have simp : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
Tactic: simp only [Poly.map_apply]