awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ)
s : Option α ⊕ β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) s = (x ::ₒ v ⊗ t) s
have inl : ∀ (a : Option α), ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (x ::ₒ 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
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
s : Option α ⊕ β
inl : ∀ (a : Option α), ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (x ::ₒ v ⊗ t) (Sum.inl a)
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) s = (x ::ₒ v ⊗ t) s
have inr : ∀ (b : β), ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (inr b) = (x ::ₒ 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
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (x ::ₒ v ⊗ t) : ℤ) (0 : ℤ)
a : Option α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (x ::ₒ v ⊗ t) (inl a)
have inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (x ::ₒ v ⊗ t) (inl none)
Tactic: cases a
Cleared hypotheses: a
-- 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 : ℤ)
a : Option α
inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (x ::ₒ v ⊗ t) (Sum.inl a)
have inl₁ : ∀ (val : α),
  ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
Tactic: cases a
Cleared hypotheses: a
-- 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 : ℤ)
a : Option α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (x ::ₒ v ⊗ t) (inl a)
have inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (x ::ₒ v ⊗ t) (inl none)
Tactic: { cases a <;> rfl}
Cleared hypotheses: a
-- 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 : ℤ)
a : Option α
inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (x ::ₒ v ⊗ t) (Sum.inl a)
have inl₁ : ∀ (val : α),
  ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
Tactic: { cases a <;> rfl}
Cleared hypotheses: a
-- 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 : ℤ)
a : Option α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (x ::ₒ v ⊗ t) (inl a)
have inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (x ::ₒ v ⊗ t) (inl none)
Tactic: try { cases a <;> rfl}
Cleared hypotheses: a
-- 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 : ℤ)
a : Option α
inl : ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (x ::ₒ v ⊗ t) (Sum.inl none)
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (x ::ₒ v ⊗ t) (Sum.inl a)
have inl₁ : ∀ (val : α),
  ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (x ::ₒ v ⊗ t) (Sum.inl (some val))
Tactic: try { cases a <;> rfl}
Cleared hypotheses: a
-- 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 :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
s : Option α ⊕ β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) s = (t none ::ₒ v ⊗ t ∘ some) s
have inl : ∀ (a : Option α), ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (t none ::ₒ v ⊗ t ∘ some) (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 (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ Sum.inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
s : Option α ⊕ β
inl :
  ∀ (a : Option α), ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl a)
⊢ ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) s = (t none ::ₒ v ⊗ t ∘ some) s
have inr : ∀ (b : β), ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (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 (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ (t : β → ℕ), Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
v : α → ℕ
h :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (t none ::ₒ v ⊗ t ∘ some) (inl a)
have inl : ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (t none ::ₒ v ⊗ t ∘ some) (inl none)
Tactic: cases a
Cleared hypotheses: a
-- 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 :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ Sum.inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
⊢ ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl a)
have inl₁ : ∀ (val : α),
  ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
Tactic: cases a
Cleared hypotheses: a
-- 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 :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (t none ::ₒ v ⊗ t ∘ some) (inl a)
have inl : ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (t none ::ₒ v ⊗ t ∘ some) (inl none)
Tactic: { cases a <;> rfl }
Cleared hypotheses: a
-- 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 :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ Sum.inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
⊢ ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl a)
have inl₁ : ∀ (val : α),
  ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
Tactic: { cases a <;> rfl }
Cleared hypotheses: a
-- 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 :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (t none ::ₒ v ⊗ t ∘ some) (inl a)
have inl : ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (t none ::ₒ v ⊗ t ∘ some) (inl none)
Tactic: try { cases a <;> rfl }
Cleared hypotheses: a
-- 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 :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ Sum.inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
a : Option α
inl : ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl none) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl none)
⊢ ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl a) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl a)
have inl₁ : ∀ (val : α),
  ((v ⊗ t) ∘ (inr none ::ₒ Sum.inl ⊗ inr ∘ some)) (Sum.inl (some val)) = (t none ::ₒ v ⊗ t ∘ some) (Sum.inl (some val))
Tactic: try { cases a <;> rfl }
Cleared hypotheses: a
-- 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 :
  ∃ (t : Option β → ℕ),
    Eq (α := ℤ) ((Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p : (a : α ⊕ Option β → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)
t : Option β → ℕ
ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (t none ::ₒ v ⊗ t ∘ some) : ℤ) (0 : ℤ)
have rwa : ∀ (ht : Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (t none ::ₒ v ⊗ t ∘ some) : ℤ) (0 : ℤ)),
  Eq (α := ℤ) ((p : (a : Option α ⊕ β → ℕ) → ℤ) (t none ::ₒ v ⊗ t ∘ some) : ℤ) (0 : ℤ)
Tactic: rwa [show (v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = t none ::ₒ v ⊗ t ∘ some 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
f : (α → ℕ) → ℕ
⊢ DiophFn f = DiophPFun (↑f : (α → ℕ) →. ℕ)
have refine : ∀ (v : Option α → ℕ),
  Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | f (v ∘ some) = v none} v ↔
    Membership.mem (γ := Set (Option α → ℕ)) {v : Option α → ℕ | (v ∘ some, v none) ∈ (↑f : (α → ℕ) →. ℕ).graph} v
Tactic: refine congr_arg Dioph (Set.ext fun v => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
p : Poly α
v : Option α → ℕ
⊢ Membership.mem (γ := Set (Option α → ℕ))
      {v : Option α → ℕ | (fun (v : α → ℕ) ↦ Int.natAbs ((p : (a : α → ℕ) → ℤ) v)) (v ∘ some) = v none} v ↔
    Eq (α := ℤ)
      (((Poly.map some p - Poly.proj none) * (Poly.map some p + Poly.proj none) : (a : Option α → ℕ) → ℤ) v : ℤ) (0 : ℤ)
have dsimp : Int.natAbs ((p : (a : α → ℕ) → ℤ) (v ∘ some)) = v none ↔
  HSub.hSub (α := ℤ) (β := ℤ) ((p : (a : α → ℕ) → ℤ) (v ∘ some) : ℤ) ((↑(v none) : ℤ) : ℤ) *
      HAdd.hAdd (α := ℤ) (β := ℤ) ((p : (a : α → ℕ) → ℤ) (v ∘ some) : ℤ) ((↑(v none) : ℤ) : ℤ) =
    0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (hypothesis)
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
h :
  ∃ (h : (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).Dom),
    (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).get h = ((x ::ₒ v) ∘ some, (x ::ₒ v) none).2
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v
have h₁ : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
Tactic: rw [show (x ::ₒ v) ∘ some = v from funext fun s => rfl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (hypothesis)
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v
have hf : (f (v, (x ::ₒ v) none).1).Dom
Tactic: obtain ⟨hf, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (hypothesis)
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
hf : (f (v, (x ::ₒ v) none).1).Dom
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v
have h₁ : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
Tactic: obtain ⟨hf, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v
have refine : f.fn v hf ::ₒ v ∈ S
Tactic: refine ⟨hf, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h_1 :
  Membership.mem (γ := Set (α → ℕ))
    {v : α → ℕ | ∃ (x : ℕ), x ::ₒ v ∈ S ∩ {v : Option α → ℕ | (v ∘ some, v none) ∈ f.graph}} v
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ f.fn v hf ::ₒ v ∈ S
have rw : (v, (x ::ₒ v) none).2 ::ₒ v ∈ S
Tactic: rw [PFun.fn, h]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
h : Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S} v
x : f.Dom v
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).Dom),
    (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).get h = ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).2
have rw : ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2
Tactic: rw [show (f.fn v x ::ₒ v) ∘ some = v from funext fun s => rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ Membership.mem (γ := Set (Fin2 n → ℕ))
      {v : Fin2 n → ℕ |
        Membership.mem (γ := Set (Option (Fin2 n) → ℕ)) {v : Option (Fin2 n) → ℕ | (v ∘ none :: some) ∈ S} (f v ::ₒ v)}
      v ↔
    Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v
have dsimp : ((f v ::ₒ v) ∘ none :: some) ∈ S ↔ Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) ∈ S ↔ Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v
have a : (((f v ::ₒ v) ∘ none :: some) ∈ S) = Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v
Tactic: apply iff_of_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ (((f v ::ₒ v) ∘ none :: some) ∈ S) = Membership.mem (γ := Set (Fin2 n → ℕ)) {v : Vector3 ℕ n | (f v :: v) ∈ S} v
have a : ((f v ::ₒ v) ∘ none :: some) = f v :: v
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) = f v :: v
have a : ∀ (x : Fin2 (n + 1)), ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
x : Fin2 (n + 1)
⊢ ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x
have a : ((f v ::ₒ v) ∘ none :: some) fz = (f v :: v) fz
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
x : Fin2 (n + 1)
a : ((f v ::ₒ v) ∘ none :: some) fz = (f v :: v) fz
⊢ ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x
have a₁ : ∀ (a : Fin2 n), ((f v ::ₒ v) ∘ none :: some) a.fs = (f v :: v) a.fs
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ Membership.mem (γ := Set (Option (Fin2 n) → ℕ)) {v : Option (Fin2 n) → ℕ | (v ∘ none :: some) ∈ S} (x ::ₒ v) ↔
    (x :: v) ∈ S
have dsimp : ((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
s : Fin2 (n + 1)
⊢ ((x ::ₒ v) ∘ none :: some) s = (x :: v) s
have fz : ((x ::ₒ v) ∘ none :: some) fz = (x :: v) fz
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
s : Fin2 (n + 1)
fz : ((x ::ₒ v) ∘ none :: some) Fin2.fz = (x :: v) Fin2.fz
⊢ ((x ::ₒ v) ∘ none :: some) s = (x :: v) s
have fs : ∀ (b : Fin2 n), ((x ::ₒ v) ∘ none :: some) b.fs = (x :: v) b.fs
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ ((x ::ₒ v) ∘ none :: some) ∈ S ↔ (x :: v) ∈ S
have rw : (x :: v) ∈ S ↔ (x :: v) ∈ S
Tactic: rw [show Option.elim' x v ∘ cons none some = x :: v from
          funext fun s => by rcases s with a | b <;> rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
h : VectorAllP DiophFn f
v : α → ℕ
⊢ Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α)) ∈ S} v ↔
    Membership.mem (γ := Set (α → ℕ)) {v : α → ℕ | (v ⊗ fun (i : Fin2 0) ↦ f i v) ∈ S} v
have dsimp : v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α)) ∈ S ↔ (v ⊗ fun (i : Fin2 0) ↦ f i v) ∈ S
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
h : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α)) ∈ S ↔ (v ⊗ fun (i : Fin2 0) ↦ f i v) ∈ S
have a : v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α)) = v ⊗ fun (i : Fin2 0) ↦ f i v
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
h : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α)) = v ⊗ fun (i : Fin2 0) ↦ f i v
have a : ∀ (x : α ⊕ Fin2 0), (v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α))) x = (v ⊗ fun (i : Fin2 0) ↦ f i v) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
h : VectorAllP DiophFn f
v : α → ℕ
x : α ⊕ Fin2 0
⊢ (v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α))) x = (v ⊗ fun (i : Fin2 0) ↦ f i v) x
have a : ∀ (val : α), (v ∘ (id ⊗ elim0 (C := fun (a : Fin2 0) ↦ α))) (inl val) = (v ⊗ fun (i : Fin2 0) ↦ f i v) (inl val)
Tactic: obtain _ | _ | _ := x
Cleared hypotheses: x