awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
obtain :
  ∀ (n : N)
    (hn :
      (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E)),
    ∃ (n : N),
      (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((σ' : (a : G) → E) g : E) ((S.inl : (a : N) → E) n : E)
⊢ ∃ (n : N), (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((σ' : (a : G) → E) g : E) ((S.inl : (a : N) → E) n : E)

Tactic:
obtain ⟨n, hn⟩ := inv_mul_mem_range_inl σ' σ g

Premises used: GroupExtension.Section.inv_mul_mem_range_inl
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E)
rw :
  (σ : (a : G) → E) g =
    HMul.hMul (α := E) ((σ' : (a : G) → E) g : E)
      (HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E))
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) ((σ : (a : G) → E) g : E) ((σ : (a : G) → E) g : E)
⊢ (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((σ' : (a : G) → E) g : E) ((S.inl : (a : N) → E) n : E)

Tactic:
rw [hn, mul_inv_cancel_left]

Premises used: mul_inv_cancel_left
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E)
⊢ ∃ (n : N), (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((σ' : (a : G) → E) g : E) ((S.inl : (a : N) → E) n : E)

Tactic:
exact ⟨n, by rw [hn, mul_inv_cancel_left]⟩
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
⊢ HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) ∈
    S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
    mul_inv_cancel]

Premises used: map_inv, GroupExtension.Section.rightHom_section, MonoidHom.mem_ker, map_mul, mul_inv_cancel, GroupExtension.range_inl_eq_ker_rightHom
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
⊢ HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E) ∈
    S.inl.range

Tactic:
simp only [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, rightHom_section,
    mul_assoc, inv_mul_cancel]

Premises used: inv_mul_cancel, map_inv, mul_assoc, GroupExtension.Section.rightHom_section, MonoidHom.mem_ker, map_mul, GroupExtension.range_inl_eq_ker_rightHom
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
obtain :
  ∀ (n : N)
    (hn :
      (S.inl : (a : N) → E) n =
        HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
          (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)),
    ∃ (n : N),
      (σ : (a : G) → E) (g₁ * g₂) =
        HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) g₁ : E))
          ((σ : (a : G) → E) g₂ : E)
⊢ ∃ (n : N),
    (σ : (a : G) → E) (g₁ * g₂) =
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) g₁ : E))
        ((σ : (a : G) → E) g₂ : E)

Tactic:
obtain ⟨n, hn⟩ := mul_mul_mul_inv_mem_range_inl σ g₁ g₂

Premises used: GroupExtension.Section.mul_mul_mul_inv_mem_range_inl
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
h :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
⊢ ∃ (n : N),
    (σ : (a : G) → E) (g₁ * g₂) =
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) g₁ : E))
        ((σ : (a : G) → E) g₂ : E)

Tactic:
use n⁻¹
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
h :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (α := E) ((S.inl : (a : N) → E) n⁻¹ : E)
      (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
h₁ :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (α := E) (((S.inl : (a : N) → E) n)⁻¹ : E)
      (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
h₂ :
  HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) (g₁ * g₂) : E) =
    HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E)
h₃ :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
h₄ h₅ :
  HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
⊢ (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)

Tactic:
rw [mul_assoc, map_inv, eq_inv_mul_iff_mul_eq, ← eq_mul_inv_iff_mul_eq, hn]

Premises used: map_inv, mul_assoc, eq_inv_mul_iff_mul_eq, eq_mul_inv_iff_mul_eq
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
obtain :
  ∀ (n : N)
    (hn :
      (S.inl : (a : N) → E) n =
        HMul.hMul (β := E)
          (HMul.hMul (α := E) (β := E) (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
          ((σ : (a : G) → E) g₂ : E)),
    ∃ (n : N),
      (σ : (a : G) → E) (g₁ * g₂) =
        HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
          ((S.inl : (a : N) → E) n : E)
⊢ ∃ (n : N),
    (σ : (a : G) → E) (g₁ * g₂) =
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
        ((S.inl : (a : N) → E) n : E)

Tactic:
obtain ⟨n, hn⟩ := mul_inv_mul_mul_mem_range_inl σ g₁ g₂

Premises used: GroupExtension.Section.mul_inv_mul_mul_mem_range_inl
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
h :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      ((S.inl : (a : N) → E) n⁻¹ : E)
⊢ ∃ (n : N),
    (σ : (a : G) → E) (g₁ * g₂) =
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
        ((S.inl : (a : N) → E) n : E)

Tactic:
use n⁻¹
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
h :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((S.inl : (a : N) → E) n)⁻¹ : E)
h₁ :
  HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) (g₁ * g₂) : E) ((S.inl : (a : N) → E) n : E) =
    HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E)
h₂ :
  (S.inl : (a : N) → E) n =
    HMul.hMul (α := E) (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
      (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
h₃ :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
h₄ h₅ :
  HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
⊢ (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      ((S.inl : (a : N) → E) n⁻¹ : E)

Tactic:
rw [map_inv, eq_mul_inv_iff_mul_eq, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, hn]

Premises used: map_inv, mul_assoc, eq_inv_mul_iff_mul_eq, eq_mul_inv_iff_mul_eq
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
σ σ' : S.Section
g_1 g₁ g₂ : G
equiv : S.Equiv S'
g : G
rw : (S'.rightHom : (a : E') → G) ((equiv : (a : E) → E') ((σ : (a : G) → E) g : E) : E') = g
rw₁ : (S.rightHom : (a : E) → G) ((σ : (a : G) → E) g : E) = g
rw₂ rw₃ : g = g
⊢ (S'.rightHom : (a : E') → G)
      (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑equiv : (a : E) → E') (⇑σ : (a : G) → E) g) =
    g

Tactic:
rw [Function.comp_apply, equiv.rightHom_map, rightHom_section]

Premises used: GroupExtension.Section.rightHom_section, GroupExtension.Equiv.rightHom_map, Function.comp_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
simp :
  HMul.hMul (β := E) (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))
      ((S.inl : (a : N) → E)
          (Function.invFun.{u_1 + 1, u_4 + 1} (β := E') ((⇑S'.inl : (a : N) → E') : (a : N) → E')
            ((f : (a : E) → E')
                ((Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e) :
              E')) :
        E) =
    e
⊢ (fun (e' : E') ↦
        let e := Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e');
        HMul.hMul (β := E) e
          ((S.inl : (a : N) → E)
              (Function.invFun (⇑S'.inl : (a : N) → E') (HMul.hMul (α := E') (((f : (a : E) → E') e)⁻¹ : E') e')) :
            E))
      ((↑f : OneHom E E').toFun e) =
    e

Tactic:
simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, ← map_inv, ← map_mul]

Premises used: map_inv, MonoidHom.toOneHom_coe, map_mul, OneHom.toFun_eq_coe
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
rw :
  HMul.hMul (α := G) (β := G) (((S.rightHom : (a : E) → G) (Function.surjInv ⋯ ((S.rightHom : (a : E) → G) e)))⁻¹ : G)
      ((S.rightHom : (a : E) → G) e : G) =
    1
⊢ (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e ∈ S.inl.range

Tactic:
rw [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, ← MonoidHom.comp_apply,
        rightHom_comp]

Premises used: map_inv, MonoidHom.mem_ker, map_mul, GroupExtension.range_inl_eq_ker_rightHom, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
⊢ HMul.hMul (α := G) (β := G) (((S.rightHom : (a : E) → G) (Function.surjInv ⋯ ((S.rightHom : (a : E) → G) e)))⁻¹ : G)
      ((S.rightHom : (a : E) → G) e : G) =
    1

Tactic:
simpa only [Function.surjInv_eq] using inv_mul_cancel (S.rightHom e)

Premises used: inv_mul_cancel, GroupExtension.rightHom, Function.surjInv_eq, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
obtain :
  ∀ (n : N)
    (hn :
      (S.inl : (a : N) → E) n = (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e),
    HMul.hMul (β := E) (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))
        ((S.inl : (a : N) → E)
            (Function.invFun.{u_1 + 1, u_4 + 1} (β := E') ((⇑S'.inl : (a : N) → E') : (a : N) → E')
              ((f : (a : E) → E')
                  ((Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e) :
                E')) :
          E) =
      e
⊢ HMul.hMul (β := E) (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))
      ((S.inl : (a : N) → E)
          (Function.invFun.{u_1 + 1, u_4 + 1} (β := E') ((⇑S'.inl : (a : N) → E') : (a : N) → E')
            ((f : (a : E) → E')
                ((Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e) :
              E')) :
        E) =
    e

Tactic:
obtain ⟨n, hn⟩ :
        (Function.surjInv S.rightHom_surjective (S'.rightHom (f e)))⁻¹ * e ∈ S.inl.range := by
      rw [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, ← MonoidHom.comp_apply,
        rightHom_comp]
      simpa only [Function.surjInv_eq] using inv_mul_cancel (S.rightHom e)

Premises used: MonoidHom.range, GroupExtension.rightHom, GroupExtension.rightHom_surjective, Function.surjInv, GroupExtension.inl, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
n : N
hn : (S.inl : (a : N) → E) n = (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e
rw :
  (S.inl : (a : N) → E)
      (Function.invFun.{u_1 + 1, u_4 + 1} (β := E') ((⇑S'.inl : (a : N) → E') : (a : N) → E')
        ((f : (a : E) → E') ((Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e) :
          E')) =
    (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e
rw₁ :
  Eq.{u_3 + 1} (α := E)
    ((S.inl : (a : N) → E)
        (Function.invFun.{u_1 + 1, u_4 + 1} (β := E') ((⇑S'.inl : (a : N) → E') : (a : N) → E')
          ((f : (a : E) → E') ((S.inl : (a : N) → E) n : E) : E')) :
      E)
    ((S.inl : (a : N) → E) n : E)
rw₂ :
  Eq.{u_3 + 1} (α := E)
    ((S.inl : (a : N) → E)
        (Function.invFun.{u_1 + 1, u_4 + 1} (β := E') ((⇑S'.inl : (a : N) → E') : (a : N) → E')
          ((f.comp S.inl : (a : N) → E') n : E')) :
      E)
    ((S.inl : (a : N) → E) n : E)
rw₃ :
  Eq.{u_3 + 1} (α := E)
    ((S.inl : (a : N) → E)
        (Function.invFun.{u_1 + 1, u_4 + 1} (β := E') ((⇑S'.inl : (a : N) → E') : (a : N) → E')
          ((S'.inl : (a : N) → E') n : E')) :
      E)
    ((S.inl : (a : N) → E) n : E)
rw₄ rw₅ : Eq.{u_3 + 1} (α := E) ((S.inl : (a : N) → E) n : E) ((S.inl : (a : N) → E) n : E)
⊢ HMul.hMul (β := E) (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))
      ((S.inl : (a : N) → E)
          (Function.invFun.{u_1 + 1, u_4 + 1} (β := E') ((⇑S'.inl : (a : N) → E') : (a : N) → E')
            ((f : (a : E) → E')
                ((Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e) :
              E')) :
        E) =
    e

Tactic:
rw [← eq_inv_mul_iff_mul_eq, ← hn, ← MonoidHom.comp_apply, comp_inl,
      Function.leftInverse_invFun S'.inl_injective]

Premises used: eq_inv_mul_iff_mul_eq, Function.leftInverse_invFun, GroupExtension.inl_injective, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
simp :
  HMul.hMul (α := E') (β := E') ((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')) : E')
      ((f : (a : E) → E')
          ((S.inl : (a : N) → E)
              (Function.invFun (⇑S'.inl : (a : N) → E')
                (HMul.hMul (α := E')
                  (((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e')) :
            E) :
        E') =
    e'
⊢ (↑f : OneHom E E').toFun
      ((fun (e' : E') ↦
          let e := Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e');
          HMul.hMul (β := E) e
            ((S.inl : (a : N) → E)
                (Function.invFun (⇑S'.inl : (a : N) → E') (HMul.hMul (α := E') (((f : (a : E) → E') e)⁻¹ : E') e')) :
              E))
        e') =
    e'

Tactic:
simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, map_mul]

Premises used: MonoidHom.toOneHom_coe, map_mul, OneHom.toFun_eq_coe
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
rw :
  (S'.inl : (a : N) → E')
      (Function.invFun (⇑S'.inl : (a : N) → E')
        (HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e')) =
    HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e'
⊢ HMul.hMul (α := E') (β := E') ((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')) : E')
      ((f : (a : E) → E')
          ((S.inl : (a : N) → E)
              (Function.invFun (⇑S'.inl : (a : N) → E')
                (HMul.hMul (α := E')
                  (((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e')) :
            E) :
        E') =
    e'

Tactic:
rw [← eq_inv_mul_iff_mul_eq, ← MonoidHom.comp_apply, comp_inl]

Premises used: eq_inv_mul_iff_mul_eq, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
h :
  ∃ (a : N),
    (S'.inl : (a : N) → E') a =
      HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e'
⊢ (S'.inl : (a : N) → E')
      (Function.invFun (⇑S'.inl : (a : N) → E')
        (HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e')) =
    HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e'

Tactic:
apply Function.invFun_eq

Premises used: Function.invFun_eq
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
h :
  HMul.hMul (α := G) (β := G)
      (((S.rightHom : (a : E) → G) (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : G)
      ((S'.rightHom : (a : E') → G) e' : G) =
    1
⊢ ∃ (a : N),
    (S'.inl : (a : N) → E') a =
      HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e'

Tactic:
rw [← MonoidHom.mem_range, S'.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      ← MonoidHom.comp_apply, rightHom_comp]

Premises used: map_inv, MonoidHom.mem_ker, MonoidHom.mem_range, map_mul, GroupExtension.range_inl_eq_ker_rightHom, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
E' : Type u_4
inst_3 : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ HMul.hMul (α := G) (β := G)
      (((S.rightHom : (a : E) → G) (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) e')))⁻¹ : G)
      ((S'.rightHom : (a : E') → G) e' : G) =
    1

Tactic:
simpa only [Function.surjInv_eq] using inv_mul_cancel (S'.rightHom e')

Premises used: inv_mul_cancel, GroupExtension.rightHom, Function.surjInv_eq, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
s : S.Splitting
x : N ⋊[s.conjAct] G
n : N
g : G
⊢ Eq (α := N ⋊[s.conjAct] G)
    ((fun (e : E) ↦
        (⟨Function.invFun (⇑S.inl : (a : N) → E)
              (HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)),
            (S.rightHom : (a : E) → G) e⟩ :
          N ⋊[s.conjAct] G))
      ((fun (x : N ⋊[s.conjAct] G) ↦
          (match (motive := N ⋊[s.conjAct] G → E) x with
            | ⟨n, g⟩ => HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((s : (a : G) → E) g : E) :
            E))
        ⟨n, g⟩))
    ⟨n, g⟩

Tactic:
simp only [map_mul, rightHom_inl, rightHom_splitting, one_mul, mul_inv_cancel_right,
      Function.leftInverse_invFun S.inl_injective n]

Premises used: mul_inv_cancel_right, GroupExtension.rightHom_inl, map_mul, Function.leftInverse_invFun, GroupExtension.inl_injective, GroupExtension.Splitting.rightHom_splitting, one_mul