awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
f : G →* N
simp_rw : ∀ (x : N), x ∈ range (f.restrict K) ↔ x ∈ map f K
⊢ range (f.restrict K) = map f K
have simp_rw₁ : ∀ (x : N), (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔ x ∈ map f K
Tactic: simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
    exists_prop, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
f : G →* N
simp_rw : ∀ (x : N), x ∈ range (f.restrict K) ↔ x ∈ map f K
simp_rw₁ :
  ∀ (x : N), (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔ x ∈ map f K
⊢ range (f.restrict K) = map f K
have simp_rw₂ : ∀ (x : N),
  (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔
    ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
Tactic: simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
    exists_prop, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
f : G →* N
simp_rw : ∀ (x : N), x ∈ range (f.restrict K) ↔ x ∈ map f K
simp_rw₁ :
  ∀ (x : N), (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔ x ∈ map f K
simp_rw₂ :
  ∀ (x : N),
    (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔
      ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
⊢ range (f.restrict K) = map f K
have simp_rw₃ : ∀ (x : N), (∃ (x_1 : ↥K), (f : (a : G) → N) (↑x_1 : G) = x) ↔ ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
Tactic: simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
    exists_prop, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
f : G →* N
simp_rw : ∀ (x : N), x ∈ range (f.restrict K) ↔ x ∈ map f K
simp_rw₁ :
  ∀ (x : N), (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔ x ∈ map f K
simp_rw₂ :
  ∀ (x : N),
    (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔
      ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
simp_rw₃ : ∀ (x : N), (∃ (x_1 : ↥K), (f : (a : G) → N) (↑x_1 : G) = x) ↔ ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
⊢ range (f.restrict K) = map f K
have simp_rw₄ : ∀ (x : N), (∃ (x_1 : G) (_ : x_1 ∈ K), (f : (a : G) → N) x_1 = x) ↔ ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
Tactic: simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
    exists_prop, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
K : Subgroup G
f : G →* N
simp_rw : ∀ (x : N), x ∈ range (f.restrict K) ↔ x ∈ map f K
simp_rw₁ :
  ∀ (x : N), (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔ x ∈ map f K
simp_rw₂ :
  ∀ (x : N),
    (∃ (x_1 : ↥K), ((f.restrict K : MonoidHom.{u_1, u_5} (↥K) N) : (a : ↥K) → N) x_1 = x) ↔
      ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
simp_rw₃ : ∀ (x : N), (∃ (x_1 : ↥K), (f : (a : G) → N) (↑x_1 : G) = x) ↔ ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
simp_rw₄ : ∀ (x : N), (∃ (x_1 : G) (_ : x_1 ∈ K), (f : (a : G) → N) x_1 = x) ↔ ∃ x_1 ∈ K, (f : (a : G) → N) x_1 = x
⊢ range (f.restrict K) = map f K
have simp_rw₅ : ∀ (x : N), True
Tactic: simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,
    exists_prop, forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
P : Type u_6
inst_1 : Group N
inst_2 : Group P
g : N →* P
f : G →* N
⊢ map g f.range = (g.comp f).range
have rw : map g (map f ⊤) = map (g.comp f) ⊤
Tactic: rw [range_eq_map, range_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_7
inst_1 : Group N
f : G →* N
⊢ (↑f.range : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ
have rw : Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑⊤ : Set N) ↔
  Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ
Tactic: rw [coe_range, coe_top]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_7
inst_1 : Group N
f : G →* N
rw :
  Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑⊤ : Set N) ↔
    Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ
⊢ (↑f.range : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ
have rw₁ : Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ ↔
  Eq.{u_7 + 1} (α := Set N) (Set.range.{u_7, u_1 + 1} (ι := G) (⇑f : (a : G) → N)) Set.univ
Tactic: rw [coe_range, coe_top]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ f.range.subgroupOf K = range (f.codRestrict K ⋯)
have h₁ : ∀ (k : ↥K), k ∈ f.range.subgroupOf K ↔ k ∈ range (f.codRestrict K sorry)
Tactic: ext k
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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 ⋯)
have h₁ : ∀ (a : G₁),
  Eq.{u_8 + 1} (α := G₂) ((f : (a : G₁) → G₂) a : G₂) ((K.subtype : (a : ↥K) → G₂) k : G₂) ↔
    ((f.codRestrict K sorry : MonoidHom.{u_7, u_8} G₁ ↥K) : (a : G₁) → ↥K) a = k
Tactic: refine exists_congr ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ (f : (a : G) → M) x⁻¹ = HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) x⁻¹ : M)
have rw : (f : (a : G) → M) x⁻¹ = HMul.hMul (α := M) (β := M) (1 : M) ((f : (a : G) → M) x⁻¹ : M)
Tactic: rw [hx, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ (f : (a : G) → M) x⁻¹ = HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) x⁻¹ : M)
have rw₁ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x⁻¹ : M) ((f : (a : G) → M) x⁻¹ : M)
Tactic: rw [hx, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) x⁻¹ : M) = 1
have rw : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (x * x⁻¹) : M) (1 : M)
Tactic: rw [← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) x⁻¹ : M) = 1
have rw₁ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) 1 : M) (1 : M)
Tactic: rw [← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) x⁻¹ : M) = 1
have rw₂ : Eq.{u_7 + 1} (α := M) 1 1
Tactic: rw [← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x y : G
⊢ x / y ∈ f.ker ↔ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mp : x / y ∈ f.ker → Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ x / y ∈ f.ker ↔ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mpr : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M) → x / y ∈ f.ker
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mp : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (x / y * y) : M) ((f : (a : G) → M) y : M)
Tactic: rw [← div_mul_cancel x y, map_mul, mem_ker.mp h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mp₁ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) (x / y) : M) ((f : (a : G) → M) y : M) = (f : (a : G) → M) y
Tactic: rw [← div_mul_cancel x y, map_mul, mem_ker.mp h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mp₂ : HMul.hMul (α := M) (β := M) (1 : M) ((f : (a : G) → M) y : M) = (f : (a : G) → M) y
Tactic: rw [← div_mul_cancel x y, map_mul, mem_ker.mp h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mp₃ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) y : M)
Tactic: rw [← div_mul_cancel x y, map_mul, mem_ker.mp h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ x / y ∈ f.ker
have mpr : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (x / y) : M) (1 : M)
Tactic: rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ x / y ∈ f.ker
have mpr₁ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (x * y⁻¹) : M) (1 : M)
Tactic: rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ x / y ∈ f.ker
have mpr₂ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y⁻¹ : M) = 1
Tactic: rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ x / y ∈ f.ker
have mpr₃ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) y⁻¹ : M) = 1
Tactic: rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ x / y ∈ f.ker
have mpr₄ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * y⁻¹) : M) (1 : M)
Tactic: rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ x / y ∈ f.ker
have mpr₅ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) 1 : M) (1 : M)
Tactic: rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ x / y ∈ f.ker
have mpr₆ : Eq.{u_7 + 1} (α := M) 1 1
Tactic: rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
M : Type u_8
inst_1 : Monoid M
f : G →* M
⊢ f.toHomUnits.ker = f.ker
have h : ∀ (x : G), x ∈ f.toHomUnits.ker ↔ x ∈ f.ker
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
M : Type u_7
inst_1 : MulOneClass M
f : G →* M
x y : G
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M) ↔ y⁻¹ * x ∈ f.ker
have mp : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M) → y⁻¹ * x ∈ f.ker
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M) ↔ y⁻¹ * x ∈ f.ker
have mpr : y⁻¹ * x ∈ f.ker → Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ y⁻¹ * x ∈ f.ker
have mp : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y⁻¹ * x) : M) (1 : M)
Tactic: rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ y⁻¹ * x ∈ f.ker
have mp₁ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y⁻¹ : M) ((f : (a : G) → M) x : M) = 1
Tactic: rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ y⁻¹ * x ∈ f.ker
have mp₂ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y⁻¹ : M) ((f : (a : G) → M) y : M) = 1
Tactic: rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ y⁻¹ * x ∈ f.ker
have mp₃ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y⁻¹ * y) : M) (1 : M)
Tactic: rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ y⁻¹ * x ∈ f.ker
have mp₄ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) 1 : M) (1 : M)
Tactic: rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ y⁻¹ * x ∈ f.ker
have mp₅ : Eq.{u_7 + 1} (α := M) 1 1
Tactic: rw [mem_ker, map_mul, h, ← map_mul, inv_mul_cancel, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mpr : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (1 * 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mpr₁ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * y⁻¹ * 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mpr₂ : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * (y⁻¹ * 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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)
⊢ Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
have mpr₃ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) (y⁻¹ * x) : M) = (f : (a : G) → M) y
Tactic: rw [← one_mul x, ← mul_inv_cancel y, mul_assoc, map_mul, mem_ker.1 h, mul_one]