Casting and inductions

Stream: new members

[Gareth Ma]

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]

@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]

Thank you!! Really helps a lot :heart:

[Kyle Miller]

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]

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