-- 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
s : α ⊕ β
⊢ ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) s = (v ⊗ t ∘ inl) s

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

Result:
no goals

Proof state:
case cons
α : 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 : List.Forall Dioph (S :: l)
⊢ ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) (S :: l) ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl

Tactic:
simp? at d says simp only [List.forall_cons] at d

Result:
case cons
α : 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
⊢ ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) (S :: l) ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl

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
s : α ⊕ γ
⊢ (v ⊗ m ⊗ n) ((inl ⊗ fun x => inr (inr x)) s) = (v ⊗ n) 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 : α → ℕ
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
⊢ p (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

Result:
no goals

Proof state:
case cons
α : 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
⊢ ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S => S v) (S :: l) ↔ ∃ t, List.Forall (fun p => p (v ⊗ t) = 0) pl

Tactic:
exact
  let ⟨⟨β, p, pe⟩, dl⟩ := d
  let ⟨γ, pl, ple⟩ := IH dl
  ⟨β ⊕ γ, p.map (inl ⊗ inr ∘ inl)::pl.map fun q => q.map (inl ⊗ inr ∘ inr),
    fun v => by
    simp; 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
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
s : α ⊕ β
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) s = (v ⊗ m) 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 : α → ℕ
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
⊢ p ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) = 0

Tactic:
rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m 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
⊢ p (v ⊗ m) = 0