# Zulip Chat Archive

## Stream: new members

### Topic: rewrite goal

#### Thorsten Altenkirch (Sep 21 2020 at 15:04):

I couldn't find a tactic to rewrite the current goal. I can use `have`

but this seems to be a bit verbose. E.g. like in the following example

``

def is_tt : bool → Prop

| ff := false

| tt := true

-- BEGIN

theorem cons : ¬ (tt = ff) :=

begin

assume h,

have aux : is_tt ff,

rewrite← h,

constructor,

exact aux,

end

#### Johan Commelin (Sep 21 2020 at 15:04):

You need triple #backticks

#### Thorsten Altenkirch (Sep 21 2020 at 15:05):

Is there a tactic to rewrite the current goal? I can use `have`

but this seems to be a bit verbose. E.g.

```
```

#### Mario Carneiro (Sep 21 2020 at 15:06):

you can edit your posts too

#### Mario Carneiro (Sep 21 2020 at 15:07):

`rw`

will rewrite in the current goal. Could you give an example of what you would like to write?

#### Kevin Buzzard (Sep 21 2020 at 15:08):

```
def is_tt : bool → Prop
| ff := false
| tt := true
-- BEGIN
theorem cons : ¬ (tt = ff) :=
begin
assume h,
cases h,
end
```

#### Mario Carneiro (Sep 21 2020 at 15:08):

by the way you can prove this theorem using simply `theorem cons : ¬ (tt = ff).`

#### Mario Carneiro (Sep 21 2020 at 15:08):

which is equivalent to Kevin's proof

#### Mario Carneiro (Sep 21 2020 at 15:09):

but I can see you are going for the proof that doesn't use the builtin knowledge that cases has about injectivity of constructors

#### Kevin Buzzard (Sep 21 2020 at 15:10):

Rewriting `h : X = Y`

with X a variable can sometimes be done more powerfully in Lean by using `subst h`

or `cases h`

. If these work they might globally replace X by Y

#### Kevin Buzzard (Sep 21 2020 at 15:10):

I am always looking for places to do `cases`

on stuff

#### Mario Carneiro (Sep 21 2020 at 15:10):

I would suggest presenting your proof like so:

```
def is_tt : bool → Prop
| ff := false
| tt := true
theorem cons : tt ≠ ff :=
begin
assume h,
change is_tt ff,
rw ← h,
trivial
end
```

#### Mario Carneiro (Sep 21 2020 at 15:10):

you can also insert `change true`

before the `trivial`

to make it clearer

#### Kevin Buzzard (Sep 21 2020 at 15:11):

inb4 Mario

```
def is_tt : bool → Prop
| ff := false
| tt := true
theorem cons : ¬ (tt = ff).
```

#### Kevin Buzzard (Sep 21 2020 at 15:11):

@Thorsten Altenkirch the equation compiler can prove your theorem all by itself.

#### Mario Carneiro (Sep 21 2020 at 15:11):

Mario Carneiro said:

by the way you can prove this theorem using simply

`theorem cons : ¬ (tt = ff).`

#### Kevin Buzzard (Sep 21 2020 at 15:12):

dammit I haven't got my glasses on

#### Kevin Buzzard (Sep 21 2020 at 15:12):

I missed the full stop :-)

#### Kevin Buzzard (Sep 21 2020 at 15:12):

touch\'e

#### Kevin Buzzard (Sep 21 2020 at 15:12):

My VS Code font is a lot bigger than my Zulip font :-)

#### Thorsten Altenkirch (Sep 21 2020 at 15:27):

I know that I can prove it directly but I just wanted to show how to prove it from basic principles.

#### Mario Carneiro (Sep 21 2020 at 15:34):

Kevin should be familiar with this from his blog post no confusion over no_confusion

Last updated: May 11 2021 at 22:14 UTC