help with function application and equality type

Stream: new members

[Dean Young]

does anyone know how to fill in sorry in the lemma?

lemma (X : Type) (Y : Type) (Z : Type) (A : Type) (f : X → Y → Z → A) (x₁ : X) (x₂ : X) (y₁ : Y) (y₂ : Y) (z₁ : Z) (z₂ : Z)  : f x₁ y₁ z₁ = f x₁ y₂ z₂ := sorry

edit: oops:

lemma (X : Type) (Y : Type) (Z : Type) (A : Type) (f : X → Y → Z → A) (x₁ : X) (x₂ : X) (y₁ : Y) (y₂ : Y) (z₁ : Z) (z₂ : Z) (p : x₁ = x₂) (q : y₁ = y₂) (r : z₁ = z₂) : f x₁ y₁ z₁ = f x₁ y₂ z₂ := sorry

[Eric Wieser]

What's the maths proof?

[Notification Bot]

This topic was moved here from #general > help with function application and equality type by Eric Wieser.

[Eric Wieser]

(I've moved this because the answer to your question is "this is obviously false", and explaining why feels like a #new members-type problem)

[Dean Young]

oops:

lemma (X : Type) (Y : Type) (Z : Type) (A : Type) (f : X → Y → Z → A) (x₁ : X) (x₂ : X) (y₁ : Y) (y₂ : Y) (z₁ : Z) (z₂ : Z) (p : x₁ = x₂) (q : y₁ = y₂) (r : z₁ = z₂) : f x₁ y₁ z₁ = f x₁ y₂ z₂ := sorry

[Eric Wieser]

Do you know about tactic#rewrite (aka rw)?

[Eric Wieser]

Sorry, that link fails

[Eric Wieser]

https://leanprover-community.github.io/mathlib_docs/tactics.html#rw%20/%20rewrite