Rewrite rule corresponding to `#reduce (types := true)`?

Stream: general

[nrs]

If let s : someStructure := <2, fun x => Fin x>, we have that #reduce (types := true) s.2 7 will produce Fin 7. Is there a rewrite rule that I could use to reduce x : s.2 7 in my proof state to x : Fin 7? I would be looking for a lemma like s.2 7 = (fun x => Fin x) 7 = Fin 7, but is there one similar to this that is either automatically generated (similarly to .eq_def) or that can be inferred somehow?

[Kevin Buzzard]

If you wrote the structure then why don't you just write the lemma yourself and prove it with rfl?

[nrs]

Kevin Buzzard said:

If you wrote the structure then why don't you just write the lemma yourself and prove it with rfl?

Yeah I've been doing this but I thought, any such reduction rule is probably generated by Lean itself when it evaluates #reduce right?

[nrs]

In case anyone has a similar issue: the reduce tactic can be used for this purpose. If you're in term mode and don't want to enter tactics mode, and if x : s.2 7 is in your context, you can use let x := beta% clear% by reduce at x; exact x, which will give you a term x : Fin 7 which is defeq to the previous one

[Kevin Buzzard]

You say "if you don't want enter tactic mode" but that by puts you into tactic mode.

[nrs]

Kevin Buzzard said:

You say "if you don't want enter tactic mode" but that by puts you into tactic mode.

Yeah I meant for the rest of the proof (in general, once you enter tactic mode with a by at top of your declaration, you can't leave it, right?). I'm working on an elaborator to avoid it entirely, just for metaprogramming practice, but here's how you can keep in term mode after using it:

theorem ... (x : s.2 7) ... :=
  let x := beta% clear% by reduce at x; exact x
  ...

[Kevin Buzzard]

exact takes you back into term mode. In Lean 3 it was pretty common to see things like by classical; exact... to switch classical mode on.

[nrs]

Kevin Buzzard said:

exact takes you back into term mode. In Lean 3 it was pretty common to see things like by classical; exact... to switch classical mode on.

woah! I've never encountered using exact like this before, only exact t with a term ending the proof, thanks a lot for that tip!

[Mario Carneiro]

FYI it's by classical exact in lean 4

[Mario Carneiro]

because classical is a tactic combinator, not a tactic (anymore)

[nrs]

I see ty!!

[Kevin Buzzard]

nrs said:

Kevin Buzzard said:

exact takes you back into term mode. In Lean 3 it was pretty common to see things like by classical; exact... to switch classical mode on.

woah! I've never encountered using exact like this before, only exact t with a term ending the proof, thanks a lot for that tip!

I remember Mario telling me this in 2017 and it blowing my mind too :-)