awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HAdd.hAdd (α := ℤ) (β := ℤ) ((-x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((-x + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₁ : HAdd.hAdd (α := ℤ) (β := ℤ) (-(x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (0 : (a : α → ℕ) → ℤ) x_1
Tactic: simp_rw [add_apply, neg_apply, neg_add_cancel, zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HAdd.hAdd (α := ℤ) (β := ℤ) ((-x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
a₁ :
  HAdd.hAdd (α := ℤ) (β := ℤ) (-(x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((-x + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₂ : Eq (α := ℤ) (0 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: simp_rw [add_apply, neg_apply, neg_add_cancel, zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x x_1 : Poly α
⊢ x + x_1 = x_1 + x
have a : ∀ (x_2 : α → ℕ), Eq (α := ℤ) ((x + x_1 : (a : α → ℕ) → ℤ) x_2 : ℤ) ((x_1 + x : (a : α → ℕ) → ℤ) x_2 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have a : ∀ (x_3 : α → ℕ), Eq (α := ℤ) ((x * x_1 * x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x * (x_1 * x_2) : (a : α → ℕ) → ℤ) x_3 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
⊢ 1 * x = x
have a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((1 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
⊢ Eq (α := ℤ) ((1 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a : HMul.hMul (α := ℤ) (β := ℤ) ((1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
Tactic: rw [mul_apply, one_apply, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((1 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₁ : HMul.hMul (α := ℤ) (β := ℤ) (1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
Tactic: rw [mul_apply, one_apply, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
a₁ : HMul.hMul (α := ℤ) (β := ℤ) (1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((1 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₂ : Eq (α := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: rw [mul_apply, one_apply, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
⊢ x * 1 = x
have a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((x * 1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
⊢ Eq (α := ℤ) ((x * 1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a : HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((1 : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
Tactic: rw [mul_apply, one_apply, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((1 : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((x * 1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₁ : HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) (1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
Tactic: rw [mul_apply, one_apply, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((1 : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
a₁ : HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) (1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((x * 1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₂ : Eq (α := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: rw [mul_apply, one_apply, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
⊢ 0 * x = 0
have a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((0 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
⊢ Eq (α := ℤ) ((0 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a : HMul.hMul (α := ℤ) (β := ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (0 : (a : α → ℕ) → ℤ) x_1
Tactic: rw [mul_apply, zero_apply, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((0 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₁ : HMul.hMul (α := ℤ) (β := ℤ) (0 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = 0
Tactic: rw [mul_apply, zero_apply, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
a₁ : HMul.hMul (α := ℤ) (β := ℤ) (0 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = 0
⊢ Eq (α := ℤ) ((0 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₂ : Eq (α := ℤ) 0 0
Tactic: rw [mul_apply, zero_apply, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
⊢ x * 0 = 0
have a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((x * 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
⊢ Eq (α := ℤ) ((x * 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a : HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) = (0 : (a : α → ℕ) → ℤ) x_1
Tactic: rw [mul_apply, zero_apply, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((x * 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₁ : HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) (0 : ℤ) = 0
Tactic: rw [mul_apply, zero_apply, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
a₁ : HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) (0 : ℤ) = 0
⊢ Eq (α := ℤ) ((x * 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₂ : Eq (α := ℤ) 0 0
Tactic: rw [mul_apply, zero_apply, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
⊢ x * (x_1 + x_2) = x * x_1 + x * x_2
have a : ∀ (x_3 : α → ℕ),
  Eq (α := ℤ) ((x * (x_1 + x_2) : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x * x_1 + x * x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2
have a : ∀ (x_3 : α → ℕ),
  Eq (α := ℤ) (((x + x_1) * x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x * x_2 + x_1 * x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x x_1 : Poly α
⊢ x * x_1 = x_1 * x
have a : ∀ (x_2 : α → ℕ), Eq (α := ℤ) ((x * x_1 : (a : α → ℕ) → ℤ) x_2 : ℤ) ((x_1 * x : (a : α → ℕ) → ℤ) x_2 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : Poly α
⊢ C f
have obtain : ∀ (f : (α → ℕ) → ℤ) (pf : IsPoly f), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f pf)
Tactic: obtain ⟨f, pf⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f pf)
have proj : ∀ (i : α), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ (↑(x i) : ℤ)) sorry)
Tactic: induction pf with
  | proj => apply H1
  | const => apply H2
  | sub _ _ ihf ihg => apply H3 _ _ ihf ihg
  | mul _ _ ihf ihg => apply H4 _ _ ihf ihg
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (Poly.proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
proj : ∀ (i : α), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ (↑(x i) : ℤ)) ⋯)
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f pf)
have const : ∀ (n : ℤ), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ n) sorry)
Tactic: induction pf with
  | proj => apply H1
  | const => apply H2
  | sub _ _ ihf ihg => apply H3 _ _ ihf ihg
  | mul _ _ ihf ihg => apply H4 _ _ ihf ihg
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (Poly.proj i)
H2 : ∀ (n : ℤ), C (Poly.const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
proj : ∀ (i : α), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ (↑(x i) : ℤ)) ⋯)
const : ∀ (n : ℤ), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ n) ⋯)
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f pf)
have sub : ∀ {f g : (α → ℕ) → ℤ} (a : IsPoly f) (a_1 : IsPoly g) (ihf : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f a))
  (ihg : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) g a_1)),
  C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ f x - g x) sorry)
Tactic: induction pf with
  | proj => apply H1
  | const => apply H2
  | sub _ _ ihf ihg => apply H3 _ _ ihf ihg
  | mul _ _ ihf ihg => apply H4 _ _ ihf ihg
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (Poly.proj i)
H2 : ∀ (n : ℤ), C (Poly.const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
proj : ∀ (i : α), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ (↑(x i) : ℤ)) ⋯)
const : ∀ (n : ℤ), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ n) ⋯)
sub :
  ∀ {f g : (α → ℕ) → ℤ} (a : IsPoly f) (a_1 : IsPoly g)
    (ihf : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f a))
    (ihg : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) g a_1)),
    C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ f x - g x) ⋯)
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f pf)
have mul : ∀ {f g : (α → ℕ) → ℤ} (a : IsPoly f) (a_1 : IsPoly g) (ihf : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f a))
  (ihg : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) g a_1)),
  C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ f x * g x) sorry)
Tactic: induction pf with
  | proj => apply H1
  | const => apply H2
  | sub _ _ ihf ihg => apply H3 _ _ ihf ihg
  | mul _ _ ihf ihg => apply H4 _ _ ihf ihg
Cleared hypotheses: pf
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
⊢ (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((Poly.map (inl ⊗ inr ∘ f) p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
have dsimp : (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
  ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
⊢ (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
have refine_1 : ∀ (t : ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)),
  ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
Tactic: refine ⟨fun t => ?_, fun t => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
refine_1 :
  ∀ (t : ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)),
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
⊢ (∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ↔
    ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
have refine_2 : ∀ (t : ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)),
  ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
Tactic: refine ⟨fun t => ?_, fun t => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
⊢ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
have refine_1 : ∀ (t : β → ℕ) (ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)),
  ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
Tactic: obtain ⟨t, ht⟩ := t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
⊢ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
have refine_2 : ∀ (t : γ → ℕ) (ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)),
  ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
Tactic: obtain ⟨t, ht⟩ := t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
s : α ⊕ β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) s = (v ⊗ t) s
have inl : ∀ (a : α), ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inl a) = (v ⊗ t) (inl a)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
s : α ⊕ β
inl : ∀ (a : α), ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (Sum.inl ⊗ inr ∘ f)) (Sum.inl a) = (v ⊗ t) (Sum.inl a)
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (Sum.inl ⊗ inr ∘ f)) s = (v ⊗ t) s
have inr : ∀ (b : β), ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (Sum.inl ⊗ inr ∘ f)) (inr b) = (v ⊗ t) (inr b)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
b : β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inr b) = (v ⊗ t) (inr b)
have inr : (0 ::ₒ t) (g (f b)) = t b
Tactic: dsimp [(· ∘ ·)]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
b : β
⊢ (0 ::ₒ t) (g (f b)) = t b
have inr : (0 ::ₒ t) (some b) = t b
Tactic: rw [inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
b : β
⊢ (0 ::ₒ t) (g (f b)) = t b
have inr : (0 ::ₒ t) (some b) = t b
Tactic: try rw [inv]; rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (hypothesis)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
⊢ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
have this : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t
Tactic: have : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t :=
      funext fun s => by rcases s with a | b <;> dsimp [(· ∘ ·)]; try rw [inv]; rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
s : α ⊕ β
⊢ (v ⊗ t ∘ f) s = ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) s
have inl : ∀ (a : α), (v ⊗ t ∘ f) (inl a) = ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) (inl a)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
s : α ⊕ β
inl : ∀ (a : α), (v ⊗ t ∘ f) (Sum.inl a) = ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ f)) (Sum.inl a)
⊢ (v ⊗ t ∘ f) s = ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ f)) s
have inr : ∀ (b : β), (v ⊗ t ∘ f) (inr b) = ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ f)) (inr b)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (hypothesis)
Goal:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) : ℤ) (0 : ℤ)
⊢ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
have this : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f)
Tactic: have : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f) := funext fun s => by rcases s with a | b <;> rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : β → ℕ
t : γ → ℕ
s : α ⊕ γ
⊢ (v ∘ f ⊗ t) s = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) s
have inl : ∀ (a : α), (v ∘ f ⊗ t) (inl a) = ((v ⊗ t) ∘ (inl ∘ f ⊗ 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 (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : γ → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : β → ℕ
t : γ → ℕ
s : α ⊕ γ
inl : ∀ (a : α), (v ∘ f ⊗ t) (Sum.inl a) = ((v ⊗ t) ∘ (Sum.inl ∘ f ⊗ inr)) (Sum.inl a)
⊢ (v ∘ f ⊗ t) s = ((v ⊗ t) ∘ (Sum.inl ∘ f ⊗ inr)) s
have inr : ∀ (b : γ), (v ∘ f ⊗ t) (inr b) = ((v ⊗ t) ∘ (Sum.inl ∘ f ⊗ inr)) (inr b)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
l : List (Set (α → ℕ))
d : List.Forall Dioph l
⊢ Dioph.{u} (α := α) {v : α → ℕ | List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l}
have suffices : ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
  ∀ (v : α → ℕ),
    List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) l ↔
      ∃ (t : β → ℕ),
        List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
Tactic: suffices ∃ (β : _) (pl : List (Poly (α ⊕ β))), ∀ v, List.Forall (fun S : Set _ => v ∈ S) l ↔
          ∃ t, List.Forall (fun p : Poly (α ⊕ β) => p (v ⊗ t) = 0) pl
    from
    let ⟨β, pl, h⟩ := this
    ⟨β, Poly.sumsq pl, fun v => (h v).trans <| exists_congr fun t => (Poly.sumsq_eq_zero _ _).symm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
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)
⊢ ∃ (β : 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
have cons : ∀ (dl : List.Forall Dioph l) (β : Type u) (p : Poly (α ⊕ β))
  (pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)),
  ∃ (β : Type u) (pl : List (Poly (α ⊕ β))),
    ∀ (v : α → ℕ),
      List.Forall (fun (S : Set (α → ℕ)) ↦ v ∈ S) (S :: l) ↔
        ∃ (t : β → ℕ),
          List.Forall (fun (p : Poly (α ⊕ β)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) pl
Tactic: obtain ⟨⟨β, p, pe⟩, dl⟩ := (List.forall_cons _ _ _).mp d