α✝ : Type u
β✝ : Type v
α : Type u_1
β : α → Type u_2
x y : (a : α) → Perm (β a)
h : ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y
⊢ x = y
α✝ : Type u
β✝ : Type v
α : Type u_1
β : α → Type u_2
⊢ Function.Injective ↑(sigmaCongrRightHom β)
intro x y h
case h.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : α → Type u_2
x y : (a : α) → Perm (β a)
h : ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y
a : α
b : β a
⊢ ↑(x a) b = ↑(y a) b
α✝ : Type u
β✝ : Type v
α : Type u_1
β : α → Type u_2
x y : (a : α) → Perm (β a)
h : ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y
⊢ x = y
ext (a b)
no goals
case h.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : α → Type u_2
x y : (a : α) → Perm (β a)
h : ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y
a : α
b : β a
⊢ ↑(x a) b = ↑(y a) b
simpa using Equiv.congr_fun h ⟨a, b⟩