Theorem: trivial_kernel_equiv_inj (src/Group.lean)

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
⊢ ∀ (hom : group_homomorphism G H), set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)
Tactic:
intros hom
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)
Tactic:
let φ := hom.fn
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)
Tactic:
have hphi : φ = hom.fn := by simp
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) → injective (group_homomorphism.fn G H)

case mpr
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ injective (group_homomorphism.fn G H) → set_eq (kernel G H hom) (trivial_subgroup G)

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) → injective (group_homomorphism.fn G H)
Tactic:
case mp =>
  intro h
  rw [injective]
  intros x y hinj
  rw [← hphi] at hinj
  have hh := mult_left H (H.inv (φ x)) _ _ hinj
  rw [H.mul_left_inv] at hh
  rw [←hom_preserve_inv] at hh
  rw [←hphi] at hh
  rw [←hom.preserve_comp] at hh
  have hker : (G.inv x * y) ∈ kernel G H hom := by
    rw [kernel, Membership.mem, instMembershipSet]
    simp
    rw [hh]
  have hsp := (h (G.inv x * y)).mp hker
  rw [trivial_subgroup, Membership.mem, instMembershipSet] at hsp
  simp at hsp
  have hmul := mult_left G x (group.inv x * y) G.one hsp
  rw [←G.mul_assoc] at hmul
  rw [mul_right_inv, G.one_mul, G.mul_one] at hmul
  rw [hmul]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ injective (group_homomorphism.fn G H) → set_eq (kernel G H hom) (trivial_subgroup G)
Tactic:
case mpr =>
  intro h
  rw [set_eq]
  intro x
  apply Iff.intro
  case mp =>
    intro hker
    rw [kernel, Membership.mem, instMembershipSet] at hker
    simp at hker
    rw [←hphi] at hker
    rw [injective] at h
    have hinj := h G.one x
    rw [←hphi] at hinj
    rw [hphi, hom_preserve_one G H hom, ←hphi] at hinj
    have hl := hinj hker.symm
    rw [←hl]
    rw [Membership.mem, instMembershipSet]
    simp
    have hts : subgroup G (trivial_subgroup G) := triv_is_subgroup
    apply hts.one_mem
  case mpr =>
    intro hone
    rw [trivial_subgroup, Membership.mem, instMembershipSet] at hone
    simp at hone
    rw [hone]
    rw [kernel, Membership.mem, instMembershipSet]
    simp
    apply hom_preserve_one
State after:
no goals

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
⊢ φ = group_homomorphism.fn G H
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) → injective (group_homomorphism.fn G H)
Tactic:
intro h
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
⊢ injective (group_homomorphism.fn G H)

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
⊢ injective (group_homomorphism.fn G H)
Tactic:
rw [injective]
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
⊢ ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
⊢ ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
Tactic:
intros x y hinj
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : group_homomorphism.fn G H x = group_homomorphism.fn G H y
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : group_homomorphism.fn G H x = group_homomorphism.fn G H y
⊢ x = y
Tactic:
rw [← hphi] at hinj
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
⊢ x = y
Tactic:
have hh := mult_left H (H.inv (φ x)) _ _ hinj
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : group.inv (φ x) * φ x = group.inv (φ x) * φ y
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : group.inv (φ x) * φ x = group.inv (φ x) * φ y
⊢ x = y
Tactic:
rw [H.mul_left_inv] at hh
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group.inv (φ x) * φ y
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group.inv (φ x) * φ y
⊢ x = y
Tactic:
rw [←hom_preserve_inv] at hh
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x) * φ y
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x) * φ y
⊢ x = y
Tactic:
rw [←hphi] at hh
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = φ (group.inv x) * φ y
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = φ (group.inv x) * φ y
⊢ x = y
Tactic:
rw [←hom.preserve_comp] at hh
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ x = y
Tactic:
have hker : (G.inv x * y) ∈ kernel G H hom := by
  rw [kernel, Membership.mem, instMembershipSet]
  simp
  rw [hh]
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
⊢ x = y
Tactic:
have hsp := (h (G.inv x * y)).mp hker
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y ∈ trivial_subgroup G
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y ∈ trivial_subgroup G
⊢ x = y
Tactic:
rw [trivial_subgroup, Membership.mem, instMembershipSet] at hsp
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : { mem := fun x s => Set.isMember x }.1 (group.inv x * y) { isMember := fun x => x = has_one.one }
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : { mem := fun x s => Set.isMember x }.1 (group.inv x * y) { isMember := fun x => x = has_one.one }
⊢ x = y
Tactic:
simp at hsp
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y = has_one.one
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y = has_one.one
⊢ x = y
Tactic:
have hmul := mult_left G x (group.inv x * y) G.one hsp
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y = has_one.one
hmul : x * (group.inv x * y) = x * has_one.one
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y = has_one.one
hmul : x * (group.inv x * y) = x * has_one.one
⊢ x = y
Tactic:
rw [←G.mul_assoc] at hmul
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y = has_one.one
hmul : x * group.inv x * y = x * has_one.one
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y = has_one.one
hmul : x * group.inv x * y = x * has_one.one
⊢ x = y
Tactic:
rw [mul_right_inv, G.one_mul, G.mul_one] at hmul
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y = has_one.one
hmul : y = x
⊢ x = y

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
hker : group.inv x * y ∈ kernel G H hom
hsp : group.inv x * y = has_one.one
hmul : y = x
⊢ x = y
Tactic:
rw [hmul]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ group.inv x * y ∈ kernel G H hom
Tactic:
rw [kernel, Membership.mem, instMembershipSet]
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ { mem := fun x s => Set.isMember x }.1 (group.inv x * y)
    { isMember := fun g => group_homomorphism.fn G H g = has_one.one }

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ { mem := fun x s => Set.isMember x }.1 (group.inv x * y)
    { isMember := fun g => group_homomorphism.fn G H g = has_one.one }
Tactic:
simp
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ group_homomorphism.fn G H (group.inv x * y) = has_one.one

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : set_eq (kernel G H hom) (trivial_subgroup G)
x y : α
hinj : φ x = φ y
hh : has_one.one = group_homomorphism.fn G H (group.inv x * y)
⊢ group_homomorphism.fn G H (group.inv x * y) = has_one.one
Tactic:
rw [hh]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ injective (group_homomorphism.fn G H) → set_eq (kernel G H hom) (trivial_subgroup G)
Tactic:
intro h
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
⊢ set_eq (kernel G H hom) (trivial_subgroup G)

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
⊢ set_eq (kernel G H hom) (trivial_subgroup G)
Tactic:
rw [set_eq]
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
⊢ ∀ (x : α), x ∈ kernel G H hom ↔ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
⊢ ∀ (x : α), x ∈ kernel G H hom ↔ x ∈ trivial_subgroup G
Tactic:
intro x
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ kernel G H hom ↔ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ kernel G H hom ↔ x ∈ trivial_subgroup G
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ kernel G H hom → x ∈ trivial_subgroup G

case mpr
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ trivial_subgroup G → x ∈ kernel G H hom

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ kernel G H hom → x ∈ trivial_subgroup G
Tactic:
case mp =>
  intro hker
  rw [kernel, Membership.mem, instMembershipSet] at hker
  simp at hker
  rw [←hphi] at hker
  rw [injective] at h
  have hinj := h G.one x
  rw [←hphi] at hinj
  rw [hphi, hom_preserve_one G H hom, ←hphi] at hinj
  have hl := hinj hker.symm
  rw [←hl]
  rw [Membership.mem, instMembershipSet]
  simp
  have hts : subgroup G (trivial_subgroup G) := triv_is_subgroup
  apply hts.one_mem
State after:
no goals

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ trivial_subgroup G → x ∈ kernel G H hom
Tactic:
case mpr =>
  intro hone
  rw [trivial_subgroup, Membership.mem, instMembershipSet] at hone
  simp at hone
  rw [hone]
  rw [kernel, Membership.mem, instMembershipSet]
  simp
  apply hom_preserve_one
State after:
no goals

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ kernel G H hom → x ∈ trivial_subgroup G
Tactic:
intro hker
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : x ∈ kernel G H hom
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : x ∈ kernel G H hom
⊢ x ∈ trivial_subgroup G
Tactic:
rw [kernel, Membership.mem, instMembershipSet] at hker
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : { mem := fun x s => Set.isMember x }.1 x { isMember := fun g => group_homomorphism.fn G H g = has_one.one }
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : { mem := fun x s => Set.isMember x }.1 x { isMember := fun g => group_homomorphism.fn G H g = has_one.one }
⊢ x ∈ trivial_subgroup G
Tactic:
simp at hker
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : group_homomorphism.fn G H x = has_one.one
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : group_homomorphism.fn G H x = has_one.one
⊢ x ∈ trivial_subgroup G
Tactic:
rw [←hphi] at hker
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : φ x = has_one.one
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hker : φ x = has_one.one
⊢ x ∈ trivial_subgroup G
Tactic:
rw [injective] at h
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
⊢ x ∈ trivial_subgroup G
Tactic:
have hinj := h G.one x
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : group_homomorphism.fn G H has_one.one = group_homomorphism.fn G H x → has_one.one = x
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : group_homomorphism.fn G H has_one.one = group_homomorphism.fn G H x → has_one.one = x
⊢ x ∈ trivial_subgroup G
Tactic:
rw [←hphi] at hinj
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : φ has_one.one = φ x → has_one.one = x
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : φ has_one.one = φ x → has_one.one = x
⊢ x ∈ trivial_subgroup G
Tactic:
rw [hphi, hom_preserve_one G H hom, ←hphi] at hinj
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
⊢ x ∈ trivial_subgroup G
Tactic:
have hl := hinj hker.symm
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ x ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ x ∈ trivial_subgroup G
Tactic:
rw [←hl]
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ has_one.one ∈ trivial_subgroup G

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ has_one.one ∈ trivial_subgroup G
Tactic:
rw [Membership.mem, instMembershipSet]
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one (trivial_subgroup G)

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one (trivial_subgroup G)
Tactic:
simp
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ Set.isMember has_one.one

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
⊢ Set.isMember has_one.one
Tactic:
have hts : subgroup G (trivial_subgroup G) := triv_is_subgroup
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
hts : subgroup G (trivial_subgroup G)
⊢ Set.isMember has_one.one

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : ∀ (x y : α), group_homomorphism.fn G H x = group_homomorphism.fn G H y → x = y
x : α
hker : φ x = has_one.one
hinj : has_one.one = φ x → has_one.one = x
hl : has_one.one = x
hts : subgroup G (trivial_subgroup G)
⊢ Set.isMember has_one.one
Tactic:
apply hts.one_mem
State after:
no goals

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
⊢ x ∈ trivial_subgroup G → x ∈ kernel G H hom
Tactic:
intro hone
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x ∈ trivial_subgroup G
⊢ x ∈ kernel G H hom

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x ∈ trivial_subgroup G
⊢ x ∈ kernel G H hom
Tactic:
rw [trivial_subgroup, Membership.mem, instMembershipSet] at hone
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : { mem := fun x s => Set.isMember x }.1 x { isMember := fun x => x = has_one.one }
⊢ x ∈ kernel G H hom

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : { mem := fun x s => Set.isMember x }.1 x { isMember := fun x => x = has_one.one }
⊢ x ∈ kernel G H hom
Tactic:
simp at hone
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ x ∈ kernel G H hom

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ x ∈ kernel G H hom
Tactic:
rw [hone]
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ has_one.one ∈ kernel G H hom

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ has_one.one ∈ kernel G H hom
Tactic:
rw [kernel, Membership.mem, instMembershipSet]
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun g => group_homomorphism.fn G H g = has_one.one }

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun g => group_homomorphism.fn G H g = has_one.one }
Tactic:
simp
State after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ group_homomorphism.fn G H has_one.one = has_one.one

State before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
h : injective (group_homomorphism.fn G H)
x : α
hone : x = has_one.one
⊢ group_homomorphism.fn G H has_one.one = has_one.one
Tactic:
apply hom_preserve_one
State after:
no goals