α✝ : Type ?u.2199
β✝ : Type ?u.2202
γ : Type ?u.2205
δ : Type ?u.2208
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂
α✝ : Type ?u.2199
β✝ : Type ?u.2202
γ : Type ?u.2205
δ : Type ?u.2208
α : Type u_1
β : Type u_2
a : α
⊢ Function.Injective (mk a)
intro b₁ b₂ h
no goals
α✝ : Type ?u.2199
β✝ : Type ?u.2202
γ : Type ?u.2205
δ : Type ?u.2208
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂
simpa only [true_and, Prod.mk.inj_iff, eq_self_iff_true] using h