awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G₁ : Type u_7
G₂ : Type u_8
inst : Group G₁
inst_1 : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
h₁ : ∀ (k : ↥K), k ∈ f.range.subgroupOf K ↔ k ∈ range (f.codRestrict K ⋯)
⊢ f.range.subgroupOf K = range (f.codRestrict K ⋯)

Tactic:
ext k
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G₁ : Type u_7
G₂ : Type u_8
inst : Group G₁
inst_1 : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ k ∈ f.range.subgroupOf K ↔ k ∈ range (f.codRestrict K ⋯)

Tactic:
exists_congr ?_

Premises used: Set.Mem, setOf, exists_congr, Set.preimage, Set.range
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G₁ : Type u_7
G₂ : Type u_8
inst : Group G₁
inst_1 : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
h₁ :
  ∀ (a : G₁),
    Eq.{u_8 + 1} (α := G₂) ((f : (a : G₁) → G₂) a : G₂) ((K.subtype : (a : ↥K) → G₂) k : G₂) ↔
      ((f.codRestrict K ⋯ : MonoidHom.{u_7, u_8} G₁ ↥K) : (a : G₁) → ↥K) a = k
⊢ k ∈ f.range.subgroupOf K ↔ k ∈ range (f.codRestrict K ⋯)

Tactic:
refine exists_congr ?_

Premises used: exists_congr
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G₁ : Type u_7
G₂ : Type u_8
inst : Group G₁
inst_1 : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
k : ↥K
⊢ ∀ (a : G₁),
    Eq.{u_8 + 1} (α := G₂) ((f : (a : G₁) → G₂) a : G₂) ((K.subtype : (a : ↥K) → G₂) k : G₂) ↔
      ((f.codRestrict K ⋯ : MonoidHom.{u_7, u_8} G₁ ↥K) : (a : G₁) → ↥K) a = k

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
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
N : Type u_5
P : Type u_6
inst_4 : Group N
inst_5 : Group P
K : Subgroup G
f : G →* N
g : N →* G
h : LeftInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
y : G
⊢ Eq (α := ↥f.range)
    ((f.rangeRestrict : (a : G) → ↥f.range)
        (Function.comp (α := ↥f.range) (β := N) (⇑g : (a : N) → G)
          ((⇑f.range.subtype : (a : ↥f.range) → N) : (a : ↥f.range) → N)
          (Subtype.mk (p := fun (x : N) ↦ x ∈ f.range) ((f : (a : G) → N) y) ⋯ : ↥f.range)) :
      ↥f.range)
    (Subtype.mk (p := fun (x : N) ↦ x ∈ f.range) ((f : (a : G) → N) y) ⋯ : ↥f.range)

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
g : N →* G
h : LeftInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
x : G
⊢ Eq.{u_5 + 1} (α := N) ((↑((ofLeftInverse h : (a : G) → ↥f.range) x) : N) : N) ((f : (a : G) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
g : N →* G
h : LeftInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
x : ↥f.range
⊢ Eq.{u_1 + 1} (α := G) (((ofLeftInverse h).symm : (a : ↥f.range) → G) x : G) ((g : (a : N) → G) (↑x : N) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
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
N : Type u_5
P : Type u_6
inst_4 : Group N
inst_5 : Group P
K : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
y : G
⊢ ∃ (a : G),
    Eq.{u_5 + 1} (α := ↥f.range)
      (((f.codRestrict f.range ⋯ : MonoidHom.{u_1, u_5} G ↥f.range) : (a : G) → ↥f.range) a : ↥f.range)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ f.range) ((f : (a : G) → N) y) ⋯ : ↥f.range)

Tactic:
⟨y, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
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
N : Type u_5
P : Type u_6
inst_4 : Group N
inst_5 : Group P
K : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
y : G
⊢ ∃ (a : G),
    Eq.{u_5 + 1} (α := ↥f.range)
      (((f.codRestrict f.range ⋯ : MonoidHom.{u_1, u_5} G ↥f.range) : (a : G) → ↥f.range) a : ↥f.range)
      (Subtype.mk (p := fun (x : N) ↦ x ∈ f.range) ((f : (a : G) → N) y) ⋯ : ↥f.range)

Tactic:
exact ⟨y, rfl⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
x : G
⊢ Eq.{u_5 + 1} (α := N) ((↑((ofInjective hf : (a : G) → ↥f.range) x) : N) : N) ((f : (a : G) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
x : ↥f.range
⊢ (f : (a : G) → N) (((ofInjective hf).symm : (a : ↥f.range) → G) x : G) = (↑x : N)

Tactic:
Subtype.ext_iff.1 <| (ofInjective hf).apply_symm_apply x

Premises used: Subtype.ext_iff, Iff.mp, MonoidHom.ofInjective, MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ Eq.{u_2 + 1} (α := AddSubgroup (Additive G'))
    (AddMonoidHom.range.{u_1, u_2} (G := Additive G) ((toAdditive : (a : G →* G') → Additive G →+ Additive G') f))
    ((toAddSubgroup : (a : Subgroup G') → AddSubgroup (Additive G')) f.range)

Tactic:
rfl

Premises used: Set.Mem, Additive, setOf, AddMonoidHom.range, AddSubgroup.copy, Set.preimage, Set.range, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
A : Type u_7
A' : Type u_8
inst : AddGroup A
inst_1 : AddGroup A'
f : A →+ A'
⊢ Eq.{u_8 + 1} (α := Subgroup (Multiplicative A'))
    (range.{u_7, u_8} (G := Multiplicative A)
      ((AddMonoidHom.toMultiplicative : (a : A →+ A') → Multiplicative A →* Multiplicative A') f))
    ((AddSubgroup.toSubgroup : (a : AddSubgroup A') → Subgroup (Multiplicative A')) f.range)

Tactic:
rfl

Premises used: MonoidHom.range, Set.Mem, setOf, Subgroup.copy, Multiplicative, Set.preimage, Set.range, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
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
N : Type u_5
P : Type u_6
inst_4 : Group N
inst_5 : Group P
K : Subgroup G
M : Type u_7
inst_6 : MulOneClass M
f : G →* M
x : G
hx : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) (1 : M)
rw : (f : (a : G) → M) x⁻¹ = HMul.hMul (α := M) (β := M) (1 : M) ((f : (a : G) → M) x⁻¹ : M)
rw₁ rw₂ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x⁻¹ : M) ((f : (a : G) → M) x⁻¹ : M)
⊢ (f : (a : G) → M) x⁻¹ = HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) x⁻¹ : M)

Tactic:
rw [hx, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
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
N : Type u_5
P : Type u_6
inst_4 : Group N
inst_5 : Group P
K : Subgroup G
M : Type u_7
inst_6 : MulOneClass M
f : G →* M
x : G
hx : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) (1 : M)
rw : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (x * x⁻¹) : M) (1 : M)
rw₁ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) 1 : M) (1 : M)
rw₂ rw₃ : Eq.{u_7 + 1} (α := M) 1 1
⊢ HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) x⁻¹ : M) = 1

Tactic:
rw [← map_mul, mul_inv_cancel, map_one]

Premises used: map_mul, map_one, mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
⊢ f.ker.toSubmonoid = mker f

Tactic:
rfl

Premises used: MonoidHom.mker, Submonoid.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x : G
⊢ x ∈ f.ker ↔ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) (1 : M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x y : G
mp : x / y ∈ f.ker → Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
mpr : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M) → x / y ∈ f.ker
⊢ x / y ∈ f.ker ↔ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x y : G
h : x / y ∈ f.ker
mp : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (x / y * y) : M) ((f : (a : G) → M) y : M)
mp₁ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) (x / y) : M) ((f : (a : G) → M) y : M) = (f : (a : G) → M) y
mp₂ : HMul.hMul (α := M) (β := M) (1 : M) ((f : (a : G) → M) y : M) = (f : (a : G) → M) y
mp₃ mp₄ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) y : M)
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)

Tactic:
rw [← div_mul_cancel x y, map_mul, mem_ker.mp h, one_mul]

Premises used: MonoidHom.mem_ker, map_mul, Iff.mp, div_mul_cancel, one_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x y : G
h : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
mpr : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (x / y) : M) (1 : M)
mpr₁ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (x * y⁻¹) : M) (1 : M)
mpr₂ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y⁻¹ : M) = 1
mpr₃ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) y⁻¹ : M) = 1
mpr₄ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * y⁻¹) : M) (1 : M)
mpr₅ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) 1 : M) (1 : M)
mpr₆ mpr₇ : Eq.{u_7 + 1} (α := M) 1 1
⊢ x / y ∈ f.ker

Tactic:
rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]

Premises used: MonoidHom.mem_ker, div_eq_mul_inv, map_mul, map_one, mul_inv_cancel
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
⊢ (↑f.ker : Set G) = Set.preimage (β := M) (⇑f : (a : G) → M) {1}

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_8
inst_1 : Monoid M
f : G →* M
h : ∀ (x : G), x ∈ f.toHomUnits.ker ↔ x ∈ f.ker
⊢ f.toHomUnits.ker = f.ker

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_8
inst_1 : Monoid M
f : G →* M
x : G
⊢ x ∈ f.toHomUnits.ker ↔ x ∈ f.ker

Tactic:
simp [mem_ker, Units.ext_iff]

Premises used: Units.ext_iff, MonoidHom.mem_ker
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x y : G
mp : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M) → y⁻¹ * x ∈ f.ker
mpr : y⁻¹ * x ∈ f.ker → Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M) ↔ y⁻¹ * x ∈ f.ker

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x y : G
h : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
mp : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y⁻¹ * x) : M) (1 : M)
mp₁ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y⁻¹ : M) ((f : (a : G) → M) x : M) = 1
mp₂ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y⁻¹ : M) ((f : (a : G) → M) y : M) = 1
mp₃ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y⁻¹ * y) : M) (1 : M)
mp₄ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) 1 : M) (1 : M)
mp₅ mp₆ : Eq.{u_7 + 1} (α := M) 1 1
⊢ y⁻¹ * x ∈ f.ker

Tactic:
rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]

Premises used: inv_mul_cancel, MonoidHom.mem_ker, map_mul, map_one
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
mpr : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (1 * x) : M) ((f : (a : G) → M) y : M)
mpr₁ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * y⁻¹ * x) : M) ((f : (a : G) → M) y : M)
mpr₂ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * (y⁻¹ * x)) : M) ((f : (a : G) → M) y : M)
mpr₃ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) (y⁻¹ * x) : M) = (f : (a : G) → M) y
mpr₄ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) (1 : M) = (f : (a : G) → M) y
mpr₅ mpr₆ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) y : M)
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)

Tactic:
rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]

Premises used: mul_assoc, MonoidHom.mem_ker, map_mul, Iff.mp, mul_inv_cancel, mul_one, one_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
P : Type u_8
inst_2 : MulOneClass P
g : N →* P
f : G →* N
⊢ comap f g.ker = (g.comp f).ker

Tactic:
rfl

Premises used: MonoidHom.mker, Set.Mem, setOf, MonoidHom.ker, Submonoid.comap, Set.preimage, Set.singleton, Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
P : Type u_8
inst_2 : MulOneClass P
g : N →* P
iso : G ≃* N
rw : Eq (α := Subgroup G) (comap (↑iso : G →* N) g.ker) (map (↑iso.symm : N →* G) g.ker)
rw₁ rw₂ : Eq (α := Subgroup G) (map (↑iso.symm : N →* G) g.ker) (map (↑iso.symm : N →* G) g.ker)
⊢ Eq (α := Subgroup G) (ker (g.comp (↑iso : G →* N))) (map (↑iso.symm : N →* G) g.ker)

Tactic:
rw [← comap_ker, comap_equiv_eq_map_symm]

Premises used: Subgroup.comap_equiv_eq_map_symm, MonoidHom.comap_ker
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
P : Type u_8
inst_2 : MulOneClass P
f : G →* N
iso : N ≃* P
h : ∀ (x : G), x ∈ ker (comp (↑iso : N →* P) f) ↔ x ∈ f.ker
⊢ ker (comp (↑iso : N →* P) f) = f.ker

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
P : Type u_8
inst_2 : MulOneClass P
f : G →* N
iso : N ≃* P
x : G
⊢ x ∈ ker (comp (↑iso : N →* P) f) ↔ x ∈ f.ker

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ comap f ⊥ = f.ker

Tactic:
rfl

Premises used: MonoidHom.mker, MonoidHom.ker, Submonoid.comap, Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
⊢ ker (f.restrict K) = f.ker.subgroupOf K

Tactic:
rfl

Premises used: Subgroup.subgroupOf, MonoidHom.mker, Set.Mem, setOf, MonoidHom.ker, Submonoid.comap, Set.preimage, Set.singleton, Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
S : Type u_8
inst_2 : SetLike S N
inst_3 : SubmonoidClass S N
f : G →* N
s : S
h : ∀ (x : G), Membership.mem.{u_5, u_8} (α := N) s ((f : (a : G) → N) x : N)
⊢ ker (f.codRestrict s h : MonoidHom.{u_1, u_5} G ↥s) = f.ker

Tactic:
SetLike.ext fun _x => Subtype.ext_iff

Premises used: Subtype.ext_iff, SetLike.ext
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ f.rangeRestrict.ker = f.ker

Tactic:
ker_codRestrict _ _ _

Premises used: MonoidHom.rangeRestrict, MonoidHom.ker_codRestrict
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
⊢ Eq.{u_1 + 1} (α := Subgroup G) (ker.{u_1, u_7} (M := M) 1) ⊤

Tactic:
SetLike.ext fun _x => eq_self_iff_true _

Premises used: SetLike.ext, OfNat.ofNat, DFunLike.coe, eq_self_iff_true
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (ker (id G)) ⊥

Tactic:
rfl

Premises used: MonoidHom.mker, Set.Mem, setOf, MonoidHom.ker, Submonoid.comap, Set.preimage, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
⊢ f.ker = ⊤ ↔ f = 1

Tactic:
simp [ker, ← top_le_iff, SetLike.le_def, f.ext_iff]

Premises used: SetLike.le_def, MonoidHom.ext_iff, MonoidHom.ker, top_le_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
rw : f.range ≤ ⊥ ↔ f = 1
rw₁ : map f ⊤ ≤ ⊥ ↔ f = 1
rw₂ : ⊤ ≤ comap f ⊥ ↔ f = 1
rw₃ : comap f ⊥ = ⊤ ↔ f = 1
rw₄ : f.ker = ⊤ ↔ f = 1
rw₅ rw₆ : f = 1 ↔ f = 1
⊢ f.range = ⊥ ↔ f = 1

Tactic:
rw [← le_bot_iff, f.range_eq_map, map_le_iff_le_comap, top_le_iff, comap_bot, ker_eq_top_iff]

Premises used: le_bot_iff, MonoidHom.comap_bot, MonoidHom.ker_eq_top_iff, MonoidHom.range_eq_map, Subgroup.map_le_iff_le_comap, top_le_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
rwa : ∀ (hxy : y⁻¹ * x ∈ f.ker), x = y
rwa₁ : ∀ (hxy : Membership.mem (γ := Subgroup G) ⊥ (y⁻¹ * x)), x = y
rwa₂ : ∀ (hxy : y⁻¹ * x = 1), x = y
rwa₃ : ∀ (hxy : y = x), x = y
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (hxy : x = y), x = y
⊢ x = y

Tactic:
rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy

Premises used: eq_comm, MonoidHom.eq_iff, Subgroup.mem_bot, inv_mul_eq_one
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H.subtype.ker = ⊥

Tactic:
H.subtype.ker_eq_bot_iff.mpr Subtype.coe_injective

Premises used: Iff.mpr, Subgroup.subtype, Subtype.coe_injective, MonoidHom.ker_eq_bot_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ (inclusion h).ker = ⊥

Tactic:
(inclusion h).ker_eq_bot_iff.mpr (Set.inclusion_injective h)

Premises used: Iff.mpr, Subgroup.inclusion, Set.inclusion_injective, MonoidHom.ker_eq_bot_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_8
N : Type u_9
inst_1 : MulOneClass M
inst_2 : MulOneClass N
f : G →* M
g : G →* N
⊢ (f.prod g).ker = f.ker ⊓ g.ker

Tactic:
SetLike.ext fun _ => Prod.mk_eq_one

Premises used: Prod.mk_eq_one, SetLike.ext
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
M : Type u_7
inst_2 : MulOneClass M
f : G →* G'
g : G' →* M
h : g.comp f = 1
y : G
⊢ Membership.mem (α := G') g.ker ((f : (a : G) → G') y : G')

Tactic:
DFunLike.congr_fun h y

Premises used: DFunLike.congr_fun, Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
M : Type u_7
inst_2 : MulOneClass M
f : G →* G'
g : G' →* M
h : g.comp f = 1
y : G
⊢ Membership.mem (α := G') g.ker ((f : (a : G) → G') y : G')

Tactic:
exact DFunLike.congr_fun h y

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
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
N : Type u_5
P : Type u_6
inst_4 : Group N
inst_5 : Group P
K : Subgroup G
M : Type u_7
inst_6 : MulOneClass M
f : G →* M
x : G
hx : x ∈ f.ker
y : G
rw : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * x * y⁻¹) : M) (1 : M)
rw₁ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) (y * x) : M) ((f : (a : G) → M) y⁻¹ : M) = 1
rw₂ :
  HMul.hMul (β := M) (HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) x : M))
      ((f : (a : G) → M) y⁻¹ : M) =
    1
rw₃ : HMul.hMul (β := M) (HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) (1 : M)) ((f : (a : G) → M) y⁻¹ : M) = 1
rw₄ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) y⁻¹ : M) = 1
rw₅ rw₆ : Eq.{u_7 + 1} (α := M) 1 1
⊢ y * x * y⁻¹ ∈ f.ker

Tactic:
rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]

Premises used: MonoidHom.mem_ker, map_mul, Iff.mp, map_mul_eq_one, mul_inv_cancel, mul_one
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ Eq.{u_1 + 1} (α := AddSubgroup (Additive G))
    (AddMonoidHom.ker.{u_1, u_2} (M := Additive G') ((toAdditive : (a : G →* G') → Additive G →+ Additive G') f))
    ((toAddSubgroup : (a : Subgroup G) → AddSubgroup (Additive G)) f.ker)

Tactic:
rfl

Premises used: Set.Mem, Additive, setOf, AddMonoidHom.mker, AddSubmonoid.comap, Set.preimage, Set.singleton, rfl, AddMonoidHom.ker
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
A : Type u_8
A' : Type u_9
inst : AddGroup A
inst_1 : AddZeroClass A'
f : A →+ A'
⊢ Eq.{u_8 + 1} (α := Subgroup (Multiplicative A))
    (ker.{u_8, u_9} (M := Multiplicative A')
      ((AddMonoidHom.toMultiplicative : (a : A →+ A') → Multiplicative A →* Multiplicative A') f))
    ((AddSubgroup.toSubgroup : (a : AddSubgroup A) → Subgroup (Multiplicative A)) f.ker)

Tactic:
rfl

Premises used: MonoidHom.mker, Set.Mem, setOf, Multiplicative, MonoidHom.ker, Submonoid.comap, Set.preimage, Set.singleton, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
⊢ f.eqLocus f = ⊤

Tactic:
SetLike.ext fun _ => eq_self_iff_true _

Premises used: SetLike.ext, DFunLike.coe, eq_self_iff_true
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : Monoid M
f g : G →* M
s : Set G
h : Set.EqOn.{u_1, u_7} (β := M) (⇑f : (a : G) → M) (⇑g : (a : G) → M) s
⊢ Set.EqOn.{u_1, u_7} (β := M) (⇑f : (a : G) → M) (⇑g : (a : G) → M) (↑(closure s) : Set G)

Tactic:
show closure s ≤ f.eqLocus g from (closure_le _).2 h

Premises used: Iff.mpr, Set.Mem, setOf, Subgroup.closure_le, Set.EqOn, MonoidHom.eqLocus
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : Monoid M
f g : G →* M
h : Set.EqOn.{u_1, u_7} (β := M) (⇑f : (a : G) → M) (⇑g : (a : G) → M) (↑⊤ : Set G)
⊢ f = g

Tactic:
ext fun _x => h trivial

Premises used: trivial, MonoidHom.ext
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : Monoid M
s : Set G
hs : Eq (α := Subgroup G) (closure s) ⊤
f g : G →* M
h : Set.EqOn.{u_1, u_7} (β := M) (⇑f : (a : G) → M) (⇑g : (a : G) → M) s
⊢ f = g

Tactic:
eq_of_eqOn_top <| hs ▸ eqOn_closure h

Premises used: MonoidHom.eq_of_eqOn_top, Eq.rec, MonoidHom.eqOn_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G →* N
⊢ map f H = ⊥ ↔ H ≤ f.ker

Tactic:
(gc_map_comap f).l_eq_bot

Premises used: Subgroup.gc_map_comap, Set.Mem, GaloisConnection.l_eq_bot
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
rw : H ≤ f.ker ↔ H = ⊥
rw₁ : H ≤ ⊥ ↔ H = ⊥
rw₂ rw₃ : H = ⊥ ↔ H = ⊥
⊢ map f H = ⊥ ↔ H = ⊥

Tactic:
rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]

Premises used: le_bot_iff, Iff.mpr, Subgroup.map_eq_bot_iff, MonoidHom.ker_eq_bot_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
⊢ map f H ≤ f.range

Tactic:
(range_eq_map f).symm ▸ map_mono le_top

Premises used: MonoidHom.range_eq_map, Eq.rec, le_top, Subgroup.map_mono, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
K : Subgroup ↥H
⊢ map H.subtype K ≤ H

Tactic:
(K.map_le_range H.subtype).trans_eq H.range_subtype

Premises used: Subgroup.map_le_range, LE.le.trans_eq, Subgroup.subtype, Subgroup.range_subtype
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup N
⊢ f.ker ≤ comap f H

Tactic:
comap_bot f ▸ comap_mono bot_le

Premises used: MonoidHom.comap_bot, Eq.rec, Subgroup.comap_mono, bot_le