awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
toMonoidHom : G →* E
rightInverse_rightHom : Function.RightInverse (↑toMonoidHom : OneHom G E).toFun (⇑S.rightHom : (a : E) → G)
toMonoidHom_1 : G →* E
rightInverse_rightHom_1 : Function.RightInverse (↑toMonoidHom_1 : OneHom G E).toFun (⇑S.rightHom : (a : E) → G)
h :
  Eq (α := (a : G) → E)
    ((fun (s : S.Splitting) ↦ (↑s.toMonoidHom : OneHom G E).toFun)
      { toMonoidHom := toMonoidHom, rightInverse_rightHom := rightInverse_rightHom })
    ((fun (s : S.Splitting) ↦ (↑s.toMonoidHom : OneHom G E).toFun)
      { toMonoidHom := toMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 })
⊢ toMonoidHom = toMonoidHom_1

Tactic:
exact DFunLike.coe_injective h

Premises used: DFunLike.coe_injective
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
s : G →* E
hs : Function.RightInverse.{u_2 + 1, u_3 + 1} (α := E) (β := G) (⇑s : (a : G) → E) (⇑S.rightHom : (a : E) → G)
⊢ Eq (α := (a : G) → E) (⇑{ toMonoidHom := s, rightInverse_rightHom := hs : S.Splitting } : (a : G) → E)
    (⇑s : (a : G) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
s : G →* E
hs : Function.RightInverse.{u_2 + 1, u_3 + 1} (α := E) (β := G) (⇑s : (a : G) → E) (⇑S.rightHom : (a : E) → G)
⊢ (↑{ toMonoidHom := s, rightInverse_rightHom := hs : S.Splitting } : G →* E) = s

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
s : S.Splitting
g : G
⊢ (S.rightHom : (a : E) → G) ((s : (a : G) → E) g : E) = g

Tactic:
s.rightInverse_rightHom g

Premises used: GroupExtension.Splitting.rightInverse_rightHom
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
s : S.Splitting
h : ∀ (g : G), Eq (α := G) ((S.rightHom.comp (↑s : G →* E) : (a : G) → G) g : G) ((MonoidHom.id G : (a : G) → G) g : G)
⊢ S.rightHom.comp (↑s : G →* E) = MonoidHom.id G

Tactic:
ext g
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
s : S.Splitting
g : G
⊢ Eq (α := G) ((S.rightHom.comp (↑s : G →* E) : (a : G) → G) g : G) ((MonoidHom.id G : (a : G) → G) g : G)

Tactic:
simp only [MonoidHom.comp_apply, MonoidHom.id_apply, MonoidHom.coe_coe, rightHom_splitting]

Premises used: MonoidHom.coe_coe, MonoidHom.id_apply, GroupExtension.Splitting.rightHom_splitting, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
G : Type u_3
inst : Group G
inst_1 : Group N
φ : MonoidHom.{u_3, u_1} G (MulAut N)
⊢ (toGroupExtension φ).inl = inl

Tactic:
rfl

Premises used: SemidirectProduct.inl, rfl
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
G : Type u_3
inst : Group G
inst_1 : Group N
φ : MonoidHom.{u_3, u_1} G (MulAut N)
⊢ (toGroupExtension φ).rightHom = rightHom

Tactic:
rfl

Premises used: SemidirectProduct.rightHom, rfl
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
⊢ Group (HNNExtension.con G A B φ).Quotient

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ (fun (x1 x2 : G ∗ Multiplicative ℤ) ↦ x1 * x2)
        ((inr : (a : Multiplicative ℤ) → G ∗ Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1))
        ((inl : (a : G) → G ∗ Multiplicative ℤ) (↑a : G)) =
      HMul.hMul (α := G ∗ Multiplicative ℤ) (β := G ∗ Multiplicative ℤ)
        ((inr : (a : Multiplicative ℤ) → G ∗ Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1) :
          G ∗ Multiplicative ℤ)
        ((inl : (a : G) → G ∗ Multiplicative ℤ) (↑a : G) : G ∗ Multiplicative ℤ) ∧
    (fun (x1 x2 : G ∗ Multiplicative ℤ) ↦ x1 * x2)
        ((inl : (a : G) → G ∗ Multiplicative ℤ) (↑((φ : (a : ↥A) → ↥B) a) : G))
        ((inr : (a : Multiplicative ℤ) → G ∗ Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1)) =
      HMul.hMul (α := G ∗ Multiplicative ℤ) (β := G ∗ Multiplicative ℤ)
        ((inl : (a : G) → G ∗ Multiplicative ℤ) (↑((φ : (a : ↥A) → ↥B) a) : G))
        ((inr : (a : Multiplicative ℤ) → G ∗ Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1) :
          G ∗ Multiplicative ℤ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
rw :
  HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) t =
    HMul.hMul (α := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) ((φ.symm : (a : ↥B) → ↥A) b)) : G)) t
⊢ HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) t =
    HMul.hMul (α := HNNExtension G A B φ) t ((of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G))

Tactic:
rw [t_mul_of]

Premises used: HNNExtension.t_mul_of
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) t =
    HMul.hMul (α := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) ((φ.symm : (a : ↥B) → ↥A) b)) : G)) t

Tactic:
simp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
rw :
  (of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) a) : G) =
    HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) a) : G)) t * t⁻¹
⊢ (of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) a) : G) =
    HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t
        ((of : (a : G) → HNNExtension G A B φ) (↑a : G) : HNNExtension G A B φ) *
      t⁻¹

Tactic:
rw [t_mul_of]

Premises used: HNNExtension.t_mul_of
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ (of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) a) : G) =
    HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) a) : G)) t * t⁻¹

Tactic:
simp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
rw :
  (of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G) =
    t⁻¹ *
      HMul.hMul (α := HNNExtension G A B φ) t
        ((of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G))
⊢ (of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G) =
    HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t⁻¹
        ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) *
      t

Tactic:
rw [mul_assoc, of_mul_t]

Premises used: mul_assoc, HNNExtension.of_mul_t
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ (of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G) =
    t⁻¹ *
      HMul.hMul (α := HNNExtension G A B φ) t
        ((of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G))

Tactic:
simp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
rw :
  HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t⁻¹
      ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) =
    HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t⁻¹
          ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) *
        t *
      t⁻¹
⊢ HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t⁻¹
      ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) =
    HMul.hMul (α := HNNExtension G A B φ) ((of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G))
      t⁻¹

Tactic:
rw [equiv_symm_eq_conj]

Premises used: HNNExtension.equiv_symm_eq_conj
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t⁻¹
      ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) =
    HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t⁻¹
          ((of : (a : G) → HNNExtension G A B φ) (↑b : G) : HNNExtension G A B φ) *
        t *
      t⁻¹

Tactic:
simp
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
rw :
  HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑a : G) : HNNExtension G A B φ) t⁻¹ =
    t⁻¹ *
      (HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t
          ((of : (a : G) → HNNExtension G A B φ) (↑a : G) : HNNExtension G A B φ) *
        t⁻¹)
⊢ HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑a : G) : HNNExtension G A B φ) t⁻¹ =
    HMul.hMul (α := HNNExtension G A B φ) t⁻¹ ((of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) a) : G))

Tactic:
rw [equiv_eq_conj]

Premises used: HNNExtension.equiv_eq_conj
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ)
      ((of : (a : G) → HNNExtension G A B φ) (↑a : G) : HNNExtension G A B φ) t⁻¹ =
    t⁻¹ *
      (HMul.hMul (α := HNNExtension G A B φ) (β := HNNExtension G A B φ) t
          ((of : (a : G) → HNNExtension G A B φ) (↑a : G) : HNNExtension G A B φ) *
        t⁻¹)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
M : Type u_3
inst_2 : Monoid M
f : G →* H
x : H
hx :
  ∀ (a : ↥A),
    HMul.hMul (β := H) x ((f : (a : G) → H) (↑a : G) : H) =
      HMul.hMul (α := H) ((f : (a : G) → H) (↑((φ : (a : ↥A) → ↥B) a) : G) : H) x
a : ↥A
⊢ (Con.ker (F := MonoidHom.{u_1, u_2} (G ∗ Multiplicative ℤ) H)
        (Coprod.lift f ((zpowersHom H : (a : H) → Multiplicative ℤ →* H) x)) :
      (a : G ∗ Multiplicative ℤ) → G ∗ Multiplicative ℤ → Prop)
    (HMul.hMul (α := G ∗ Multiplicative ℤ) (β := G ∗ Multiplicative ℤ)
      ((inr : (a : Multiplicative ℤ) → G ∗ Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1) :
        G ∗ Multiplicative ℤ)
      ((inl : (a : G) → G ∗ Multiplicative ℤ) (↑a : G) : G ∗ Multiplicative ℤ))
    (HMul.hMul (α := G ∗ Multiplicative ℤ) (β := G ∗ Multiplicative ℤ)
      ((inl : (a : G) → G ∗ Multiplicative ℤ) (↑((φ : (a : ↥A) → ↥B) a) : G))
      ((inr : (a : Multiplicative ℤ) → G ∗ Multiplicative ℤ) ((ofAdd : (a : ℤ) → Multiplicative ℤ) 1) :
        G ∗ Multiplicative ℤ))

Tactic:
simp [hx]
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
f : G →* H
x : H
hx :
  ∀ (a : ↥A),
    HMul.hMul (β := H) x ((f : (a : G) → H) (↑a : G) : H) =
      HMul.hMul (α := H) ((f : (a : G) → H) (↑((φ : (a : ↥A) → ↥B) a) : G) : H) x
delta : (lift f x hx : (a : (con G A B φ).Quotient) → H) t = x
⊢ (lift f x hx : (a : HNNExtension G A B φ) → H) t = x

Tactic:
delta HNNExtension

Premises used: HNNExtension
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
f : G →* H
x : H
hx :
  ∀ (a : ↥A),
    HMul.hMul (β := H) x ((f : (a : G) → H) (↑a : G) : H) =
      HMul.hMul (α := H) ((f : (a : G) → H) (↑((φ : (a : ↥A) → ↥B) a) : G) : H) x
⊢ (lift f x hx : (a : (con G A B φ).Quotient) → H) t = x

Tactic:
simp [lift, t]

Premises used: HNNExtension.t, HNNExtension.lift
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
f : G →* H
x : H
hx :
  ∀ (a : ↥A),
    HMul.hMul (β := H) x ((f : (a : G) → H) (↑a : G) : H) =
      HMul.hMul (α := H) ((f : (a : G) → H) (↑((φ : (a : ↥A) → ↥B) a) : G) : H) x
g : G
delta :
  Eq.{u_2 + 1} (α := H)
    ((lift f x hx : (a : (con G A B φ).Quotient) → H)
        ((of : (a : G) → (con G A B φ).Quotient) g : (con G A B φ).Quotient) :
      H)
    ((f : (a : G) → H) g : H)
⊢ Eq.{u_2 + 1} (α := H)
    ((lift f x hx : (a : HNNExtension G A B φ) → H) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ) :
      H)
    ((f : (a : G) → H) g : H)

Tactic:
delta HNNExtension

Premises used: HNNExtension
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst_1 : Group H
f : G →* H
x : H
hx :
  ∀ (a : ↥A),
    HMul.hMul (β := H) x ((f : (a : G) → H) (↑a : G) : H) =
      HMul.hMul (α := H) ((f : (a : G) → H) (↑((φ : (a : ↥A) → ↥B) a) : G) : H) x
g : G
⊢ Eq.{u_2 + 1} (α := H)
    ((lift f x hx : (a : (con G A B φ).Quotient) → H)
        ((of : (a : G) → (con G A B φ).Quotient) g : (con G A B φ).Quotient) :
      H)
    ((f : (a : G) → H) g : H)

Tactic:
simp [lift, of]

Premises used: HNNExtension.of, HNNExtension.lift
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
M : Type u_3
inst_1 : Monoid M
f g : MonoidHom.{u_1, u_3} (HNNExtension G A B φ) M
hg : f.comp of = g.comp of
ht : Eq.{u_3 + 1} (α := M) ((f : (a : HNNExtension G A B φ) → M) t : M) ((g : (a : HNNExtension G A B φ) → M) t : M)
⊢ f = g

Tactic:
(MonoidHom.cancel_right Con.mk'_surjective).mp <|
    Coprod.hom_ext hg (MonoidHom.ext_mint ht)

Premises used: Con.mk'_surjective, HNNExtension, Iff.mp, Monoid.Coprod.hom_ext, MonoidHom.cancel_right, MonoidHom.ext_mint
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
⊢ 1 ∈ setOf motive

Tactic:
simpa using of 1

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
let : motive x
⊢ motive x

Tactic:
let S : Subgroup (HNNExtension G A B φ) :=
    { carrier := setOf motive
      one_mem' := by simpa using of 1
      mul_mem' := mul _ _
      inv_mem' := inv _ }
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
a : ↥A
a₁ :
  (↑(HMul.hMul (β := ↥S) (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t)
          (((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑a : G) : ↥S)) :
      HNNExtension G A B φ) =
    (↑(((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑((φ : (a : ↥A) → ↥B) a) : G) *
          Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) :
      HNNExtension G A B φ)
⊢ HMul.hMul (β := ↥S) (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t)
      (((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑a : G) : ↥S) =
    ((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑((φ : (a : ↥A) → ↥B) a) : G) *
      Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t

Tactic:
ext
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
a : ↥A
⊢ (↑(HMul.hMul (β := ↥S) (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t)
          (((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑a : G) : ↥S)) :
      HNNExtension G A B φ) =
    (↑(((MonoidHom.codRestrict HNNExtension.of S of : G →* ↥S) : (a : G) → ↥S) (↑((φ : (a : ↥A) → ↥B) a) : G) *
          Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) :
      HNNExtension G A B φ)

Tactic:
simp [equiv_eq_conj, mul_assoc]

Premises used: HNNExtension.equiv_eq_conj, mul_assoc
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S :=
  lift (MonoidHom.codRestrict HNNExtension.of S of)
    (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) ⋯
h :
  ∀ (x : G),
    Eq (α := HNNExtension G A B φ)
      (((S.subtype.comp f).comp HNNExtension.of : (a : G) → HNNExtension G A B φ) x : HNNExtension G A B φ)
      ((MonoidHom.comp (MonoidHom.id (HNNExtension G A B φ)) HNNExtension.of : (a : G) → HNNExtension G A B φ) x :
        HNNExtension G A B φ)
⊢ (S.subtype.comp f).comp HNNExtension.of = MonoidHom.comp (MonoidHom.id (HNNExtension G A B φ)) HNNExtension.of

Tactic:
ext
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S :=
  lift (MonoidHom.codRestrict HNNExtension.of S of)
    (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) ⋯
x_1 : G
⊢ Eq (α := HNNExtension G A B φ)
    (((S.subtype.comp f).comp HNNExtension.of : (a : G) → HNNExtension G A B φ) x_1 : HNNExtension G A B φ)
    ((MonoidHom.comp (MonoidHom.id (HNNExtension G A B φ)) HNNExtension.of : (a : G) → HNNExtension G A B φ) x_1 :
      HNNExtension G A B φ)

Tactic:
simp [f]
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S :=
  lift (MonoidHom.codRestrict HNNExtension.of S of)
    (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) ⋯
⊢ Eq (α := HNNExtension G A B φ)
    ((S.subtype.comp f : (a : HNNExtension G A B φ) → HNNExtension G A B φ) HNNExtension.t : HNNExtension G A B φ)
    ((MonoidHom.id (HNNExtension G A B φ) : (a : HNNExtension G A B φ) → HNNExtension G A B φ) HNNExtension.t :
      HNNExtension G A B φ)

Tactic:
simp [f]
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S :=
  lift (MonoidHom.codRestrict HNNExtension.of S of)
    (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) ⋯
⊢ S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)

Tactic:
have hf : S.subtype.comp f = MonoidHom.id _ :=
    hom_ext (by ext; simp [f]) (by simp [f])
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S :=
  lift (MonoidHom.codRestrict HNNExtension.of S of)
    (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) ⋯
hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)
change : motive ((MonoidHom.id (HNNExtension G A B φ) : (a : HNNExtension G A B φ) → HNNExtension G A B φ) x)
⊢ motive x

Tactic:
change motive (MonoidHom.id _ x)

Premises used: MonoidHom.id, DFunLike.coe
-- Module: Mathlib.GroupTheory.HNNExtension
Goal:
G : Type u_1
inst : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive ((HNNExtension.of : (a : G) → HNNExtension G A B φ) g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := setOf motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S :=
  lift (MonoidHom.codRestrict HNNExtension.of S of)
    (Subtype.mk (p := fun (x : HNNExtension G A B φ) ↦ x ∈ S) HNNExtension.t t) ⋯
hf : S.subtype.comp f = MonoidHom.id (HNNExtension G A B φ)
rw : motive ((S.subtype.comp f : (a : HNNExtension G A B φ) → HNNExtension G A B φ) x)
⊢ motive ((MonoidHom.id (HNNExtension G A B φ) : (a : HNNExtension G A B φ) → HNNExtension G A B φ) x)

Tactic:
rw [← hf]