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 : S.Splitting
e : E
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)
⊢ (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

Tactic:
simp only [← eq_mul_inv_iff_mul_eq]

Premises used: 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 : S.Splitting
e : E
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)
⊢ (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:
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
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
h₆ h₇ : Eq.{u_2 + 1} (α := G) 1 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)

Tactic:
rw [← MonoidHom.mem_range, S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      rightHom_splitting, mul_inv_cancel]

Premises used: map_inv, MonoidHom.mem_ker, MonoidHom.mem_range, map_mul, mul_inv_cancel, GroupExtension.Splitting.rightHom_splitting, 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 : S.Splitting
x x_1 : N ⋊[s.conjAct] G
n₁ : N
g₁ : G
n₂ : N
g₂ : G
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)
⊢ (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)

Tactic:
simp only [conjAct, MonoidHom.comp_apply, map_mul, inl_conjAct_comm, MonoidHom.coe_coe]

Premises used: GroupExtension.Splitting.conjAct, MonoidHom.coe_coe, map_mul, GroupExtension.inl_conjAct_comm, 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
s : S.Splitting
x x_1 : N ⋊[s.conjAct] G
n₁ : N
g₁ : G
n₂ : N
g₂ : G
⊢ 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:
group
-- 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
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 := ⋯, right_inv := ⋯, map_mul' := ⋯ } :
            (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)
⊢ 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)

Tactic:
ext 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 : S.Splitting
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 := ⋯, right_inv := ⋯, map_mul' := ⋯ } :
          (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:
simp only [SemidirectProduct.toGroupExtension, Function.comp_apply, MulEquiv.coe_mk,
      Equiv.coe_fn_mk, SemidirectProduct.left_inl, SemidirectProduct.right_inl, map_one, mul_one]

Premises used: SemidirectProduct.left_inl, MulEquiv.coe_mk, map_one, SemidirectProduct.toGroupExtension, Equiv.coe_fn_mk, Function.comp_apply, mul_one, SemidirectProduct.right_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 : S.Splitting
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 := ⋯, right_inv := ⋯, map_mul' := ⋯ } :
            (a : N ⋊[s.conjAct] G) → E)
          ⟨n, g⟩ :
        G)
      (((SemidirectProduct.toGroupExtension s.conjAct).rightHom : (a : N ⋊[s.conjAct] G) → G) ⟨n, g⟩ : G)
⊢ 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)

Tactic:
ext ⟨n, g⟩
-- 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
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 := ⋯, right_inv := ⋯, map_mul' := ⋯ } :
          (a : N ⋊[s.conjAct] G) → E)
        ⟨n, g⟩ :
      G)
    (((SemidirectProduct.toGroupExtension s.conjAct).rightHom : (a : N ⋊[s.conjAct] G) → G) ⟨n, g⟩ : G)

Tactic:
simp only [SemidirectProduct.toGroupExtension, Function.comp_apply, MulEquiv.coe_mk,
      Equiv.coe_fn_mk, map_mul, rightHom_inl, one_mul, rightHom_splitting,
      SemidirectProduct.rightHom_eq_right]

Premises used: GroupExtension.rightHom_inl, MulEquiv.coe_mk, map_mul, SemidirectProduct.rightHom_eq_right, SemidirectProduct.toGroupExtension, Equiv.coe_fn_mk, Function.comp_apply, GroupExtension.Splitting.rightHom_splitting, one_mul
-- 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
⊢ Eq (α := (a : G) → E) (⇑s : (a : G) → E) fun (g : G) ↦
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) 1 : E) ((s : (a : G) → E) g : E))
      (((S.inl : (a : N) → E) 1)⁻¹ : E)

Tactic:
simp only [map_one, inv_one, one_mul, mul_one]

Premises used: inv_one, map_one, mul_one, one_mul
-- 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₂ : S.Splitting
h : S.IsConj s₁ s₂
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₁
⊢ S.IsConj s₂ s₁

Tactic:
obtain ⟨n, hn⟩ := h
-- 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₂ : 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)
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)
⊢ 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)

Tactic:
simp only [hn, map_inv]

Premises used: map_inv
-- 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₂ : 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) (((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:
group
-- 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₂ : 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)
⊢ S.IsConj s₂ s₁

Tactic:
exact ⟨n⁻¹, by simp only [hn, map_inv]; group⟩
-- 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₂ s₃ : S.Splitting
h₁ : S.IsConj s₁ s₂
h₂ : S.IsConj s₂ s₃
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₃
⊢ S.IsConj s₁ s₃

Tactic:
obtain ⟨n₁, hn₁⟩ := h₁
-- 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₂ 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)
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₃
⊢ S.IsConj s₁ s₃

Tactic:
obtain ⟨n₂, hn₂⟩ := h₂
-- 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₂ 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)
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))⁻¹
⊢ 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)

Tactic:
simp only [hn₁, hn₂, map_mul]

Premises used: map_mul
-- 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₂ 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)
    (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:
group
-- 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₂ 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)
⊢ S.IsConj s₁ s₃

Tactic:
exact ⟨n₁ * n₂, by simp only [hn₁, hn₂, map_mul]; group⟩
-- Module: Mathlib.GroupTheory.GroupExtension.Basic
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
rw₂ rw₃ : g = g
⊢ right.{u_1, u_2} (N := N) (φ := φ) ((s : (a : G) → N ⋊[φ] G) g) = g

Tactic:
rw [← rightHom_eq_right, ← toGroupExtension_rightHom, s.rightHom_splitting]

Premises used: SemidirectProduct.rightHom_eq_right, GroupExtension.Splitting.rightHom_splitting, SemidirectProduct.toGroupExtension_rightHom
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
⊢ S.inl.range.Normal

Tactic:
S.range_inl_eq_ker_rightHom ▸ S.rightHom.normal_ker

Premises used: Eq.rec, GroupExtension.rightHom, MonoidHom.normal_ker, Eq.symm, GroupExtension.range_inl_eq_ker_rightHom
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
n : N
rw : ∃ (x : N), Eq.{u_2 + 1} (α := E) ((S.inl : (a : N) → E) x : E) ((S.inl : (a : N) → E) n : E)
⊢ Eq.{u_3 + 1} (α := G) ((S.rightHom : (a : E) → G) ((S.inl : (a : N) → E) n : E) : G) (1 : G)

Tactic:
rw [← MonoidHom.mem_ker, ← S.range_inl_eq_ker_rightHom, MonoidHom.mem_range]

Premises used: MonoidHom.mem_ker, MonoidHom.mem_range, GroupExtension.range_inl_eq_ker_rightHom
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
n : N
⊢ ∃ (x : N), Eq.{u_2 + 1} (α := E) ((S.inl : (a : N) → E) x : E) ((S.inl : (a : N) → E) n : E)

Tactic:
exists_apply_eq_apply S.inl n

Premises used: GroupExtension.inl, DFunLike.coe, exists_apply_eq_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
n : N
⊢ ∃ (x : N), Eq.{u_2 + 1} (α := E) ((S.inl : (a : N) → E) x : E) ((S.inl : (a : N) → E) n : E)

Tactic:
exact exists_apply_eq_apply S.inl n

Premises used: GroupExtension.inl, DFunLike.coe, exists_apply_eq_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
h : ∀ (n : N), Eq.{u_3 + 1} (α := G) ((S.rightHom.comp S.inl : (a : N) → G) n : G) ((1 : (a : N) → G) n : G)
⊢ S.rightHom.comp S.inl = 1

Tactic:
ext n
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
n : N
h : Eq.{u_3 + 1} (α := G) ((S.rightHom : (a : E) → G) ((S.inl : (a : N) → E) n : E) : G) (1 : G)
⊢ Eq.{u_3 + 1} (α := G) ((S.rightHom.comp S.inl : (a : N) → G) n : G) ((1 : (a : N) → G) n : G)

Tactic:
rw [MonoidHom.one_apply, MonoidHom.comp_apply]

Premises used: MonoidHom.one_apply, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
n : N
⊢ Eq.{u_3 + 1} (α := G) ((S.rightHom : (a : E) → G) ((S.inl : (a : N) → E) n : E) : G) (1 : G)

Tactic:
S.rightHom_inl n

Premises used: GroupExtension.rightHom_inl
-- Module: Mathlib.GroupTheory.GroupExtension.Defs
Goal:
N : Type u_1
E : Type u_2
G : Type u_3
inst : Group N
inst_1 : Group E
inst_2 : Group G
S : GroupExtension N E G
n : N
⊢ Eq.{u_3 + 1} (α := G) ((S.rightHom : (a : E) → G) ((S.inl : (a : N) → E) n : E) : G) (1 : G)

Tactic:
exact S.rightHom_inl n

Premises used: GroupExtension.rightHom_inl