awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
s : α ⊕ β
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) s = (v ⊗ m) s
have inl : ∀ (a : α), ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) (inl a) = (v ⊗ m) (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 (α → ℕ)
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
s : α ⊕ β
inl : ∀ (a : α), ((v ⊗ m ⊗ n) ∘ (Sum.inl ⊗ inr ∘ Sum.inl)) (Sum.inl a) = (v ⊗ m) (Sum.inl a)
⊢ ((v ⊗ m ⊗ n) ∘ (Sum.inl ⊗ inr ∘ Sum.inl)) s = (v ⊗ m) s
have inr : ∀ (b : β), ((v ⊗ m ⊗ n) ∘ (Sum.inl ⊗ inr ∘ Sum.inl)) (inr b) = (v ⊗ m) (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 (α → ℕ)
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
⊢ List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ m ⊗ n) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
    pl
have 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
Tactic: refine List.Forall.imp (fun q hq => ?_) hn
-- 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)
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 : ℤ)
⊢ ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ m ⊗ n) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (inl ⊗ inr ∘ inr) q)
    q
have dsimp : Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) fun (x : α ⊕ γ) ↦ (v ⊗ m ⊗ n) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) x) : ℤ) (0 : ℤ)
Tactic: dsimp [Function.comp_def]
-- 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)
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 : α ⊕ γ
⊢ (v ⊗ m ⊗ n) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) s) = (v ⊗ n) s
have inl : ∀ (a : α), (v ⊗ m ⊗ n) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) (inl a)) = (v ⊗ n) (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 (α → ℕ)
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 : γ) ↦ inr (inr x)) (Sum.inl a)) = (v ⊗ n) (Sum.inl a)
⊢ (v ⊗ m ⊗ n) ((Sum.inl ⊗ fun (x : γ) ↦ inr (inr x)) s) = (v ⊗ n) s
have inr : ∀ (b : γ), (v ⊗ m ⊗ n) ((Sum.inl ⊗ fun (x : γ) ↦ inr (inr x)) (inr b)) = (v ⊗ n) (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 (α → ℕ)
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
s : α ⊕ β
⊢ ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) s = (v ⊗ t ∘ inl) s
have inl : ∀ (a : α), ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) (inl a) = (v ⊗ t ∘ inl) (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 (α → ℕ)
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 ⊗ inr ∘ Sum.inl)) : ℤ) (0 : ℤ) ∧
      List.Forall
        ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
          fun (q : Poly (α ⊕ γ)) ↦ Poly.map (Sum.inl ⊗ inr ∘ inr) q)
        pl
t : β ⊕ γ → ℕ
hl : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ Sum.inl)) : ℤ) (0 : ℤ)
hr :
  List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (Sum.inl ⊗ inr ∘ inr) q)
    pl
s : α ⊕ β
inl : ∀ (a : α), ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ Sum.inl)) (Sum.inl a) = (v ⊗ t ∘ Sum.inl) (Sum.inl a)
⊢ ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ Sum.inl)) s = (v ⊗ t ∘ Sum.inl) s
have inr : ∀ (b : β), ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ Sum.inl)) (inr b) = (v ⊗ t ∘ Sum.inl) (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 (α → ℕ)
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
⊢ Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) (v ⊗ t ∘ inl) : ℤ) (0 : ℤ)
have 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 : ℤ)
Tactic: rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
                    funext fun s => by rcases s with a | b <;> rfl] at hl
Cleared hypotheses: hl, hr
-- 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)
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
have 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 : ℤ)
Tactic: refine List.Forall.imp (fun q hq => ?_) hr
-- 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)
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 : ℤ)
s : α ⊕ γ
⊢ (v ⊗ t) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) s) = (v ⊗ t ∘ inr) s
have inl : ∀ (a : α), (v ⊗ t) ((inl ⊗ fun (x : γ) ↦ inr (inr x)) (inl a)) = (v ⊗ t ∘ inr) (inl a)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S : Set (α → ℕ)
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 ⊗ inr ∘ Sum.inl)) : ℤ) (0 : ℤ) ∧
      List.Forall
        ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
          fun (q : Poly (α ⊕ γ)) ↦ Poly.map (Sum.inl ⊗ inr ∘ inr) q)
        pl
t : β ⊕ γ → ℕ
hl : Eq (α := ℤ) ((p : (a : α ⊕ β → ℕ) → ℤ) ((v ⊗ t) ∘ (Sum.inl ⊗ inr ∘ Sum.inl)) : ℤ) (0 : ℤ)
hr :
  List.Forall
    ((fun (p : Poly (α ⊕ β ⊕ γ)) ↦ Eq (α := ℤ) ((p : (a : α ⊕ β ⊕ γ → ℕ) → ℤ) (v ⊗ t) : ℤ) (0 : ℤ)) ∘
      fun (q : Poly (α ⊕ γ)) ↦ Poly.map (Sum.inl ⊗ inr ∘ inr) q)
    pl
q : Poly (α ⊕ γ)
hq :
  Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) fun (x : α ⊕ γ) ↦ (v ⊗ t) ((Sum.inl ⊗ fun (x : γ) ↦ inr (inr x)) x) : ℤ)
    (0 : ℤ)
s : α ⊕ γ
inl : ∀ (a : α), (v ⊗ t) ((Sum.inl ⊗ fun (x : γ) ↦ inr (inr x)) (Sum.inl a)) = (v ⊗ t ∘ inr) (Sum.inl a)
⊢ (v ⊗ t) ((Sum.inl ⊗ fun (x : γ) ↦ inr (inr x)) s) = (v ⊗ t ∘ inr) s
have inr : ∀ (b : γ), (v ⊗ t) ((Sum.inl ⊗ fun (x : γ) ↦ inr (inr x)) (inr b)) = (v ⊗ t ∘ inr) (inr b)
Tactic: rcases s with a | b
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u
S : Set (α → ℕ)
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 : ℤ)
⊢ Eq (α := ℤ) ((q : (a : α ⊕ γ → ℕ) → ℤ) (v ⊗ t ∘ inr) : ℤ) (0 : ℤ)
have rwa : ∀ (hq : 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
Cleared hypotheses: hq