awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ Normal (normalClosure s)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
⊢ normalClosure (↑H : Set G) = H

Tactic:
le_antisymm (normalClosure_le_normal rfl.subset) le_normalClosure

Premises used: Subgroup.le_normalClosure, Eq.subset, le_antisymm, Subgroup.normalClosure_le_normal, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ Eq (α := Subgroup G) (normalClosure (↑(normalClosure s) : Set G)) (normalClosure s)

Tactic:
normalClosure_eq_self _

Premises used: Subgroup.normalClosure_eq_self
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ LE.le (α := Subgroup G) (closure s) (normalClosure s)

Tactic:
simp only [subset_normalClosure, closure_le]

Premises used: Subgroup.closure_le, Subgroup.subset_normalClosure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ Eq (α := Subgroup G) (normalClosure (↑(closure s) : Set G)) (normalClosure s)

Tactic:
le_antisymm (normalClosure_le_normal closure_le_normalClosure) (normalClosure_mono subset_closure)

Premises used: Subgroup.normalClosure_mono, Subgroup.subset_closure, le_antisymm, Subgroup.normalClosure_le_normal, Subgroup.closure_le_normalClosure
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
rw : Eq (α := Subgroup G) (normalClosure (↑(closure ∅) : Set G)) ⊥
rw₁ : Eq (α := Subgroup G) (normalClosure (↑⊥ : Set G)) ⊥
rw₂ rw₃ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup G) (normalClosure ∅) ⊥

Tactic:
rw [← normalClosure_closure_eq_normalClosure, closure_empty, normalClosure_eq_self]

Premises used: Subgroup.closure_empty, Subgroup.normalClosure_closure_eq_normalClosure, Subgroup.normalClosure_eq_self
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
H : Subgroup G
a : G
rw : 1 ∈ H
⊢ a * 1 * a⁻¹ ∈ H

Tactic:
rw [mul_one, mul_inv_cancel]

Premises used: mul_inv_cancel, mul_one
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H

Tactic:
H.one_mem

Premises used: Set.Mem, Subgroup.one_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
H : Subgroup G
a : G
⊢ 1 ∈ H

Tactic:
exact H.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
rw : 1 * a * 1⁻¹ ∈ H
⊢ a ∈ H

Tactic:
rw [← mul_one a, ← inv_one, ← one_mul a]

Premises used: inv_one, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H

Tactic:
h 1

Premises used: Set.Mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H

Tactic:
exact h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
rw : c * b * a * (c * b)⁻¹ ∈ H
⊢ c * (b * a * b⁻¹) * c⁻¹ ∈ H

Tactic:
rw [mul_assoc, mul_assoc, ← mul_inv_rev, ← mul_assoc, ← mul_assoc]

Premises used: mul_assoc, mul_inv_rev
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * b * a * (c * b)⁻¹ ∈ H

Tactic:
h (c * b)

Premises used: HMul.hMul, Set.Mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * b * a * (c * b)⁻¹ ∈ H

Tactic:
exact h (c * b)

Premises used: HMul.hMul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hN : N.Normal
⊢ N ≤ H.normalCore ↔ N ≤ H

Tactic:
⟨ge_trans H.normalCore_le, fun h_le n hn g => h_le (hN.conj_mem n hn g)⟩

Premises used: ge_trans, Iff.intro, Subgroup.normalCore_le, Subgroup.Normal.conj_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ H.normalCore ≤ K.normalCore

Tactic:
normal_le_normalCore.mpr (H.normalCore_le.trans h)

Premises used: Iff.mpr, Subgroup.normal_le_normalCore, LE.le.trans, Subgroup.normalCore_le
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.normalCore = ⨆ (N : Subgroup G), ⨆ (_ : N.Normal), ⨆ (_ : N ≤ H), N

Tactic:
le_antisymm
    (le_iSup_of_le H.normalCore
      (le_iSup_of_le H.normalCore_normal (le_iSup_of_le H.normalCore_le le_rfl)))
    (iSup_le fun _ => iSup_le fun _ => iSup_le normal_le_normalCore.mpr)

Premises used: Iff.mpr, le_rfl, Subgroup.normal_le_normalCore, le_antisymm, le_iSup_of_le, iSup_le, Subgroup.normalCore, Subgroup.normalCore_normal, Subgroup.normalCore_le
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
⊢ H.normalCore = H

Tactic:
le_antisymm H.normalCore_le (normal_le_normalCore.mpr le_rfl)

Premises used: Iff.mpr, le_rfl, Subgroup.normal_le_normalCore, le_antisymm, Subgroup.normalCore_le
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.normalCore.normalCore = H.normalCore

Tactic:
H.normalCore.normalCore_eq_self

Premises used: Subgroup.normalCore_eq_self, Subgroup.normalCore
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
G' : Type u_8
N' : Type u_9
inst_2 : Group G'
inst_3 : Group N'
f : G →* N
g : G' →* N'
S : Subgroup N
S' : Subgroup N'
⊢ comap (f.prodMap g) (S.prod S') = (comap f S).prod (comap g S')

Tactic:
SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _

Premises used: SetLike.coe_injective, Set.preimage_prod_map_prod, DFunLike.coe
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
G' : Type u_8
N' : Type u_9
inst_2 : Group G'
inst_3 : Group N'
f : G →* N
g : G' →* N'
rw : comap (N := N × N') (f.prodMap g) ⊥ = f.ker.prod g.ker
rw₁ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod g.ker
rw₂ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod (comap g ⊥)
rw₃ : Eq (α := Subgroup (G × G')) (comap (N := N × N') (f.prodMap g) ⊥) (comap (N := N × N') (f.prodMap g) (prod ⊥ ⊥))
rw₄ rw₅ : Eq (α := Subgroup (G × G')) (comap (N := N × N') (f.prodMap g) ⊥) (comap (N := N × N') (f.prodMap g) ⊥)
⊢ (f.prodMap g).ker = f.ker.prod g.ker

Tactic:
rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]

Premises used: MonoidHom.comap_bot, MonoidHom.prodMap_comap_prod, Subgroup.bot_prod_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
⊢ Eq (α := Subgroup (G × G')) (ker (fst G G')) (prod ⊥ ⊤)

Tactic:
SetLike.ext fun _ => (iff_of_eq (and_true _)).symm

Premises used: and_true, Membership.mem, MonoidHom.ker, SetLike.ext, MonoidHom.fst, Iff.symm, iff_of_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
⊢ Eq (α := Subgroup (G × G')) (ker (snd G G')) (prod ⊤ ⊥)

Tactic:
SetLike.ext fun _ => (iff_of_eq (true_and _)).symm

Premises used: Membership.mem, MonoidHom.ker, SetLike.ext, Iff.symm, true_and, MonoidHom.snd, iff_of_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
rw : Subgroup.map f (normalizer (↑H : Set G)) ≤ normalizer (↑(Subgroup.map f H) : Set N)
⊢ (Subgroup.map f H).Normal

Tactic:
rw [← normalizer_eq_top_iff, ← top_le_iff, ← f.range_eq_top_of_surjective hf, f.range_eq_map,
    ← H.normalizer_eq_top]

Premises used: MonoidHom.range_eq_map, Subgroup.normalizer_eq_top, MonoidHom.range_eq_top_of_surjective, Subgroup.normalizer_eq_top_iff, top_le_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ Subgroup.map f (normalizer (↑H : Set G)) ≤ normalizer (↑(Subgroup.map f H) : Set N)

Tactic:
le_normalizer_map _

Premises used: Subgroup.le_normalizer_map
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ Subgroup.map f (normalizer (↑H : Set G)) ≤ normalizer (↑(Subgroup.map f H) : Set N)

Tactic:
exact le_normalizer_map _

Premises used: Subgroup.le_normalizer_map
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : N →* G
hf : Surjective.{u_5 + 1, u_1 + 1} (α := N) (β := G) (⇑f : (a : N) → G)
⊢ comap f (normalizer (↑H : Set G)) = normalizer (↑(comap f H) : Set N)

Tactic:
comap_normalizer_eq_of_le_range fun x _ ↦ hf x

Premises used: Subgroup.comap_normalizer_eq_of_le_range
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G ≃* N
h :
  ∀ (x : N),
    x ∈ map f.toMonoidHom (normalizer (↑H : Set G)) ↔
      Membership.mem (γ := Subgroup N) (normalizer (↑(map f.toMonoidHom H) : Set N)) x
⊢ map f.toMonoidHom (normalizer (↑H : Set G)) = normalizer (↑(map f.toMonoidHom H) : Set N)

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G ≃* N
x : N
h :
  (∀ (h : G),
      h ∈ H ↔
        HMul.hMul (β := G) (HMul.hMul (α := G) ((f.symm : (a : N) → G) x : G) h) (((f.symm : (a : N) → G) x)⁻¹ : G) ∈
          H) ↔
    ∀ (h : N),
      Membership.mem (α := G) H ((f.symm : (a : N) → G) h : G) ↔
        Membership.mem (α := G) H ((f.symm : (a : N) → G) (x * h * x⁻¹) : G)
⊢ x ∈ map f.toMonoidHom (normalizer (↑H : Set G)) ↔
    Membership.mem (γ := Subgroup N) (normalizer (↑(map f.toMonoidHom H) : Set N)) x

Tactic:
simp only [mem_normalizer_iff, mem_map_equiv]

Premises used: Subgroup.mem_map_equiv, Subgroup.mem_normalizer_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G ≃* N
x : N
h :
  ∀ (a : G),
    (a ∈ H ↔
        HMul.hMul (β := G) (HMul.hMul (α := G) ((f.symm : (a : N) → G) x : G) a) (((f.symm : (a : N) → G) x)⁻¹ : G) ∈
          H) ↔
      (Membership.mem (α := G) H ((f.symm : (a : N) → G) ((f.toEquiv : (a : G) → N) a : N) : G) ↔
        Membership.mem (α := G) H
          ((f.symm : (a : N) → G) (HMul.hMul (β := N) x ((f.toEquiv : (a : G) → N) a : N) * x⁻¹) : G))
⊢ (∀ (h : G),
      h ∈ H ↔
        HMul.hMul (β := G) (HMul.hMul (α := G) ((f.symm : (a : N) → G) x : G) h) (((f.symm : (a : N) → G) x)⁻¹ : G) ∈
          H) ↔
    ∀ (h : N),
      Membership.mem (α := G) H ((f.symm : (a : N) → G) h : G) ↔
        Membership.mem (α := G) H ((f.symm : (a : N) → G) (x * h * x⁻¹) : G)

Tactic:
rw [f.toEquiv.forall_congr]

Premises used: MulEquiv.toEquiv, Equiv.forall_congr
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G ≃* N
x : N
a : G
⊢ (a ∈ H ↔
      HMul.hMul (β := G) (HMul.hMul (α := G) ((f.symm : (a : N) → G) x : G) a) (((f.symm : (a : N) → G) x)⁻¹ : G) ∈ H) ↔
    (Membership.mem (α := G) H ((f.symm : (a : N) → G) ((f.toEquiv : (a : G) → N) a : N) : G) ↔
      Membership.mem (α := G) H
        ((f.symm : (a : N) → G) (HMul.hMul (β := N) x ((f.toEquiv : (a : G) → N) a : N) * x⁻¹) : G))

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G →* N
hf : Bijective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ map f (normalizer (↑H : Set G)) = normalizer (↑(map f H) : Set N)

Tactic:
map_equiv_normalizer_eq H (MulEquiv.ofBijective f hf)

Premises used: MulEquiv.toMonoidHom, MulEquiv.ofBijective, Subgroup.map_equiv_normalizer_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
rw : f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ g.ker
⊢ (g : (a : G₁) → G₃) (f_inv (x * y)) =
    HMul.hMul (α := G₃) (β := G₃) ((g : (a : G₁) → G₃) (f_inv x) : G₃) ((g : (a : G₁) → G₃) (f_inv y) : G₃)

Tactic:
rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]

Premises used: mul_inv_eq_one, MonoidHom.mem_ker, MonoidHom.map_inv, MonoidHom.map_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
a : f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ f.ker
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ g.ker

Tactic:
apply hg
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
a :
  (f : (a : G₁) → G₂) (f_inv (x * y)) =
    HMul.hMul (α := G₂) (β := G₂) ((f : (a : G₁) → G₂) (f_inv x) : G₂) ((f : (a : G₁) → G₂) (f_inv y) : G₂)
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ f.ker

Tactic:
rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul]

Premises used: mul_inv_eq_one, MonoidHom.mem_ker, MonoidHom.map_inv, MonoidHom.map_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ (f : (a : G₁) → G₂) (f_inv (x * y)) =
    HMul.hMul (α := G₂) (β := G₂) ((f : (a : G₁) → G₂) (f_inv x) : G₂) ((f : (a : G₁) → G₂) (f_inv y) : G₂)

Tactic:
simp only [hf _]
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
dsimp : Eq.{u_7 + 1} (α := G₃) ((g : (a : G₁) → G₃) (f_inv ((f : (a : G₁) → G₂) x)) : G₃) ((g : (a : G₁) → G₃) x : G₃)
⊢ Eq.{u_7 + 1} (α := G₃) ((f.liftOfRightInverseAux f_inv hf g hg : (a : G₂) → G₃) ((f : (a : G₁) → G₂) x : G₂) : G₃)
    ((g : (a : G₁) → G₃) x : G₃)

Tactic:
dsimp [liftOfRightInverseAux]

Premises used: MonoidHom.liftOfRightInverseAux
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
rw : f_inv ((f : (a : G₁) → G₂) x) * x⁻¹ ∈ g.ker
⊢ Eq.{u_7 + 1} (α := G₃) ((g : (a : G₁) → G₃) (f_inv ((f : (a : G₁) → G₂) x)) : G₃) ((g : (a : G₁) → G₃) x : G₃)

Tactic:
rw [← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]

Premises used: mul_inv_eq_one, MonoidHom.mem_ker, MonoidHom.map_inv, MonoidHom.map_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
a : f_inv ((f : (a : G₁) → G₂) x) * x⁻¹ ∈ f.ker
⊢ f_inv ((f : (a : G₁) → G₂) x) * x⁻¹ ∈ g.ker

Tactic:
apply hg
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
a : Eq.{u_6 + 1} (α := G₂) ((f : (a : G₁) → G₂) (f_inv ((f : (a : G₁) → G₂) x)) : G₂) ((f : (a : G₁) → G₂) x : G₂)
⊢ f_inv ((f : (a : G₁) → G₂) x) * x⁻¹ ∈ f.ker

Tactic:
rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one]

Premises used: mul_inv_eq_one, MonoidHom.mem_ker, MonoidHom.map_inv, MonoidHom.map_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ Eq.{u_6 + 1} (α := G₂) ((f : (a : G₁) → G₂) (f_inv ((f : (a : G₁) → G₂) x)) : G₂) ((f : (a : G₁) → G₂) x : G₂)

Tactic:
simp only [hf _]
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
φ : G₂ →* G₃
x : G₁
hx : x ∈ f.ker
⊢ Eq.{u_7 + 1} (α := G₃) ((φ.comp f : (a : G₁) → G₃) x : G₃) (1 : G₃)

Tactic:
simp [mem_ker.mp hx]

Premises used: MonoidHom.mem_ker, Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : { g : G₁ →* G₃ // f.ker ≤ g.ker }
a :
  ∀ (x : G₁),
    Eq.{u_7 + 1} (α := G₃)
      (((↑((fun (φ : G₂ →* G₃) ↦
                    (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) ⋯ :
                      { g : G₁ →* G₃ // f.ker ≤ g.ker }))
                  ((fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) ⋯)
                    g)) :
              G₁ →* G₃) :
            (a : G₁) → G₃)
          x :
        G₃)
      (((↑g : G₁ →* G₃) : (a : G₁) → G₃) x : G₃)
⊢ (fun (φ : G₂ →* G₃) ↦
        (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) ⋯ : { g : G₁ →* G₃ // f.ker ≤ g.ker }))
      ((fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) ⋯) g) =
    g

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : { g : G₁ →* G₃ // f.ker ≤ g.ker }
x : G₁
⊢ Eq.{u_7 + 1} (α := G₃)
    (((↑((fun (φ : G₂ →* G₃) ↦
                  (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) ⋯ :
                    { g : G₁ →* G₃ // f.ker ≤ g.ker }))
                ((fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) ⋯)
                  g)) :
            G₁ →* G₃) :
          (a : G₁) → G₃)
        x :
      G₃)
    (((↑g : G₁ →* G₃) : (a : G₁) → G₃) x : G₃)

Tactic:
simp only [comp_apply, liftOfRightInverseAux_comp_apply]

Premises used: MonoidHom.liftOfRightInverseAux_comp_apply, MonoidHom.comp_apply
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
φ : G₂ →* G₃
h :
  ∀ (b : G₂),
    Eq.{u_7 + 1} (α := G₃)
      (((fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) ⋯)
              ((fun (φ : G₂ →* G₃) ↦
                  (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) ⋯ :
                    { g : G₁ →* G₃ // f.ker ≤ g.ker }))
                φ) :
            (a : G₂) → G₃)
          b :
        G₃)
      ((φ : (a : G₂) → G₃) b : G₃)
⊢ (fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) ⋯)
      ((fun (φ : G₂ →* G₃) ↦
          (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) ⋯ : { g : G₁ →* G₃ // f.ker ≤ g.ker }))
        φ) =
    φ

Tactic:
ext b
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
φ : G₂ →* G₃
b : G₂
⊢ Eq.{u_7 + 1} (α := G₃)
    (((fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) ⋯)
            ((fun (φ : G₂ →* G₃) ↦
                (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) ⋯ : { g : G₁ →* G₃ // f.ker ≤ g.ker }))
              φ) :
          (a : G₂) → G₃)
        b :
      G₃)
    ((φ : (a : G₂) → G₃) b : G₃)

Tactic:
simp [liftOfRightInverseAux, hf b]

Premises used: MonoidHom.liftOfRightInverseAux
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : { g : G₁ →* G₃ // f.ker ≤ g.ker }
x : G₁
⊢ Eq.{u_7 + 1} (α := G₃)
    ((((f.liftOfRightInverse f_inv hf : (a : { g : G₁ →* G₃ // f.ker ≤ g.ker }) → G₂ →* G₃) g : G₂ →* G₃) :
          (a : G₂) → G₃)
        ((f : (a : G₁) → G₂) x : G₂) :
      G₃)
    (((↑g : G₁ →* G₃) : (a : G₁) → G₃) x : G₃)

Tactic:
f.liftOfRightInverseAux_comp_apply f_inv hf g.1 g.2 x

Premises used: MonoidHom.liftOfRightInverseAux_comp_apply, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Group.Subgroup.Basic
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : { g : G₁ →* G₃ // f.ker ≤ g.ker }
⊢ comp ((f.liftOfRightInverse f_inv hf : (a : { g : G₁ →* G₃ // f.ker ≤ g.ker }) → G₂ →* G₃) g) f = (↑g : G₁ →* G₃)

Tactic:
MonoidHom.ext <| f.liftOfRightInverse_comp_apply f_inv hf g

Premises used: MonoidHom.ext, MonoidHom.liftOfRightInverse_comp_apply