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
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
⊢ 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) (1 : 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]
-- 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)
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
⊢ 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 : 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
N : Type u_5
inst_1 : Group N
P : Type u_8
inst_2 : MulOneClass P
g : N →* P
iso : G ≃* N
⊢ Eq (α := Subgroup G) (ker (g.comp (↑iso : G →* N))) (map (↑iso.symm : N →* G) g.ker)
have rw : Eq (α := Subgroup G) (comap (↑iso : G →* N) g.ker) (map (↑iso.symm : N →* G) g.ker)
Tactic: rw [← comap_ker, comap_equiv_eq_map_symm]
-- 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
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)
⊢ Eq (α := Subgroup G) (ker (g.comp (↑iso : G →* N))) (map (↑iso.symm : N →* G) g.ker)
have rw₁ : Eq (α := Subgroup G) (map (↑iso.symm : N →* G) g.ker) (map (↑iso.symm : N →* G) g.ker)
Tactic: rw [← comap_ker, comap_equiv_eq_map_symm]
-- 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
P : Type u_8
inst_2 : MulOneClass P
f : G →* N
iso : N ≃* P
⊢ ker (comp (↑iso : N →* P) f) = f.ker
have h : ∀ (x : G), x ∈ ker (comp (↑iso : N →* P) f) ↔ x ∈ f.ker
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ f.range = ⊥ ↔ f = 1
have rw : 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
rw : f.range ≤ ⊥ ↔ f = 1
⊢ f.range = ⊥ ↔ f = 1
have rw₁ : map f ⊤ ≤ ⊥ ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ f.range = ⊥ ↔ f = 1
have rw₂ : ⊤ ≤ comap f ⊥ ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ f.range = ⊥ ↔ f = 1
have rw₃ : comap f ⊥ = ⊤ ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ f.range = ⊥ ↔ f = 1
have rw₄ : f.ker = ⊤ ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
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
⊢ f.range = ⊥ ↔ f = 1
have rw₅ : f = 1 ↔ 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]
-- 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
h : f.ker = ⊥
x y : G
hxy : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
⊢ x = y
have rwa : ∀ (hxy : y⁻¹ * x ∈ f.ker), x = y
Tactic: rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy
Cleared hypotheses: hxy
-- 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
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
⊢ x = y
have rwa₁ : ∀ (hxy : Membership.mem (γ := Subgroup G) ⊥ (y⁻¹ * x)), x = y
Tactic: rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy
Cleared hypotheses: hxy
-- 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
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
⊢ x = y
have rwa₂ : ∀ (hxy : y⁻¹ * x = 1), x = y
Tactic: rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy
Cleared hypotheses: hxy
-- 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
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
⊢ x = y
have rwa₃ : ∀ (hxy : y = x), x = y
Tactic: rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy
Cleared hypotheses: hxy
-- 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
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
⊢ x = y
have rwa₄ : ∀ (hxy : x = y), x = y
Tactic: rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy
Cleared hypotheses: hxy
-- 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 : x ∈ f.ker
y : G
⊢ y * x * y⁻¹ ∈ f.ker
have rw : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * x * y⁻¹) : M) (1 : M)
Tactic: rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]
-- 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 : x ∈ f.ker
y : G
rw : Eq.{u_7 + 1} (α := M) ((f : (a : G) → M) (y * x * y⁻¹) : M) (1 : M)
⊢ y * x * y⁻¹ ∈ f.ker
have rw₁ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) (y * x) : M) ((f : (a : G) → M) y⁻¹ : M) = 1
Tactic: rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]
-- 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 : 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
⊢ y * x * y⁻¹ ∈ f.ker
have 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
Tactic: rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]
-- 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 : 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
⊢ y * x * y⁻¹ ∈ f.ker
have rw₃ : HMul.hMul (β := M) (HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) (1 : M)) ((f : (a : G) → M) y⁻¹ : M) = 1
Tactic: rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]
-- 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 : 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
⊢ y * x * y⁻¹ ∈ f.ker
have rw₄ : HMul.hMul (α := M) (β := M) ((f : (a : G) → M) y : M) ((f : (a : G) → M) y⁻¹ : M) = 1
Tactic: rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]
-- 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 : 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
⊢ y * x * y⁻¹ ∈ f.ker
have rw₅ : Eq.{u_7 + 1} (α := M) 1 1
Tactic: rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]
-- 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
H : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ map f H = ⊥ ↔ H = ⊥
have rw : H ≤ f.ker ↔ H = ⊥
Tactic: rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]
-- 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
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 = ⊥
⊢ map f H = ⊥ ↔ H = ⊥
have rw₁ : H ≤ ⊥ ↔ H = ⊥
Tactic: rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]
-- 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
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 = ⊥
⊢ map f H = ⊥ ↔ H = ⊥
have rw₂ : H = ⊥ ↔ H = ⊥
Tactic: rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]
-- 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
f : G →* N
H : Subgroup N
⊢ (↑(map f (comap f H)) : Set N) = (↑(f.range ⊓ H) : Set N)
have rw : (⇑f : (a : G) → N) '' (↑(comap f H) : Set G) = (↑(f.range ⊓ H) : Set N)
Tactic: rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]
-- 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
f : G →* N
H : Subgroup N
rw : (⇑f : (a : G) → N) '' (↑(comap f H) : Set G) = (↑(f.range ⊓ H) : Set N)
⊢ (↑(map f (comap f H)) : Set N) = (↑(f.range ⊓ H) : Set N)
have rw₁ : Set.image.{u_1, u_5} (α := G) (⇑f : (a : G) → N) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) = (↑(f.range ⊓ H) : Set N)
Tactic: rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]
-- 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
f : G →* N
H : Subgroup N
rw : (⇑f : (a : G) → N) '' (↑(comap f H) : Set G) = (↑(f.range ⊓ H) : Set N)
rw₁ : Set.image.{u_1, u_5} (α := G) (⇑f : (a : G) → N) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) = (↑(f.range ⊓ H) : Set N)
⊢ (↑(map f (comap f H)) : Set N) = (↑(f.range ⊓ H) : Set N)
have rw₂ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑(f.range ⊓ H) : Set N)
Tactic: rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]
-- 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
f : G →* N
H : Subgroup N
rw : (⇑f : (a : G) → N) '' (↑(comap f H) : Set G) = (↑(f.range ⊓ H) : Set N)
rw₁ : Set.image.{u_1, u_5} (α := G) (⇑f : (a : G) → N) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) = (↑(f.range ⊓ H) : Set N)
rw₂ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑(f.range ⊓ H) : Set N)
⊢ (↑(map f (comap f H)) : Set N) = (↑(f.range ⊓ H) : Set N)
have rw₃ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑f.range : Set N) ∩ (↑H : Set N)
Tactic: rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]
-- 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
f : G →* N
H : Subgroup N
rw : (⇑f : (a : G) → N) '' (↑(comap f H) : Set G) = (↑(f.range ⊓ H) : Set N)
rw₁ : Set.image.{u_1, u_5} (α := G) (⇑f : (a : G) → N) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) = (↑(f.range ⊓ H) : Set N)
rw₂ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑(f.range ⊓ H) : Set N)
rw₃ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑f.range : Set N) ∩ (↑H : Set N)
⊢ (↑(map f (comap f H)) : Set N) = (↑(f.range ⊓ H) : Set N)
have rw₄ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) =
  Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) ∩ (↑H : Set N)
Tactic: rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]
-- 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
f : G →* N
H : Subgroup N
rw : (⇑f : (a : G) → N) '' (↑(comap f H) : Set G) = (↑(f.range ⊓ H) : Set N)
rw₁ : Set.image.{u_1, u_5} (α := G) (⇑f : (a : G) → N) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) = (↑(f.range ⊓ H) : Set N)
rw₂ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑(f.range ⊓ H) : Set N)
rw₃ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑f.range : Set N) ∩ (↑H : Set N)
rw₄ :
  (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) =
    Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) ∩ (↑H : Set N)
⊢ (↑(map f (comap f H)) : Set N) = (↑(f.range ⊓ H) : Set N)
have rw₅ : Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) ∩ (↑H : Set N) =
  Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) ∩ (↑H : Set N)
Tactic: rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]
-- 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
f : G →* N
H : Subgroup G
⊢ comap f (map f H) = H ⊔ f.ker
have refine : comap f (map f H) ≤ H ⊔ f.ker
Tactic: refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (hypothesis)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ f.ker
have hx₁ : ∃ x_1 ∈ H, Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) x_1 : N) ((f : (a : G) → N) x : N)
Tactic: simp only [mem_map, mem_comap] at hx
Cleared hypotheses: hx
-- 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
f : G →* N
H : Subgroup G
x : G
hx : ∃ x_1 ∈ H, Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) x_1 : N) ((f : (a : G) → N) x : N)
⊢ x ∈ H ⊔ f.ker
have rcases : ∀ (y : G) (hy : y ∈ H) (hy' : Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) y : N) ((f : (a : G) → N) x : N)), x ∈ H ⊔ f.ker
Tactic: rcases hx with ⟨y, hy, hy'⟩
Cleared hypotheses: hx
-- 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
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) y : N) ((f : (a : G) → N) x : N)
⊢ x ∈ H ⊔ f.ker
have rw : y * (y⁻¹ * x) ∈ H ⊔ f.ker
Tactic: rw [← mul_inv_cancel_left y x]
-- 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
f : G →* N
H : Subgroup N
h : H ≤ f.range
⊢ map f (comap f H) = H
have rwa : f.range ⊓ H = H
Tactic: rwa [map_comap_eq, inf_eq_right]
-- 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
f : G →* N
H : Subgroup G
h : f.ker ≤ H
⊢ comap f (map f H) = H
have rwa : H ⊔ f.ker = H
Tactic: rwa [comap_map_eq, sup_eq_left]
-- 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
f : G →* N
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K ⊔ f.ker
have rw : H ≤ comap f (map f K) ↔ H ≤ K ⊔ f.ker
Tactic: rw [map_le_iff_le_comap, comap_map_eq]
-- 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
f : G →* N
H K : Subgroup G
rw : H ≤ comap f (map f K) ↔ H ≤ K ⊔ f.ker
⊢ map f H ≤ map f K ↔ H ≤ K ⊔ f.ker
have rw₁ : H ≤ K ⊔ f.ker ↔ H ≤ K ⊔ f.ker
Tactic: rw [map_le_iff_le_comap, comap_map_eq]
-- 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
f : G →* N
H : Subgroup G
⊢ map f H = f.range ↔ Codisjoint H f.ker
have rw : map f H = map f ⊤ ↔ Codisjoint H f.ker
Tactic: rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]
-- 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
f : G →* N
H : Subgroup G
rw : map f H = map f ⊤ ↔ Codisjoint H f.ker
⊢ map f H = f.range ↔ Codisjoint H f.ker
have rw₁ : H ⊔ f.ker = ⊤ ⊔ f.ker ↔ Codisjoint H f.ker
Tactic: rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]
-- 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
f : G →* N
H : Subgroup G
rw : map f H = map f ⊤ ↔ Codisjoint H f.ker
rw₁ : H ⊔ f.ker = ⊤ ⊔ f.ker ↔ Codisjoint H f.ker
⊢ map f H = f.range ↔ Codisjoint H f.ker
have rw₂ : H ⊔ f.ker = ⊤ ⊔ f.ker ↔ H ⊔ f.ker = ⊤
Tactic: rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]
-- 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
f : G →* N
H : Subgroup G
rw : map f H = map f ⊤ ↔ Codisjoint H f.ker
rw₁ : H ⊔ f.ker = ⊤ ⊔ f.ker ↔ Codisjoint H f.ker
rw₂ : H ⊔ f.ker = ⊤ ⊔ f.ker ↔ H ⊔ f.ker = ⊤
⊢ map f H = f.range ↔ Codisjoint H f.ker
have rw₃ : H ⊔ f.ker = ⊤ ↔ H ⊔ f.ker = ⊤
Tactic: rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]
-- 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
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K
have rw : H ≤ comap f (map f K) ↔ H ≤ K
Tactic: rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]
-- 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
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
rw : H ≤ comap f (map f K) ↔ H ≤ K
⊢ map f H ≤ map f K ↔ H ≤ K
have rw₁ : H ≤ K ↔ H ≤ K
Tactic: rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (hypothesis)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : map f H = map f K
⊢ H = K
have hf₁ : comap f (map f H) = comap f (map f K)
Tactic: apply_fun comap f at hf
Cleared hypotheses: hf
-- 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
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : comap f (map f H) = comap f (map f K)
⊢ H = K
have rwa : ∀ (hf : H ⊔ f.ker = comap f (map f K)), H = K
Tactic: rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf
Cleared hypotheses: hf
-- 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
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : comap f (map f H) = comap f (map f K)
rwa : ∀ (hf : H ⊔ f.ker = comap f (map f K)), H = K
⊢ H = K
have rwa₁ : ∀ (hf : H ⊔ f.ker = K ⊔ f.ker), H = K
Tactic: rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf
Cleared hypotheses: hf