# Zulip Chat Archive

## Stream: general

### Topic: induction h vs rw h for `h : i = i'`

#### Eric Wieser (Oct 28 2020 at 10:38):

I was surprised to see `tidy?`

generate `induction h`

when `h`

is an equality. I'm a little puzzled by the meaning of this, especially since `rw h`

fails. The goal state was

```
h: i = i'
⊢ ↑(eq.rec ⟨↑si, _⟩ _) = ↑(eq.rec si h)
```

and after `induction h`

becomes

```
⊢ ↑(eq.rec ⟨↑si, _⟩ _) = ↑(eq.rec si _)
```

Can someone explain to me the intuition here?

#### Chris Hughes (Oct 28 2020 at 10:59):

I don't know exactly what's going on here, but the reason `rw`

doesn't work is probably because there is a term in the goal whose type contains `i`

, which means that it is harder to generate the motive (the argument called `C`

in the type of `eq.rec`

) when making the proof term. `induction`

on equality is basically just substitution, but the `induction`

tactic has better support for computing the motive than `rw`

, and makes the substitution everywhere. I think somehow it's easier to compute the motive when you rewrite at all your hypotheses, and also easier when one side of the equality is just a local constant.

#### Eric Wieser (Oct 28 2020 at 11:04):

Thanks, your wording made me realize that `induction h`

is doing the same thing as `subst h`

(which unlike `rw h`

, also works)

#### Eric Wieser (Oct 28 2020 at 11:05):

For more context of what's going on, I'm trying to prove the trivial-but-somehow-not-refl statement in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Difficulty.20with.20dependent.20rewrites/near/214686669

Last updated: Dec 20 2023 at 11:08 UTC