intro h ψ
case mpr
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
⊢ (∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ) →
    ∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
case mpr
G : Type u_2
X : Type u_1
H : Type u_3
inst✝² : Group G
inst✝¹ : ProperInvolutiveInv X
inst✝ : Group H
ι : X →⁻¹ G
ind : {H : Type u_3} → [inst : Group H] → X →⁻¹ H → G →* H
h : ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ
ψ : G →* H
⊢ ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ