# Zulip Chat Archive

## Stream: new members

### Topic: trouble unfolding dite

#### Daniel Fabian (Jun 10 2020 at 21:41):

In order to construct a counter example, I want to modify a function at one point and I'm having trouble proving it.

```
import tactic
theorem modified
{α : Type}
{β : α → Type}
(f : Π x, β x)
(x : α) (y : β x) : ∃ f' : Π x, β x, f' x = y ∧ ∀ x' ≠ x, f' x' = f x' :=
begin
classical,
set f' : Π x, β x := λ x', dite (x = x') (λ hxx', by { rw hxx' at y, exact y }) (λ _, f x') with hf',
use f',
split,
begin
rw hf',
--refl -- doesn't work,
simp,
end,
begin
intros x' hnxx',
rw hf',
simp,
sorry
end,
end
```

it boils down to this:

```
hnxx' : x' ≠ x
⊢ dite (x = x') (λ (hxx' : x = x'), eq.mp _ y) (λ (_x : ¬x = x'), f x') = f x'
```

which should obviously hold. But how can we unfold `dite`

, taking into consideration, that we've got a proof of $x' \ne x$.

#### Kevin Buzzard (Jun 10 2020 at 21:42):

`dif_neg`

#### Kevin Buzzard (Jun 10 2020 at 21:43):

` rw dif_neg hnxx'.symm,`

#### Daniel Fabian (Jun 10 2020 at 21:44):

fantastic, thanks

#### Kevin Buzzard (Jun 10 2020 at 21:46):

In general you can deconstruct `dite`

with `split_ifs`

but in the situation where you know the truth value of the hypothesis `dif_pos`

and `dif_neg`

are easier.

#### Daniel Fabian (Jun 10 2020 at 21:47):

thanks. (and you sure are very quick to respond, lol)

#### Kevin Buzzard (Jun 10 2020 at 21:47):

I'm addicted

#### Mario Carneiro (Jun 10 2020 at 21:51):

If you want to modify a function at one point, try `function.update`

#### Mario Carneiro (Jun 10 2020 at 21:52):

which in particular deals with the messy business of dependent function updates

#### Daniel Fabian (Jun 10 2020 at 21:53):

but that particular one changes the type, though, right? Because at point a', you are now of a different type. My theorem preserves the same type.

#### Daniel Fabian (Jun 10 2020 at 21:54):

(deleted)

#### Mario Carneiro (Jun 10 2020 at 21:55):

```
import tactic logic.function.basic
theorem modified
{α : Type}
{β : α → Type}
(f : Π x, β x)
(x : α) (y : β x) : ∃ f' : Π x, β x, f' x = y ∧ ∀ x' ≠ x, f' x' = f x' :=
by classical; exact
⟨function.update f x y,
function.update_same _ _ _,
λ x' h, function.update_noteq h _ _⟩
```

#### Daniel Fabian (Jun 10 2020 at 21:59):

ah, very nice

#### Daniel Fabian (Jun 10 2020 at 22:00):

thanks, learnt something again

Last updated: May 15 2021 at 23:13 UTC