-- 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) = 0) ∧ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
m : β → ℕ
hm : p (v ⊗ m) = 0
n : γ → ℕ
hn : List.Forall (fun p => p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : q (v ⊗ n) = 0
⊢ (q 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]

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) = 0) ∧ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
m : β → ℕ
hm : p (v ⊗ m) = 0
n : γ → ℕ
hn : List.Forall (fun p => p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : q (v ⊗ n) = 0
⊢ q (v ⊗ n) = 0

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) = 0) ∧ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
m : β → ℕ
hm : p (v ⊗ m) = 0
n : γ → ℕ
hn : List.Forall (fun p => p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : q (v ⊗ n) = 0
⊢ q (v ⊗ n) = 0

Tactic:
exact 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 : (q 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

Tactic:
rcases s with a | b <;> rfl

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 : α → ℕ
⊢ S v ∧ List.Forall (fun S => S v) l ↔
    ∃ 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

Tactic:
exact
Iff.trans (and_congr (pe v) (ple v))
⟨fun ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ =>
⟨m ⊗ n, by
  rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from
        funext fun s => by rcases s with a | b <;> rfl]; exact hm, by
  refine List.Forall.imp (fun q hq => ?_) hn; dsimp [Function.comp_def]
  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]; exact hq⟩,
fun ⟨t, hl, hr⟩ =>
⟨⟨t ∘ inl, by
    rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
        funext fun s => by rcases s with a | b <;> rfl] at hl⟩,
  ⟨t ∘ inr, by
    refine List.Forall.imp (fun q hq => ?_) hr; dsimp [Function.comp_def] at hq
    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
d : List.Forall Dioph []
x✝ : α → ℕ
⊢ List.Forall (fun S => S x✝) [] ↔ ∃ t, List.Forall (fun p => p (x✝ ⊗ t) = 0) []

Tactic:
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) = 0) ∧ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
m : β → ℕ
hm : p (v ⊗ m) = 0
n : γ → ℕ
hn : List.Forall (fun p => p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : q (v ⊗ n) = 0
⊢ ((fun p => p (v ⊗ m ⊗ n) = 0) ∘ fun q => Poly.map (inl ⊗ inr ∘ inr) q) q

Tactic:
dsimp [Function.comp_def]

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) = 0) ∧ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl
m : β → ℕ
hm : p (v ⊗ m) = 0
n : γ → ℕ
hn : List.Forall (fun p => p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : q (v ⊗ n) = 0
⊢ (q fun x => (v ⊗ m ⊗ n) ((inl ⊗ fun x => inr (inr x)) x)) = 0