awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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)
⊢ { 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 }
have e_toMulEquiv : toMulEquiv = toMulEquiv_1
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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)
⊢ toMulEquiv = toMulEquiv_1
have e_toMulEquiv : ∀ (x : E), Eq.{u_4 + 1} (α := E') ((toMulEquiv : (a : E) → E') x : E') ((toMulEquiv_1 : (a : E) → E') x : E')
Tactic: rw [MulEquiv.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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 (α := 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)
have 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))
Tactic: rw [MulEquiv.symm_comp_eq, ← equiv.inl_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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))
⊢ 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)
have 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))
Tactic: rw [MulEquiv.symm_comp_eq, ← equiv.inl_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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' → 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)
have 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'))
Tactic: rw [MulEquiv.comp_symm_eq, ← equiv.rightHom_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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'))
⊢ 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)
have 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'))
Tactic: rw [MulEquiv.comp_symm_eq, ← equiv.rightHom_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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''
⊢ 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'')
have 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'')
Tactic: rw [MulEquiv.coe_trans, Function.comp_assoc, equiv.inl_comm, equiv'.inl_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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'')
⊢ 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'')
have 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'')
Tactic: rw [MulEquiv.coe_trans, Function.comp_assoc, equiv.inl_comm, equiv'.inl_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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'')
⊢ 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'')
have 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'')
Tactic: rw [MulEquiv.coe_trans, Function.comp_assoc, equiv.inl_comm, equiv'.inl_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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'')
⊢ 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'')
have rw₃ : Eq (α := N → 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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''
⊢ 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)
have 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)
Tactic: rw [MulEquiv.coe_trans, ← Function.comp_assoc, equiv'.rightHom_comm, equiv.rightHom_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [MulEquiv.coe_trans, ← Function.comp_assoc, equiv'.rightHom_comm, equiv.rightHom_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: rw [MulEquiv.coe_trans, ← Function.comp_assoc, equiv'.rightHom_comm, equiv.rightHom_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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)
⊢ 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)
have rw₃ : Eq (α := E → G) (⇑S.rightHom : (a : E) → G) (⇑S.rightHom : (a : E) → G)
Tactic: rw [MulEquiv.coe_trans, ← Function.comp_assoc, equiv'.rightHom_comm, equiv.rightHom_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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)
⊢ ∀ ⦃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₂
have 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 }
Tactic: ⟨_, _⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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, rightInverse_rightHom := rightInverse_rightHom : S.Splitting } =
    { toMonoidHom := toMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 }
have e_toMonoidHom : toMonoidHom = toMonoidHom_1
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Defs (goal)
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
⊢ S.rightHom.comp (↑s : G →* E) = MonoidHom.id G
have h : ∀ (g : G), Eq (α := G) ((S.rightHom.comp (↑s : G →* E) : (a : G) → G) g : G) ((MonoidHom.id G : (a : G) → G) g : G)
Tactic: ext g
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 φ) t ((of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G))
have 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
Tactic: rw [t_mul_of]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 φ) (β := HNNExtension G A B φ) t
        ((of : (a : G) → HNNExtension G A B φ) (↑a : G) : HNNExtension G A B φ) *
      t⁻¹
have 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⁻¹
Tactic: rw [t_mul_of]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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) =
    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
have 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))
Tactic: rw [mul_assoc, of_mul_t]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 φ) ((of : (a : G) → HNNExtension G A B φ) (↑((φ.symm : (a : ↥B) → ↥A) b) : G))
      t⁻¹
have 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⁻¹
Tactic: rw [equiv_symm_eq_conj]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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⁻¹ =
    HMul.hMul (α := HNNExtension G A B φ) t⁻¹ ((of : (a : G) → HNNExtension G A B φ) (↑((φ : (a : ↥A) → ↥B) a) : G))
have 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⁻¹)
Tactic: rw [equiv_eq_conj]
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 : HNNExtension G A B φ) → H) t = x
have delta : (lift f x hx : (a : (con G A B φ).Quotient) → H) t = x
Tactic: delta HNNExtension
-- Lean 4 proof step from Mathlib.GroupTheory.HNNExtension (goal)
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 : HNNExtension G A B φ) → H) ((of : (a : G) → HNNExtension G A B φ) g : HNNExtension G A B φ) :
      H)
    ((f : (a : G) → H) g : H)
have 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)
Tactic: delta HNNExtension