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
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'
⊢ ∃ (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'
have h : 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 [← MonoidHom.mem_range, 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
s : S.Splitting
e : E
⊢ (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))
      ((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))
        e) =
    e
have simp : (S.inl : (a : N) → E)
    (Function.invFun (⇑S.inl : (a : N) → E)
      (HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E))) =
  HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
Tactic: simp only [← eq_mul_inv_iff_mul_eq]
-- 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 : S.Splitting
e : E
⊢ (S.inl : (a : N) → E)
      (Function.invFun (⇑S.inl : (a : N) → E)
        (HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E))) =
    HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
have h : ∃ (a : N), (S.inl : (a : N) → E) a = HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
Tactic: apply Function.invFun_eq
-- 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 : S.Splitting
e : E
⊢ ∃ (a : N),
    (S.inl : (a : N) → E) a = HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
have h : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.inl.range
Tactic: rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]
-- 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 : S.Splitting
e : E
h : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.inl.range
⊢ ∃ (a : N),
    (S.inl : (a : N) → E) a = HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
have h₁ : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.rightHom.ker
Tactic: rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]
-- 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 : S.Splitting
e : E
h : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.inl.range
h₁ : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.rightHom.ker
⊢ ∃ (a : N),
    (S.inl : (a : N) → E) a = HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
have h₂ : Eq.{u_2 + 1} (α := G)
  ((S.rightHom : (a : E) → G) (HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)) : G)
  (1 : G)
Tactic: rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]
-- 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 : S.Splitting
e : E
h : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.inl.range
h₁ : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.rightHom.ker
h₂ :
  Eq.{u_2 + 1} (α := G)
    ((S.rightHom : (a : E) → G) (HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)) :
      G)
    (1 : G)
⊢ ∃ (a : N),
    (S.inl : (a : N) → E) a = HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
have h₃ : HMul.hMul (α := G) (β := G) ((S.rightHom : (a : E) → G) e : G)
    ((S.rightHom : (a : E) → G) (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) : G) =
  1
Tactic: rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]
-- 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 : S.Splitting
e : E
h : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.inl.range
h₁ : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.rightHom.ker
h₂ :
  Eq.{u_2 + 1} (α := G)
    ((S.rightHom : (a : E) → G) (HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)) :
      G)
    (1 : G)
h₃ :
  HMul.hMul (α := G) (β := G) ((S.rightHom : (a : E) → G) e : G)
      ((S.rightHom : (a : E) → G) (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) : G) =
    1
⊢ ∃ (a : N),
    (S.inl : (a : N) → E) a = HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
have h₄ : HMul.hMul (α := G) (β := G) ((S.rightHom : (a : E) → G) e : G)
    (((S.rightHom : (a : E) → G) ((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G) : E))⁻¹ : G) =
  1
Tactic: rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]
-- 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 : S.Splitting
e : E
h : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.inl.range
h₁ : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.rightHom.ker
h₂ :
  Eq.{u_2 + 1} (α := G)
    ((S.rightHom : (a : E) → G) (HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)) :
      G)
    (1 : G)
h₃ :
  HMul.hMul (α := G) (β := G) ((S.rightHom : (a : E) → G) e : G)
      ((S.rightHom : (a : E) → G) (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) : G) =
    1
h₄ :
  HMul.hMul (α := G) (β := G) ((S.rightHom : (a : E) → G) e : G)
      (((S.rightHom : (a : E) → G) ((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G) : E))⁻¹ : G) =
    1
⊢ ∃ (a : N),
    (S.inl : (a : N) → E) a = HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
have h₅ : HMul.hMul (α := G) (β := G) ((S.rightHom : (a : E) → G) e : G) (((S.rightHom : (a : E) → G) e)⁻¹ : G) = 1
Tactic: rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]
-- 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 : S.Splitting
e : E
h : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.inl.range
h₁ : HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) ∈ S.rightHom.ker
h₂ :
  Eq.{u_2 + 1} (α := G)
    ((S.rightHom : (a : E) → G) (HMul.hMul (β := E) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)) :
      G)
    (1 : G)
h₃ :
  HMul.hMul (α := G) (β := G) ((S.rightHom : (a : E) → G) e : G)
      ((S.rightHom : (a : E) → G) (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E) : G) =
    1
h₄ :
  HMul.hMul (α := G) (β := G) ((S.rightHom : (a : E) → G) e : G)
      (((S.rightHom : (a : E) → G) ((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G) : E))⁻¹ : G) =
    1
h₅ : HMul.hMul (α := G) (β := G) ((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) e (((s : (a : G) → E) ((S.rightHom : (a : E) → G) e : G))⁻¹ : E)
have h₆ : Eq.{u_2 + 1} (α := G) 1 1
Tactic: rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]
-- 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 : S.Splitting
x x_1 : N ⋊[s.conjAct] G
n₁ : N
g₁ : G
n₂ : N
g₂ : G
⊢ (match (motive := N ⋊[s.conjAct] G → E) HMul.hMul (α := N ⋊[s.conjAct] G) ⟨n₁, g₁⟩ ⟨n₂, g₂⟩ with
    | ⟨n, g⟩ => HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((s : (a : G) → E) g : E)) =
    HMul.hMul (α := E) (β := E)
      (match (motive := N ⋊[s.conjAct] G → E) (⟨n₁, g₁⟩ : N ⋊[s.conjAct] G) with
        | ⟨n, g⟩ => HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((s : (a : G) → E) g : E) :
        E)
      (match (motive := N ⋊[s.conjAct] G → E) (⟨n₂, g₂⟩ : N ⋊[s.conjAct] G) with
        | ⟨n, g⟩ => HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((s : (a : G) → E) g : E) :
        E)
have simp : HMul.hMul (α := E) ((S.inl : (a : N) → E) n₁ : E)
      (HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((s : (a : G) → E) g₁ : E) ((S.inl : (a : N) → E) n₂ : E))
        (((s : (a : G) → E) g₁)⁻¹ : E)) *
    HMul.hMul (α := E) (β := E) ((s : (a : G) → E) g₁ : E) ((s : (a : G) → E) g₂ : E) =
  HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₁ : E) ((s : (a : G) → E) g₁ : E) *
    HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₂ : E) ((s : (a : G) → E) g₂ : E)
Tactic: simp only [conjAct, MonoidHom.comp_apply, map_mul, inl_conjAct_comm, MonoidHom.coe_coe]
-- 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 : S.Splitting
⊢ Eq (α := N → E)
    (Function.comp (β := N ⋊[s.conjAct] G)
      (⇑{
            toFun := 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),
            invFun := 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⟩,
            left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } :
        (a : N ⋊[s.conjAct] G) → E)
      (⇑(SemidirectProduct.toGroupExtension s.conjAct).inl : (a : N) → N ⋊[s.conjAct] G))
    (⇑S.inl : (a : N) → E)
have h : ∀ (n : N),
  Eq.{u_3 + 1} (α := E)
    (Function.comp (β := N ⋊[s.conjAct] G)
        (⇑{
              toFun := 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),
              invFun := 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⟩,
              left_inv := sorry, right_inv := sorry, map_mul' := sorry } :
          (a : N ⋊[s.conjAct] G) → E)
        (⇑(SemidirectProduct.toGroupExtension s.conjAct).inl : (a : N) → N ⋊[s.conjAct] G) n :
      E)
    ((S.inl : (a : N) → E) n : E)
Tactic: ext 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 : S.Splitting
⊢ Eq (α := N ⋊[s.conjAct] G → G)
    (Function.comp (β := E) (⇑S.rightHom : (a : E) → G)
      (⇑{
            toFun := 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),
            invFun := 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⟩,
            left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } :
        (a : N ⋊[s.conjAct] G) → E))
    (⇑(SemidirectProduct.toGroupExtension s.conjAct).rightHom : (a : N ⋊[s.conjAct] G) → G)
have h : ∀ (n : N) (g : G),
  Eq.{u_2 + 1} (α := G)
    (Function.comp (α := N ⋊[s.conjAct] G) (β := E) (⇑S.rightHom : (a : E) → G)
        (⇑{
              toFun := 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),
              invFun := 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⟩,
              left_inv := sorry, right_inv := sorry, map_mul' := sorry } :
          (a : N ⋊[s.conjAct] G) → E)
        ⟨n, g⟩ :
      G)
    (((SemidirectProduct.toGroupExtension s.conjAct).rightHom : (a : N ⋊[s.conjAct] G) → G) ⟨n, g⟩ : G)
Tactic: ext ⟨n, 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₁ s₂ : S.Splitting
h : S.IsConj s₁ s₂
⊢ S.IsConj s₂ s₁
have obtain : ∀ (n : N)
  (hn :
    Eq (α := (a : G) → E) (⇑s₁ : (a : G) → E) fun (g : G) ↦
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((s₂ : (a : G) → E) g : E))
        (((S.inl : (a : N) → E) n)⁻¹ : E)),
  S.IsConj s₂ s₁
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- 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₁ s₂ : S.Splitting
n : N
hn :
  Eq (α := (a : G) → E) (⇑s₁ : (a : G) → E) fun (g : G) ↦
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((s₂ : (a : G) → E) g : E))
      (((S.inl : (a : N) → E) n)⁻¹ : E)
⊢ Eq (α := (a : G) → E) (⇑s₂ : (a : G) → E) fun (g : G) ↦
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n⁻¹ : E) ((s₁ : (a : G) → E) g : E))
      (((S.inl : (a : N) → E) n⁻¹)⁻¹ : E)
have simp : Eq (α := (a : G) → E) (⇑s₂ : (a : G) → E) fun (g : G) ↦
  HMul.hMul (β := E)
    (HMul.hMul (α := E) (((S.inl : (a : N) → E) n)⁻¹ : E)
      (HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((s₂ : (a : G) → E) g : E))
        (((S.inl : (a : N) → E) n)⁻¹ : E)))
    (((S.inl : (a : N) → E) n)⁻¹⁻¹ : E)
Tactic: simp only [hn, map_inv]
-- 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₁ s₂ s₃ : S.Splitting
h₁ : S.IsConj s₁ s₂
h₂ : S.IsConj s₂ s₃
⊢ S.IsConj s₁ s₃
have obtain : ∀ (n₁ : N)
  (hn₁ :
    Eq (α := (a : G) → E) (⇑s₁ : (a : G) → E) fun (g : G) ↦
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₁ : E) ((s₂ : (a : G) → E) g : E))
        (((S.inl : (a : N) → E) n₁)⁻¹ : E)),
  S.IsConj s₁ s₃
Tactic: obtain ⟨n₁, hn₁⟩ := h₁
Cleared hypotheses: h₁
-- 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₁ s₂ s₃ : S.Splitting
h₂ : S.IsConj s₂ s₃
n₁ : N
hn₁ :
  Eq (α := (a : G) → E) (⇑s₁ : (a : G) → E) fun (g : G) ↦
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₁ : E) ((s₂ : (a : G) → E) g : E))
      (((S.inl : (a : N) → E) n₁)⁻¹ : E)
⊢ S.IsConj s₁ s₃
have obtain : ∀ (n₂ : N)
  (hn₂ :
    Eq (α := (a : G) → E) (⇑s₂ : (a : G) → E) fun (g : G) ↦
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₂ : E) ((s₃ : (a : G) → E) g : E))
        (((S.inl : (a : N) → E) n₂)⁻¹ : E)),
  S.IsConj s₁ s₃
Tactic: obtain ⟨n₂, hn₂⟩ := h₂
Cleared hypotheses: h₂
-- 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₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ :
  Eq (α := (a : G) → E) (⇑s₁ : (a : G) → E) fun (g : G) ↦
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₁ : E) ((s₂ : (a : G) → E) g : E))
      (((S.inl : (a : N) → E) n₁)⁻¹ : E)
n₂ : N
hn₂ :
  Eq (α := (a : G) → E) (⇑s₂ : (a : G) → E) fun (g : G) ↦
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₂ : E) ((s₃ : (a : G) → E) g : E))
      (((S.inl : (a : N) → E) n₂)⁻¹ : E)
⊢ Eq (α := (a : G) → E) (⇑s₁ : (a : G) → E) fun (g : G) ↦
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) (n₁ * n₂) : E) ((s₃ : (a : G) → E) g : E))
      (((S.inl : (a : N) → E) (n₁ * n₂))⁻¹ : E)
have simp : Eq (α := (a : G) → E)
  (fun (g : G) ↦
    HMul.hMul (β := E)
      (HMul.hMul (α := E) ((S.inl : (a : N) → E) n₁ : E)
        (HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₂ : E) ((s₃ : (a : G) → E) g : E))
          (((S.inl : (a : N) → E) n₂)⁻¹ : E)))
      (((S.inl : (a : N) → E) n₁)⁻¹ : E))
  fun (g : G) ↦
  HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₁ : E) ((S.inl : (a : N) → E) n₂ : E))
      ((s₃ : (a : G) → E) g : E) *
    (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n₁ : E) ((S.inl : (a : N) → E) n₂ : E))⁻¹
Tactic: simp only [hn₁, hn₂, 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
φ : MonoidHom.{u_2, u_1} G (MulAut N)
s : (toGroupExtension φ).Splitting
g : G
⊢ right.{u_1, u_2} (N := N) (φ := φ) ((s : (a : G) → N ⋊[φ] G) g) = g
have rw : (rightHom : (a : N ⋊[φ] G) → G) ((s : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G) = g
Tactic: rw [← rightHom_eq_right, ← toGroupExtension_rightHom, s.rightHom_splitting]
-- 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
φ : MonoidHom.{u_2, u_1} G (MulAut N)
s : (toGroupExtension φ).Splitting
g : G
rw : (rightHom : (a : N ⋊[φ] G) → G) ((s : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G) = g
⊢ right.{u_1, u_2} (N := N) (φ := φ) ((s : (a : G) → N ⋊[φ] G) g) = g
have rw₁ : ((toGroupExtension φ).rightHom : (a : N ⋊[φ] G) → G) ((s : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G) = g
Tactic: rw [← rightHom_eq_right, ← toGroupExtension_rightHom, s.rightHom_splitting]
-- 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
φ : MonoidHom.{u_2, u_1} G (MulAut N)
s : (toGroupExtension φ).Splitting
g : G
rw : (rightHom : (a : N ⋊[φ] G) → G) ((s : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G) = g
rw₁ : ((toGroupExtension φ).rightHom : (a : N ⋊[φ] G) → G) ((s : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G) = g
⊢ right.{u_1, u_2} (N := N) (φ := φ) ((s : (a : G) → N ⋊[φ] G) g) = g
have rw₂ : g = g
Tactic: rw [← rightHom_eq_right, ← toGroupExtension_rightHom, s.rightHom_splitting]
-- 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
n : N
⊢ Eq.{u_3 + 1} (α := G) ((S.rightHom : (a : E) → G) ((S.inl : (a : N) → E) n : E) : G) (1 : G)
have rw : ∃ (x : N), Eq.{u_2 + 1} (α := E) ((S.inl : (a : N) → E) x : E) ((S.inl : (a : N) → E) n : E)
Tactic: rw [← MonoidHom.mem_ker, ← S.range_inl_eq_ker_rightHom, MonoidHom.mem_range]
-- 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.rightHom.comp S.inl = 1
have h : ∀ (n : N), Eq.{u_3 + 1} (α := G) ((S.rightHom.comp S.inl : (a : N) → G) n : G) ((1 : (a : N) → G) n : G)
Tactic: ext n
-- 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
n : N
⊢ Eq.{u_3 + 1} (α := G) ((S.rightHom.comp S.inl : (a : N) → G) n : G) ((1 : (a : N) → G) n : G)
have h : Eq.{u_3 + 1} (α := G) ((S.rightHom : (a : E) → G) ((S.inl : (a : N) → E) n : E) : G) (1 : G)
Tactic: rw [MonoidHom.one_apply, MonoidHom.comp_apply]
-- 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
⊢ (MonoidHom.ofInjective ⋯).trans
      (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) 1) (MonoidHom.ofInjective ⋯).symm) =
    1
have h : ∀ (x : N),
  Eq (α := N)
    (((MonoidHom.ofInjective sorry).trans
            (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) 1) (MonoidHom.ofInjective sorry).symm) :
          (a : N) → N)
        x :
      N)
    ((1 : (a : N) → N) x : N)
Tactic: ext _
-- 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
x x_1 : E
⊢ (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)
have h : ∀ (x_2 : N),
  Eq (α := N)
    (((MonoidHom.ofInjective sorry).trans
            (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) (x * x_1))
              (MonoidHom.ofInjective sorry).symm) :
          (a : N) → N)
        x_2 :
      N)
    (((MonoidHom.ofInjective sorry).trans
              (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) x) (MonoidHom.ofInjective sorry).symm) *
            (MonoidHom.ofInjective sorry).trans
              (MulEquiv.trans ((MulAut.conjNormal : (a : E) → MulAut ↥S.inl.range) x_1)
                (MonoidHom.ofInjective sorry).symm) :
          (a : N) → N)
        x_2 :
      N)
Tactic: ext _