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
h :
  ∀ (x : N),
    Eq (α := N)
      (((MonoidHom.ofInjective ⋯).trans
              (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) 1) (MonoidHom.ofInjective ⋯).symm) :
            (a : N) → N)
          x :
        N)
      ((1 : (a : N) → N) x : N)
⊢ (MonoidHom.ofInjective ⋯).trans
      (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) 1) (MonoidHom.ofInjective ⋯).symm) =
    1

Tactic:
ext _
-- 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
x : N
⊢ Eq (α := N)
    (((MonoidHom.ofInjective ⋯).trans
            (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) 1) (MonoidHom.ofInjective ⋯).symm) :
          (a : N) → N)
        x :
      N)
    ((1 : (a : N) → N) x : N)

Tactic:
simp only [map_one, MulEquiv.trans_apply, MulAut.one_apply, MulEquiv.symm_apply_apply]

Premises used: MulAut.one_apply, MulEquiv.trans_apply, map_one, MulEquiv.symm_apply_apply
-- 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
x x_1 : E
h :
  ∀ (x_2 : N),
    Eq (α := N)
      (((MonoidHom.ofInjective ⋯).trans
              (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) (x * x_1))
                (MonoidHom.ofInjective ⋯).symm) :
            (a : N) → N)
          x_2 :
        N)
      (((MonoidHom.ofInjective ⋯).trans
                (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) x)
                  (MonoidHom.ofInjective ⋯).symm) *
              (MonoidHom.ofInjective ⋯).trans
                (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) x_1)
                  (MonoidHom.ofInjective ⋯).symm) :
            (a : N) → N)
          x_2 :
        N)
⊢ (MonoidHom.ofInjective ⋯).trans
      (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) (x * x_1)) (MonoidHom.ofInjective ⋯).symm) =
    (MonoidHom.ofInjective ⋯).trans
        (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) x) (MonoidHom.ofInjective ⋯).symm) *
      (MonoidHom.ofInjective ⋯).trans
        (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) x_1) (MonoidHom.ofInjective ⋯).symm)

Tactic:
ext _
-- 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
x x_1 : E
x_2 : N
⊢ Eq (α := N)
    (((MonoidHom.ofInjective ⋯).trans
            (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) (x * x_1))
              (MonoidHom.ofInjective ⋯).symm) :
          (a : N) → N)
        x_2 :
      N)
    (((MonoidHom.ofInjective ⋯).trans
              (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) x) (MonoidHom.ofInjective ⋯).symm) *
            (MonoidHom.ofInjective ⋯).trans
              (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) x_1)
                (MonoidHom.ofInjective ⋯).symm) :
          (a : N) → N)
        x_2 :
      N)

Tactic:
simp only [map_mul, MulEquiv.trans_apply, MulAut.mul_apply, MulEquiv.apply_symm_apply]

Premises used: MulAut.mul_apply, MulEquiv.trans_apply, map_mul, MulEquiv.apply_symm_apply
-- 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
e : E
n : N
⊢ (S.inl : (a : N) → E) ((((S.conjAct : (a : E) → MulAut N) e : MulAut N) : (a : N) → N) n : N) =
    HMul.hMul (β := E) e ((S.inl : (a : N) → E) n : E) * e⁻¹

Tactic:
simp only [conjAct, MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.trans_apply,
    MonoidHom.apply_ofInjective_symm, MulAut.conjNormal_apply, MonoidHom.ofInjective_apply]

Premises used: OneHom.coe_mk, MulEquiv.trans_apply, MonoidHom.coe_mk, MonoidHom.ofInjective_apply, GroupExtension.conjAct, MonoidHom.apply_ofInjective_symm, MulAut.conjNormal_apply
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
x x_1 : S.Equiv S'
toMulEquiv : E ≃* E'
inl_comm :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑toMulEquiv : (a : E) → E') (⇑S.inl : (a : N) → E))
    (⇑S'.inl : (a : N) → E')
rightHom_comm :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G) (⇑toMulEquiv : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
toMulEquiv_1 : E ≃* E'
inl_comm_1 :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑toMulEquiv_1 : (a : E) → E') (⇑S.inl : (a : N) → E))
    (⇑S'.inl : (a : N) → E')
rightHom_comm_1 :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G) (⇑toMulEquiv_1 : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
h :
  Eq (α := E → E')
    (⇑{ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' }.toMulEquiv :
      (a : E) → E')
    (⇑{ toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 : S.Equiv S' }.toMulEquiv :
      (a : E) → E')
h_1 :
  Eq (α := E' → E)
    (⇑{ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' }.symm :
      (a : E') → E)
    (⇑{ toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 : S.Equiv S' }.symm :
      (a : E') → E)
e_toMulEquiv : toMulEquiv = toMulEquiv_1
⊢ { toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' } =
    { toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 }

Tactic:
congr
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
x x_1 : S.Equiv S'
toMulEquiv : E ≃* E'
inl_comm :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑toMulEquiv : (a : E) → E') (⇑S.inl : (a : N) → E))
    (⇑S'.inl : (a : N) → E')
rightHom_comm :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G) (⇑toMulEquiv : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
toMulEquiv_1 : E ≃* E'
inl_comm_1 :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑toMulEquiv_1 : (a : E) → E') (⇑S.inl : (a : N) → E))
    (⇑S'.inl : (a : N) → E')
rightHom_comm_1 :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G) (⇑toMulEquiv_1 : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
h :
  Eq (α := E → E')
    (⇑{ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' }.toMulEquiv :
      (a : E) → E')
    (⇑{ toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 : S.Equiv S' }.toMulEquiv :
      (a : E) → E')
h_1 :
  Eq (α := E' → E)
    (⇑{ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' }.symm :
      (a : E') → E)
    (⇑{ toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 : S.Equiv S' }.symm :
      (a : E') → E)
e_toMulEquiv :
  ∀ (x : E), Eq.{u_4 + 1} (α := E') ((toMulEquiv : (a : E) → E') x : E') ((toMulEquiv_1 : (a : E) → E') x : E')
⊢ toMulEquiv = toMulEquiv_1

Tactic:
rw [MulEquiv.ext_iff]

Premises used: MulEquiv.ext_iff
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
x x_1 : S.Equiv S'
toMulEquiv : E ≃* E'
inl_comm :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑toMulEquiv : (a : E) → E') (⇑S.inl : (a : N) → E))
    (⇑S'.inl : (a : N) → E')
rightHom_comm :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G) (⇑toMulEquiv : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
toMulEquiv_1 : E ≃* E'
inl_comm_1 :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑toMulEquiv_1 : (a : E) → E') (⇑S.inl : (a : N) → E))
    (⇑S'.inl : (a : N) → E')
rightHom_comm_1 :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G) (⇑toMulEquiv_1 : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
h :
  Eq (α := E → E')
    (⇑{ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' }.toMulEquiv :
      (a : E) → E')
    (⇑{ toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 : S.Equiv S' }.toMulEquiv :
      (a : E) → E')
h_1 :
  Eq (α := E' → E)
    (⇑{ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' }.symm :
      (a : E') → E)
    (⇑{ toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 : S.Equiv S' }.symm :
      (a : E') → E)
⊢ ∀ (x : E), Eq.{u_4 + 1} (α := E') ((toMulEquiv : (a : E) → E') x : E') ((toMulEquiv_1 : (a : E) → E') x : E')

Tactic:
congrFun h

Premises used: congrFun
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
x x_1 : S.Equiv S'
toMulEquiv : E ≃* E'
inl_comm :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑toMulEquiv : (a : E) → E') (⇑S.inl : (a : N) → E))
    (⇑S'.inl : (a : N) → E')
rightHom_comm :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G) (⇑toMulEquiv : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
toMulEquiv_1 : E ≃* E'
inl_comm_1 :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑toMulEquiv_1 : (a : E) → E') (⇑S.inl : (a : N) → E))
    (⇑S'.inl : (a : N) → E')
rightHom_comm_1 :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G) (⇑toMulEquiv_1 : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
h :
  Eq (α := E → E')
    (⇑{ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' }.toMulEquiv :
      (a : E) → E')
    (⇑{ toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 : S.Equiv S' }.toMulEquiv :
      (a : E) → E')
h_1 :
  Eq (α := E' → E)
    (⇑{ toMulEquiv := toMulEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm : S.Equiv S' }.symm :
      (a : E') → E)
    (⇑{ toMulEquiv := toMulEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 : S.Equiv S' }.symm :
      (a : E') → E)
⊢ ∀ (x : E), Eq.{u_4 + 1} (α := E') ((toMulEquiv : (a : E) → E') x : E') ((toMulEquiv_1 : (a : E) → E') x : E')

Tactic:
exact congrFun h

Premises used: congrFun
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ equiv.toMulEquiv = (↑equiv : E ≃* E')

Tactic:
rfl

Premises used: MulEquivClass.toMulEquiv, EquivLike.toEquiv, 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ Eq (α := (a : E) → E') (⇑(↑equiv : E ≃* E') : (a : E) → E') (⇑equiv : (a : E) → 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
n : N
⊢ Eq.{u_4 + 1} (α := E') ((equiv : (a : E) → E') ((S.inl : (a : N) → E) n : E) : E') ((S'.inl : (a : N) → E') n : E')

Tactic:
congrFun equiv.inl_comm n

Premises used: GroupExtension.Equiv.inl_comm, congrFun
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
e : E
⊢ Eq.{u_3 + 1} (α := G) ((S'.rightHom : (a : E') → G) ((equiv : (a : E) → E') e : E') : G)
    ((S.rightHom : (a : E) → G) e : G)

Tactic:
congrFun equiv.rightHom_comm e

Premises used: GroupExtension.Equiv.rightHom_comm, congrFun
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
rw :
  Eq (α := N → E') (⇑S'.inl : (a : N) → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑equiv.toMulEquiv : (a : E) → E') (⇑S.inl : (a : N) → E))
rw₁ rw₂ :
  Eq (α := N → E')
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑equiv.toMulEquiv : (a : E) → E') (⇑S.inl : (a : N) → E))
    (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑equiv.toMulEquiv : (a : E) → E') (⇑S.inl : (a : N) → E))
⊢ Eq (α := N → E)
    (Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := E') (⇑equiv.symm : (a : E') → E) (⇑S'.inl : (a : N) → E'))
    (⇑S.inl : (a : N) → E)

Tactic:
rw [MulEquiv.symm_comp_eq, ← equiv.inl_comm]

Premises used: GroupExtension.Equiv.inl_comm, MulEquiv.symm_comp_eq
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
rw :
  Eq (α := E → G) (⇑S.rightHom : (a : E) → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G)
      (⇑equiv.toMulEquiv : (a : E) → E'))
rw₁ rw₂ :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G)
      (⇑equiv.toMulEquiv : (a : E) → E'))
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G)
      (⇑equiv.toMulEquiv : (a : E) → E'))
⊢ Eq (α := E' → G)
    (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑S.rightHom : (a : E) → G) (⇑equiv.symm : (a : E') → E))
    (⇑S'.rightHom : (a : E') → G)

Tactic:
rw [MulEquiv.comp_symm_eq, ← equiv.rightHom_comm]

Premises used: MulEquiv.comp_symm_eq, GroupExtension.Equiv.rightHom_comm
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ Eq (α := E' ≃* E) (MulEquiv.symm (↑equiv : E ≃* E')) (↑equiv.symm : E' ≃* E)

Tactic:
rfl

Premises used: Equiv.symm, MulEquiv.symm, MulEquivClass.toMulEquiv, EquivLike.toEquiv, 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
E'' : Type u_5
inst_4 : Group E''
S'' : GroupExtension N E'' G
equiv' : S'.Equiv S''
rw :
  Eq (α := N → E'')
    (Function.comp.{u_1 + 1, u_2 + 1, u_5 + 1} (β := E)
      (Function.comp.{u_2 + 1, u_4 + 1, u_5 + 1} (β := E') (⇑equiv'.toMulEquiv : (a : E') → E'')
        (⇑equiv.toMulEquiv : (a : E) → E'))
      (⇑S.inl : (a : N) → E))
    (⇑S''.inl : (a : N) → E'')
rw₁ :
  Eq (α := N → E'')
    (Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := E') (⇑equiv'.toMulEquiv : (a : E') → E'')
      (Function.comp.{u_1 + 1, u_2 + 1, u_4 + 1} (β := E) (⇑equiv.toMulEquiv : (a : E) → E') (⇑S.inl : (a : N) → E)))
    (⇑S''.inl : (a : N) → E'')
rw₂ :
  Eq (α := N → E'')
    (Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := E') (⇑equiv'.toMulEquiv : (a : E') → E'') (⇑S'.inl : (a : N) → E'))
    (⇑S''.inl : (a : N) → E'')
rw₃ rw₄ : Eq (α := N → E'') (⇑S''.inl : (a : N) → E'') (⇑S''.inl : (a : N) → E'')
⊢ Eq (α := N → E'')
    (Function.comp.{u_1 + 1, u_2 + 1, u_5 + 1} (β := E) (⇑(equiv.trans equiv'.toMulEquiv) : (a : E) → E'')
      (⇑S.inl : (a : N) → E))
    (⇑S''.inl : (a : N) → E'')

Tactic:
rw [MulEquiv.coe_trans, Function.comp_assoc, equiv.inl_comm, equiv'.inl_comm]

Premises used: MulEquiv.coe_trans, GroupExtension.Equiv.inl_comm, Function.comp_assoc
-- 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
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
E'' : Type u_5
inst_4 : Group E''
S'' : GroupExtension N E'' G
equiv' : S'.Equiv S''
rw :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_5 + 1, u_3 + 1} (β := E'') (⇑S''.rightHom : (a : E'') → G)
      (Function.comp.{u_2 + 1, u_4 + 1, u_5 + 1} (β := E') (⇑equiv'.toMulEquiv : (a : E') → E'')
        (⇑equiv.toMulEquiv : (a : E) → E')))
    (⇑S.rightHom : (a : E) → G)
rw₁ :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E')
      (Function.comp.{u_4 + 1, u_5 + 1, u_3 + 1} (β := E'') (⇑S''.rightHom : (a : E'') → G)
        (⇑equiv'.toMulEquiv : (a : E') → E''))
      (⇑equiv.toMulEquiv : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
rw₂ :
  Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_4 + 1, u_3 + 1} (β := E') (⇑S'.rightHom : (a : E') → G)
      (⇑equiv.toMulEquiv : (a : E) → E'))
    (⇑S.rightHom : (a : E) → G)
rw₃ rw₄ : Eq (α := E → G) (⇑S.rightHom : (a : E) → G) (⇑S.rightHom : (a : E) → G)
⊢ Eq (α := E → G)
    (Function.comp.{u_2 + 1, u_5 + 1, u_3 + 1} (β := E'') (⇑S''.rightHom : (a : E'') → G)
      (⇑(equiv.trans equiv'.toMulEquiv) : (a : E) → E''))
    (⇑S.rightHom : (a : E) → G)

Tactic:
rw [MulEquiv.coe_trans, ← Function.comp_assoc, equiv'.rightHom_comm, equiv.rightHom_comm]

Premises used: MulEquiv.coe_trans, GroupExtension.Equiv.rightHom_comm, Function.comp_assoc
-- 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
x x_1 : S.Section
toFun : G → E
rightInverse_rightHom : Function.RightInverse toFun (⇑S.rightHom : (a : E) → G)
toFun_1 : G → E
rightInverse_rightHom_1 : Function.RightInverse toFun_1 (⇑S.rightHom : (a : E) → G)
h :
  { toFun := toFun, rightInverse_rightHom := rightInverse_rightHom : S.Section }.toFun =
    { toFun := toFun_1, rightInverse_rightHom := rightInverse_rightHom_1 : S.Section }.toFun
⊢ { toFun := toFun, rightInverse_rightHom := rightInverse_rightHom : S.Section } =
    { toFun := toFun_1, rightInverse_rightHom := rightInverse_rightHom_1 }

Tactic:
congr
-- 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
σ : G → E
hσ : Function.RightInverse σ (⇑S.rightHom : (a : E) → G)
⊢ (⇑{ toFun := σ, rightInverse_rightHom := hσ : S.Section } : (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.Section
g : G
⊢ (S.rightHom : (a : E) → G) ((σ : (a : G) → E) g : E) = g

Tactic:
σ.rightInverse_rightHom g

Premises used: GroupExtension.Section.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.Section
⊢ Eq.{u_3 + 1} (α := G → G)
    (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑S.rightHom : (a : E) → G) (⇑σ : (a : G) → E)) id

Tactic:
σ.rightInverse_rightHom.comp_eq_id

Premises used: Function.RightInverse.comp_eq_id, GroupExtension.Section.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
toMonoidHom : G →* E
rightInverse_rightHom : Function.RightInverse (↑toMonoidHom : OneHom G E).toFun (⇑S.rightHom : (a : E) → G)
this :
  ∀ (toMonoidHom_1 : G →* E)
    (rightInverse_rightHom_1 : Function.RightInverse (↑toMonoidHom_1 : OneHom G E).toFun (⇑S.rightHom : (a : E) → G)),
    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, rightInverse_rightHom := rightInverse_rightHom : S.Splitting } =
        { toMonoidHom := toMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 }
⊢ ∀ ⦃a₂ : S.Splitting⦄,
    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) a₂) →
      { toMonoidHom := toMonoidHom, rightInverse_rightHom := rightInverse_rightHom : S.Splitting } = a₂

Tactic:
⟨_, _⟩
-- 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 })
e_toMonoidHom : toMonoidHom = toMonoidHom_1
⊢ { toMonoidHom := toMonoidHom, rightInverse_rightHom := rightInverse_rightHom : S.Splitting } =
    { toMonoidHom := toMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 }

Tactic:
congr
-- 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:
DFunLike.coe_injective h

Premises used: DFunLike.coe_injective