awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ∘ (Sum.inl ⊗ Sum.inr ∘ Sum.inl)) : ℤ) (0 : ℤ) ∧
      List.Forall
        ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
          fun (q : Poly (α ⊕ γ)) ↦ Poly.map (Sum.inl ⊗ Sum.inr ∘ Sum.inr) q)
        pl
t : β ⊕ γ → ℕ
hl : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (Sum.inl ⊗ Sum.inr ∘ Sum.inl)) : ℤ) (0 : ℤ)
hr :
  List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (Sum.inl ⊗ Sum.inr ∘ Sum.inr) q)
    pl
q : Poly (α ⊕ γ)
hq :
  Eq (α := ℤ)
    ((q : (a : α ⊕ γ → ℕ) → ℤ) fun (x : α ⊕ γ) ↦ (v ⊗ t) ((Sum.inl ⊗ fun (x : γ) ↦ Sum.inr (Sum.inr x)) x) : ℤ) (0 : ℤ)
s : α ⊕ γ
inl : ∀ (a : α), (v ⊗ t) ((Sum.inl ⊗ fun (x : γ) ↦ Sum.inr (Sum.inr x)) (Sum.inl a)) = (v ⊗ t ∘ Sum.inr) (Sum.inl a)
inr : ∀ (b : γ), (v ⊗ t) ((Sum.inl ⊗ fun (x : γ) ↦ Sum.inr (Sum.inr x)) (Sum.inr b)) = (v ⊗ t ∘ Sum.inr) (Sum.inr b)
⊢ (v ⊗ t) ((Sum.inl ⊗ fun (x : γ) ↦ Sum.inr (Sum.inr x)) s) = (v ⊗ t ∘ Sum.inr) 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) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ) ∧
      List.Forall
        ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
          fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
        pl
t : β ⊕ γ → ℕ
hl : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ)
hr :
  List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
    pl
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) fun (x : α ⊕ γ) ↦ (v ⊗ t) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) x) : ℤ) (0 : ℤ)
a : α
⊢ (v ⊗ t) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) (inl a)) = (v ⊗ t ∘ inr) (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) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ) ∧
      List.Forall
        ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
          fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
        pl
t : β ⊕ γ → ℕ
hl : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ)
hr :
  List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
    pl
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) fun (x : α ⊕ γ) ↦ (v ⊗ t) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) x) : ℤ) (0 : ℤ)
b : γ
⊢ (v ⊗ t) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) (inr b)) = (v ⊗ t ∘ inr) (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) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ) ∧
      List.Forall
        ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
          fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
        pl
t : β ⊕ γ → ℕ
hl : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ)
hr :
  List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
    pl
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) fun (x : α ⊕ γ) ↦ (v ⊗ t) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) x) : ℤ) (0 : ℤ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t ∘ inr) : ℤ) (0 : ℤ)),
    Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t ∘ inr) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t ∘ inr) : ℤ) (0 : ℤ)

Tactic:
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

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 : α → ℕ
⊢ List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) (S :: l) ↔
    ∃ (t : β ⊕ γ → ℕ),
      List.Forall (fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ))
        (Poly.map (inl ⊗ inr ∘ inl) p :: List.map (fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl)

Tactic:
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 ⟩⟩⟩

Premises used: Iff.intro, Iff.trans, and_congr
-- 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 (α ⊕ β))),
    ∀ (v : α → ℕ),
      List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) (S :: l) ↔
        ∃ (t : β → ℕ),
          List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl

Tactic:
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 ⟩⟩⟩⟩
-- Module: Mathlib.NumberTheory.Dioph
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
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
⊢ ∃ (β : 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

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 ⟩⟩⟩⟩

Premises used: List.forall_cons, Iff.mp
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u
S S' : Set (α → ℕ)
d : Dioph S
d' : Dioph S'
⊢ Dioph (S ∩ S')

Tactic:
DiophList.forall [S, S'] ⟨d, d'⟩

Premises used: setOf, Set.inter, List.cons, List.Forall, And.intro, Dioph.DiophList.forall, List.nil
-- Module: Mathlib.NumberTheory.Dioph
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 : ℤ)

Tactic:
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))

Premises used: or_congr, exists_or, mul_eq_zero, exists_congr, Iff.trans, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
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 : ℤ)
refine_2 :
  (∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (x : β ⊕ γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) ((v ⊗ x) ∘ (inl ⊗ inr ∘ inr)) : ℤ) (0 : ℤ)
⊢ v ∈ S ∪ S' ↔
    ∃ (t : β ⊕ γ → ℕ),
      Eq (α := ℤ) ((Poly.map (inl ⊗ inr ∘ inl) p * Poly.map (inl ⊗ inr ∘ inr) q : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ)
        (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))

Premises used: or_congr, exists_or, mul_eq_zero, exists_congr, Iff.trans, Iff.symm
-- Module: Mathlib.NumberTheory.Dioph
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 : ℤ)

Tactic:
inject_dummies_lem _ (some ⊗ fun _ => none) ?_ _ _

Premises used: Option.some, Dioph.inject_dummies_lem, Option.none, Sum.elim
-- Module: Mathlib.NumberTheory.Dioph
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 : ∀ (x : β), (some ⊗ fun (x : γ) ↦ none) (inl x) = some x
⊢ (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (x : β ⊕ γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ x) ∘ (inl ⊗ inr ∘ inl)) : ℤ) (0 : ℤ)

Tactic:
refine inject_dummies_lem _ (some ⊗ fun _ => none) ?_ _ _

Premises used: Option.some, Dioph.inject_dummies_lem, Option.none, Sum.elim
-- Module: Mathlib.NumberTheory.Dioph
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 : α → ℕ
x : β
⊢ (some ⊗ fun (x : γ) ↦ none) (inl x) = some x

Tactic:
simp only [elim_inl]

Premises used: Sum.elim_inl
-- Module: Mathlib.NumberTheory.Dioph
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 : α → ℕ
⊢ ∀ (x : β), (some ⊗ fun (x : γ) ↦ none) (inl x) = some x

Tactic:
exact fun _ => by simp only [elim_inl]
-- Module: Mathlib.NumberTheory.Dioph
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 : ℤ)

Tactic:
inject_dummies_lem _ ((fun _ => none) ⊗ some) ?_ _ _

Premises used: Option.some, Dioph.inject_dummies_lem, Option.none, Sum.elim
-- Module: Mathlib.NumberTheory.Dioph
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_2 : ∀ (x : γ), ((fun (x : β) ↦ none) ⊗ some) (inr x) = some x
⊢ (∃ (t : γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (x : β ⊕ γ → ℕ), Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) ((v ⊗ x) ∘ (inl ⊗ inr ∘ inr)) : ℤ) (0 : ℤ)

Tactic:
refine inject_dummies_lem _ ((fun _ => none) ⊗ some) ?_ _ _

Premises used: Option.some, Dioph.inject_dummies_lem, Option.none, Sum.elim
-- Module: Mathlib.NumberTheory.Dioph
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 : α → ℕ
x : γ
⊢ ((fun (x : β) ↦ none) ⊗ some) (inr x) = some x

Tactic:
simp only [elim_inr]

Premises used: Sum.elim_inr
-- Module: Mathlib.NumberTheory.Dioph
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 : α → ℕ
⊢ ∀ (x : γ), ((fun (x : β) ↦ none) ⊗ some) (inr x) = some x

Tactic:
exact fun _ => by simp only [elim_inr]
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β : Type u
f : (α → ℕ) → ℕ
g : α → β
d : DiophFn f
⊢ Dioph.{u} (α := Option β)
    {v : Option β → ℕ |
      Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | f (v ∘ some) = v none} (v ∘ Option.map g)}

Tactic:
reindex_dioph (Option β) (Option.map g) d

Premises used: Dioph.reindex_dioph, Option.map, Option
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α β : Type u
f : (α → ℕ) → ℕ
g : α → β
d : DiophFn f
⊢ DiophFn.{u} (α := β) fun (v : β → ℕ) ↦ f (v ∘ g)

Tactic:
convert! reindex_dioph (Option β) (Option.map g) d

Premises used: Dioph.reindex_dioph, Option.map, Option
-- 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 : ℤ)
simp : Eq (α := ℤ) ((p : (a : (α ⊕ β) ⊕ γ → ℕ) → ℤ) ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ x ⊗ t) : ℤ) (0 : ℤ)

Tactic:
simp only [Poly.map_apply]

Premises used: Poly.map_apply
-- 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 : ℤ)
s : (α ⊕ β) ⊕ γ
inl :
  ∀ (a : α ⊕ β),
    ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ Sum.inr ∘ Sum.inl) ⊗ Sum.inr ∘ Sum.inr)) (Sum.inl a) = ((v ⊗ x) ⊗ t) (Sum.inl a)
inr :
  ∀ (b : γ), ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ Sum.inr ∘ Sum.inl) ⊗ Sum.inr ∘ Sum.inr)) (Sum.inr b) = ((v ⊗ x) ⊗ t) (Sum.inr b)
⊢ ((v ⊗ x ⊗ t) ∘ ((Sum.inl ⊗ Sum.inr ∘ Sum.inl) ⊗ Sum.inr ∘ Sum.inr)) s = ((v ⊗ x) ⊗ t) s

Tactic:
rcases s with a | b