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) : ℤ) (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
refine :
  ∀ (q : Poly (α ⊕ γ)) (hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)),
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ m ⊗ n) : ℤ) (0 : ℤ)) ∘
        fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
      q
⊢ List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ m ⊗ n) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
    pl

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

Premises used: List.Forall.imp
-- 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
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)
dsimp :
  Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) fun (x : α ⊕ γ) ↦ (v ⊗ m ⊗ n) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) x) : ℤ)
    (0 : ℤ)
⊢ ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ m ⊗ n) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
    q

Tactic:
dsimp [Function.comp_def]

Premises used: Function.comp_def
-- 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
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)
s : α ⊕ γ
inl : ∀ (a : α), (v ⊗ m ⊗ n) ((Sum.inl ⊗ fun (x : γ) ↦ Sum.inr (Sum.inr x)) (Sum.inl a)) = (v ⊗ n) (Sum.inl a)
inr : ∀ (b : γ), (v ⊗ m ⊗ n) ((Sum.inl ⊗ fun (x : γ) ↦ Sum.inr (Sum.inr x)) (Sum.inr b)) = (v ⊗ n) (Sum.inr b)
⊢ (v ⊗ m ⊗ n) ((Sum.inl ⊗ fun (x : γ) ↦ Sum.inr (Sum.inr x)) s) = (v ⊗ n) 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
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)
a : α
⊢ (v ⊗ m ⊗ n) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) (inl a)) = (v ⊗ n) (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
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)
b : γ
⊢ (v ⊗ m ⊗ n) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) (inr b)) = (v ⊗ n) (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
q : Poly (α ⊕ γ)
hq rw : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) fun (x : α ⊕ γ) ↦ (v ⊗ m ⊗ n) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) x) : ℤ)
    (0 : ℤ)

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

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
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)

Tactic:
hq
-- 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
q : Poly (α ⊕ γ)
hq : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ n) : ℤ) (0 : ℤ)

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

Tactic:
rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
                    funext fun s => by rcases s with a | b <;> rfl] at hl

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) ∘ (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
⊢ List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t ∘ inr) : ℤ) (0 : ℤ)) pl

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

Premises used: List.Forall.imp
-- 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
refine :
  ∀ (q : Poly (α ⊕ γ))
    (hq :
      ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
          fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
        q),
    Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t ∘ inr) : ℤ) (0 : ℤ)
⊢ List.Forall (fun (p : Poly (α ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t ∘ inr) : ℤ) (0 : ℤ)) pl

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

Premises used: List.Forall.imp