internlm/Lean-Github huggingface dataset:
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof state after:
no goals
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof state after:
no goals
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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)
Theorem: trivial_kernel_equiv_inj
Proof 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]
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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]
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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]
Proof state after:
no goals
Theorem: trivial_kernel_equiv_inj
Proof 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]
Proof 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 }
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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]
Proof state after:
no goals
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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)
Theorem: trivial_kernel_equiv_inj
Proof 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]
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof state after:
no goals
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof state after:
no goals
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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