case mk.mk
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
⊢ Function.Injective ↑(sumCongrHom α β)
rintro ⟨⟩ ⟨⟩ h
case mk.mk
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
case mk.mk
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)
rw [Prod.mk.inj_iff]
case mk.mk.left.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ ↑fst✝¹ i = ↑fst✝ i

case mk.mk.right.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ ↑snd✝¹ i = ↑snd✝ i
case mk.mk
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
constructor <;> ext i
no goals
case mk.mk.left.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ ↑fst✝¹ i = ↑fst✝ i
simpa using Equiv.congr_fun h (Sum.inl i)
no goals
case mk.mk.right.H
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ ↑snd✝¹ i = ↑snd✝ i
simpa using Equiv.congr_fun h (Sum.inr i)