Local definition and substitutions

Stream: new members

[Sébastien Boisgérault]

Hi everyone,

If find myself using a lot the following pattern: within a proof, define a new variable (below ϕ) to summarize a long term, then state that both objects are equal (below ϕ_def)-- to be able to subsitute one for the other with rw[ϕ_def] and rw [<- ϕ_def]. Typical exemple:

let ϕ := f ∘ γ.extend
have ϕ_def : ϕ = f ∘ γ.extend := rfl

Is there a way to automate the definition of ϕ_def? Or a way to avoid the need for ϕ_defin the first place?

Cheers,

Sébastien

[Yaël Dillies]

Hey Sébastien! You can replace let ϕ := f ∘ γ.extend by set ϕ := f ∘ γ.extend with φ_def.

[Sébastien Boisgérault]

Yaël Dillies said:

Hey Sébastien! You can replace let ϕ := f ∘ γ.extend by set ϕ := f ∘ γ.extend with φ_def.

Thanks a lot for your answer Yaël, this is exactly what i need!

Could you point me to a place in the documentation where the set ... with ... construct is defined please?

[Yaël Dillies]

If you Ctrl + click on a set ... with ..., it will bring you to the definition

[Sébastien Boisgérault]

:+1: Thanks!

And I see that the construct performs the replacement automatically, nice!