-- Mathlib/NumberTheory/Dioph.lean
theorem diophPFun_comp1 {S : Set (Option α → ℕ)} (d : Dioph S) {f} (df : DiophPFun f) :
    Dioph {v : α → ℕ | ∃ h : f.Dom v, f.fn v h ::ₒ v ∈ S} :=
  ext (ex1_dioph (d.inter df)) fun v =>
    ⟨fun ⟨x, hS, (h : Exists _)⟩ => by
      rw [show (x ::ₒ v) ∘ some = v from funext fun s => rfl] at h
      obtain ⟨hf, h⟩ := h; refine ⟨hf, ?_⟩; rw [PFun.fn, h]; exact hS,
    fun ⟨x, hS⟩ =>
      ⟨f.fn v x, hS, show Exists _ by
        rw [show (f.fn v x ::ₒ v) ∘ some = v from funext fun s => rfl]; exact ⟨x, rfl⟩⟩⟩

Proof state:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
h :
  ∃ (h : (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).Dom),
    (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).get h = ((x ::ₒ v) ∘ some, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}

Tactic:
rw [show (x ::ₒ v) ∘ some = v from funext fun s => rfl] at h

Result:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}

Proof state:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}
x : f.Dom v
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2

Tactic:
exact ⟨x, rfl⟩

Result:
no goals

Proof state:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}

Tactic:
obtain ⟨hf, h⟩ := h

Result:
case intro
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}

Proof state:
case intro
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ (v, (x ::ₒ v) none).2 ::ₒ v ∈ S

Tactic:
exact hS

Result:
no goals

Proof state:
case intro
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}

Tactic:
refine ⟨hf, ?_⟩

Result:
case intro
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ f.fn v hf ::ₒ v ∈ S

Proof state:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}
x : f.Dom v
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).Dom),
    (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).get h = ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).2

Tactic:
rw [show (f.fn v x ::ₒ v) ∘ some = v from funext fun s => rfl]

Result:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}
x : f.Dom v
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2

Proof state:
case intro
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ f.fn v hf ::ₒ v ∈ S

Tactic:
rw [PFun.fn, h]

Result:
case intro
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ (v, (x ::ₒ v) none).2 ::ₒ v ∈ S