rw [hp a2 hp1]
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b1 = b2
case intro
α β γ : Type
f : α → β → γ
hf : Function.Injective2 f
p : α → β → β
hp : ∀ (a : α), Function.Injective (p a)
a1 a2 : α
b1 b2 : β
hab : (fun r c => f r (p r c)) a1 b1 = (fun r c => f r (p r c)) a2 b2
ha1 : a2 = a2
hp1 : p a2 b1 = p a2 b2
⊢ a2 = a2 ∧ b2 = b2