Theorem: SymmFreeGroup.induced_restrict_eq_iff_lift_unique (GroupComp/SymmFreeGroup.lean)

State before:
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
⊢ (∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ) ↔
    ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ
Tactic:
constructor
State after:
case mp
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
⊢ (∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ) →
    ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ

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 ψ)) = ψ

State before:
case mp
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
⊢ (∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ) →
    ∀ (φ : X →⁻¹ H) (ψ : G →* H), InvHom.comp ι (MonoidHom.toInvHom ψ) = φ → ind φ = ψ
Tactic:
intro h φ ψ hres
State after:
case mp
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 : ∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
φ : X →⁻¹ H
ψ : G →* H
hres : InvHom.comp ι (MonoidHom.toInvHom ψ) = φ
⊢ ind φ = ψ

State before:
case mp
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 : ∀ (ψ : G →* H), ind (InvHom.comp ι (MonoidHom.toInvHom ψ)) = ψ
φ : X →⁻¹ H
ψ : G →* H
hres : InvHom.comp ι (MonoidHom.toInvHom ψ) = φ
⊢ ind φ = ψ
Tactic:
exact hres ▸ (h ψ)
State after:
no goals

State before:
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 ψ)) = ψ
Tactic:
intro h ψ
State after:
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 ψ)) = ψ

State before:
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 ψ)) = ψ
Tactic:
exact h (ι.comp ψ.toInvHom) ψ rfl
State after:
no goals