# Zulip Chat Archive

## Stream: new members

### Topic: Casting and inductions

#### Gareth Ma (Feb 03 2023 at 16:36):

Hi. Just a disclaimer, I know I probably shouldn't worry about tactics in lean 3 too much, but I was just curious + I need to prove the results for my use case.

I am trying to read the proof of `∀ m n, ((m * n : ℤ) : α) = m * n :=`

at https://github.com/leanprover-community/mathlib/blob/bed4f0529aa52e2b169d5c2359eef2849e306028/src/data/int/cast/lemmas.lean#L47, but I don't understand their syntax. In particular, how can I turn the proof into interactive mode while still using `int.induction_on'`

?

#### Kyle Miller (Feb 03 2023 at 16:40):

@Gareth Ma Here's a tactic proof:

```
import data.int.cast.lemmas
variables {α : Type*}
@[simp, norm_cast] theorem cast_mul [non_assoc_ring α] (m n : ℤ) : ((m * n : ℤ) : α) = m * n :=
begin
induction m using int.induction_on' with k _ ih k _ ih,
{ exact 0 },
{ simp },
{ simp [add_mul, ih] },
{ simp [sub_mul, ih] },
end
```

#### Gareth Ma (Feb 03 2023 at 16:41):

Thank you!! Really helps a lot :heart:

#### Kyle Miller (Feb 03 2023 at 16:43):

You'll probably more likely see something like this, using `refine`

rather than `induction`

:

```
@[simp, norm_cast] theorem cast_mul [non_assoc_ring α] (m n : ℤ) : ((m * n : ℤ) : α) = m * n :=
begin
refine int.induction_on' m 0 _ _ _,
{ simp },
{ intros _ ih, simp [add_mul, ih] },
{ intros _ ih, simp [sub_mul, ih] },
end
```

#### Kyle Miller (Feb 03 2023 at 16:45):

I guess there's a one-lie tactic proof, where you apply `simp`

to every goal with the `contextual`

option (which allows it to use left sides of implications to simplify right sides).

```
@[simp, norm_cast] theorem cast_mul [non_assoc_ring α] (m n : ℤ) : ((m * n : ℤ) : α) = m * n :=
begin
refine int.induction_on' m 0 _ _ _; simp { contextual := tt },
end
```

Last updated: Dec 20 2023 at 11:08 UTC