rewriting terms

Stream: new members

[Dean Young]

I know how to rewrite the goal in Lean 4, but how to you rewrite a particular term?

variable {X : Type}
variable {x₁ : X}
variable {x₂ : X}
variable {p : x₁ = x₂}
def in_this_theorem_rewrite_the_term_x₁_to_x₂_using_p : X := by
rewrite_using_p x₁ p???
sorry

[Adam Topaz]

Please provide a #mwe

[Adam Topaz]

I assume you know about rw [p] at foo?

[Dean Young]

I didn't know about the "at foo" feature.

Here is the example that I got to work using that:

variable {X : Type}
variable {Y₁ : Type}
variable {Y₂ : Type}
variable {Z : Type}
variable {p : Y₁ = Y₂}
variable {f : X → Y₁}
variable {g : Y₂ → Z}
def element_of_X : X → Z := by
rw [p] at f
exact λ (x : X) => g (f x)

Thanks!

[Julian Berman]

I think def element_of_X : X → Z := g ∘ p.mp ∘ f is another way to write that specific example in case that's also helpful (though obviously for others yeah, rw at is good to know about).

[Dean Young]

When I use it, other structures start giving me errors of the form "(kernel) declaration has free variables". What does that mean?

[Alex J. Best]

That is something which shouldn't happen normally. Can you give us an example of where this happens for you. Try the recover tactic at the end of the proof which causes this error and see if any goals appear.