-- Mathlib/NumberTheory/Dioph.lean
theorem DiophList.forall (l : List (Set <| α → ℕ)) (d : l.Forall Dioph) :
    Dioph {v | l.Forall fun S : Set (α → ℕ) => v ∈ S}

Proof state:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
dl : List.Forall Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
⊢ List.Forall (fun p => p (v ⊗ t ∘ inr) = 0) pl

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

Result:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
dl : List.Forall Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) q
⊢ q (v ⊗ t ∘ inr) = 0

Proof state:
case nil
α : Type u
d : List.Forall Dioph []
⊢ ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) [] ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl

Tactic:
exact ⟨ULift Empty, [], fun _ => by simp⟩

Result:
no goals

Proof state:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
dl : List.Forall Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : (q fun x => (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) x)) = 0
⊢ q (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

Result:
no goals

Proof state:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
dl : List.Forall Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) q
⊢ q (v ⊗ t ∘ inr) = 0

Tactic:
dsimp [Function.comp_def] at hq

Result:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
d : Dioph S ∧ List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
dl : List.Forall Dioph l
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S => S v) l ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p => p (v ⊗ t) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : (q fun x => (v ⊗ t) ((inl ⊗ fun x => inr (inr x)) x)) = 0
⊢ q (v ⊗ t ∘ inr) = 0