awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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),
    (σ : (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)
have 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)
Tactic: obtain ⟨n, hn⟩ := mul_inv_mul_mul_mem_range_inl σ g₁ g₂
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use n⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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)
⊢ (σ : (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)
have 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)
Tactic: rw [map_inv, eq_mul_inv_iff_mul_eq, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, hn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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)
⊢ (σ : (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)
have 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)
Tactic: rw [map_inv, eq_mul_inv_iff_mul_eq, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, hn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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)
⊢ (σ : (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)
have 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))
Tactic: rw [map_inv, eq_mul_inv_iff_mul_eq, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, hn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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)
⊢ (σ : (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)
have 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)
Tactic: rw [map_inv, eq_mul_inv_iff_mul_eq, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, hn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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
⊢ (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
have rw : (S'.rightHom : (a : E') → G) ((equiv : (a : E) → E') ((σ : (a : G) → E) g : E) : E') = g
Tactic: rw [Function.comp_apply, equiv.rightHom_map, rightHom_section]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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
⊢ (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
have rw₁ : (S.rightHom : (a : E) → G) ((σ : (a : G) → E) g : E) = g
Tactic: rw [Function.comp_apply, equiv.rightHom_map, rightHom_section]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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
⊢ (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
have rw₂ : g = g
Tactic: rw [Function.comp_apply, equiv.rightHom_map, rightHom_section]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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
⊢ (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
have simp : HMul.hMul (β := E) (Function.surjInv sorry ((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 sorry ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e) :
            E')) :
      E) =
  e
Tactic: simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, ← map_inv, ← map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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
⊢ (Function.surjInv ⋯ ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e ∈ S.inl.range
have rw : HMul.hMul (α := G) (β := G) (((S.rightHom : (a : E) → G) (Function.surjInv sorry ((S.rightHom : (a : E) → G) e)))⁻¹ : G)
    ((S.rightHom : (a : E) → G) e : G) =
  1
Tactic: rw [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, ← MonoidHom.comp_apply,
        rightHom_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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 (β := 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
have obtain : ∀ (n : N)
  (hn :
    (S.inl : (a : N) → E) n = (Function.surjInv sorry ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e),
  HMul.hMul (β := E) (Function.surjInv sorry ((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 sorry ((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)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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
⊢ 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
have 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 sorry ((S'.rightHom : (a : E') → G) ((f : (a : E) → E') e : E')))⁻¹ * e) :
        E')) =
  (Function.surjInv sorry ((S'.rightHom : (a : E') → G) ((f : (a : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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
⊢ 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
have 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)
Tactic: rw [← eq_inv_mul_iff_mul_eq, ← hn, ← MonoidHom.comp_apply, comp_inl,
      Function.leftInverse_invFun S'.inl_injective]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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)
⊢ 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
have 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)
Tactic: rw [← eq_inv_mul_iff_mul_eq, ← hn, ← MonoidHom.comp_apply, comp_inl,
      Function.leftInverse_invFun S'.inl_injective]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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)
⊢ 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
have 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)
Tactic: rw [← eq_inv_mul_iff_mul_eq, ← hn, ← MonoidHom.comp_apply, comp_inl,
      Function.leftInverse_invFun S'.inl_injective]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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)
⊢ 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
have rw₄ : Eq.{u_3 + 1} (α := E) ((S.inl : (a : N) → E) n : E) ((S.inl : (a : N) → E) n : E)
Tactic: rw [← eq_inv_mul_iff_mul_eq, ← hn, ← MonoidHom.comp_apply, comp_inl,
      Function.leftInverse_invFun S'.inl_injective]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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'
⊢ (↑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'
have simp : HMul.hMul (α := E') (β := E') ((f : (a : E) → E') (Function.surjInv sorry ((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 sorry ((S'.rightHom : (a : E') → G) e')))⁻¹ : E')
                e')) :
          E) :
      E') =
  e'
Tactic: simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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 (α := 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'
have rw : (S'.inl : (a : N) → E')
    (Function.invFun (⇑S'.inl : (a : N) → E')
      (HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv sorry ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e')) =
  HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv sorry ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e'
Tactic: rw [← eq_inv_mul_iff_mul_eq, ← MonoidHom.comp_apply, comp_inl]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
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'
⊢ (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'
have h : ∃ (a : N),
  (S'.inl : (a : N) → E') a =
    HMul.hMul (α := E') (((f : (a : E) → E') (Function.surjInv sorry ((S'.rightHom : (a : E') → G) e')))⁻¹ : E') e'
Tactic: apply Function.invFun_eq