-- Mathlib/NumberTheory/Dioph.lean
theorem ex1_dioph {S : Set (Option α → ℕ)} : Dioph S → Dioph {v | ∃ x, x ::ₒ v ∈ S}
  | ⟨β, p, pe⟩ =>
    ⟨Option β, p.map (inr none ::ₒ inl ⊗ inr ∘ some), fun v =>
      ⟨fun ⟨x, hx⟩ =>
        let ⟨t, ht⟩ := (pe _).1 hx
        ⟨x ::ₒ t, by
          simp only [Poly.map_apply]
          rw [show (v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = x ::ₒ v ⊗ t from
            funext fun s => by rcases s with a | b <;> try { cases a <;> rfl}; rfl]
          exact ht⟩,
        fun ⟨t, ht⟩ =>
        ⟨t none,
          (pe _).2
            ⟨t ∘ some, by
              simp only [Poly.map_apply] at ht
              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 ⟩⟩⟩⟩

Proof state:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
⊢ p ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0

Tactic:
rw [show (v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = x ::ₒ v ⊗ t from
  funext fun s => by rcases s with a | b <;> try { cases a <;> rfl}; rfl]

Result:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
⊢ p (x ::ₒ v ⊗ t) = 0

Proof state:
case inl
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((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)

Tactic:
cases a <;> rfl

Result:
no goals

Proof state:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
s : Option α ⊕ β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) s = (t none ::ₒ v ⊗ t ∘ some) s

Tactic:
rcases s with a | b <;> try { cases a <;> rfl }

Result:
case inr
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)

Proof state:
case inr
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)

Tactic:
rfl

Result:
no goals

Proof state:
case inl
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
a : Option α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (x ::ₒ v ⊗ t) (inl a)

Tactic:
cases a <;> rfl

Result:
no goals

Proof state:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
s : Option α ⊕ β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) s = (x ::ₒ v ⊗ t) s

Tactic:
rcases s with a | b <;> try { cases a <;> rfl}

Result:
case inr
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
b : β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (x ::ₒ v ⊗ t) (inr b)

Proof state:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
⊢ p (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

Result:
no goals

Proof state:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
⊢ (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ x ::ₒ t) = 0

Tactic:
simp only [Poly.map_apply]

Result:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
⊢ p ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0

Proof state:
case inr
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
b : β
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (x ::ₒ v ⊗ t) (inr b)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : {v | ∃ x, x ::ₒ v ∈ S} v
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
⊢ p (x ::ₒ v ⊗ t) = 0

Tactic:
exact ht

Result:
no goals

Proof state:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
⊢ p (t none ::ₒ v ⊗ t ∘ some) = 0

Tactic:
simp only [Poly.map_apply] at ht

Result:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), S v ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
⊢ p (t none ::ₒ v ⊗ t ∘ some) = 0