internlm/Lean-Github huggingface dataset:
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : { mem := fun x s => Set.isMember x }.1 b H
⊢ a * b ∈ H
Tactic:
simp at hb
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : Set.isMember b
⊢ a * b ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : Set.isMember b
⊢ a * b ∈ H
Tactic:
rw [Set.isMember, trivial_subgroup] at hb
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : { isMember := fun x => x = has_one.one }.1 b
⊢ a * b ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : { isMember := fun x => x = has_one.one }.1 b
⊢ a * b ∈ H
Tactic:
simp at hb
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ a * b ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ a * b ∈ H
Tactic:
rw [ha, hb]
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one * has_one.one ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one * has_one.one ∈ H
Tactic:
rw [G.mul_one]
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ H
Tactic:
simp
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ trivial_subgroup G
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ has_one.one ∈ trivial_subgroup G
Tactic:
rw [trivial_subgroup, Membership.mem, instMembershipSet]
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun x => x = has_one.one }
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
a b : α
ha : a = has_one.one
hb : b = has_one.one
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one { isMember := fun x => x = has_one.one }
Tactic:
simp
Proof state after:
no goals
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
⊢ has_one.one ∈ H
Tactic:
rw [Membership.mem, instMembershipSet]
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
⊢ { mem := fun x s => Set.isMember x }.1 has_one.one H
Tactic:
simp
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
⊢ Set.isMember has_one.one
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
⊢ Set.isMember has_one.one
Tactic:
rw [Set.isMember, trivial_subgroup]
Proof state after:
no goals
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
⊢ ∀ (a : α), a ∈ H → group.inv a ∈ H
Tactic:
intros a ha
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a ∈ H
⊢ group.inv a ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a ∈ H
⊢ group.inv a ∈ H
Tactic:
rw [Membership.mem, instMembershipSet] at ha
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : { mem := fun x s => Set.isMember x }.1 a H
⊢ group.inv a ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : { mem := fun x s => Set.isMember x }.1 a H
⊢ group.inv a ∈ H
Tactic:
simp at ha
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : Set.isMember a
⊢ group.inv a ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : Set.isMember a
⊢ group.inv a ∈ H
Tactic:
rw [Set.isMember, trivial_subgroup] at ha
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : { isMember := fun x => x = has_one.one }.1 a
⊢ group.inv a ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : { isMember := fun x => x = has_one.one }.1 a
⊢ group.inv a ∈ H
Tactic:
simp at ha
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a = has_one.one
⊢ group.inv a ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a = has_one.one
⊢ group.inv a ∈ H
Tactic:
rw [ha]
Proof state after:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a = has_one.one
⊢ group.inv has_one.one ∈ H
Theorem: triv_is_subgroup
Proof state before:
α : Type u_1
G : group α
H : Set α := trivial_subgroup G
hH : H = trivial_subgroup G
hmul_mem : ∀ (a b : α), a ∈ H → b ∈ H → a * b ∈ H
hone_mem : has_one.one ∈ H
a : α
ha : a = has_one.one
⊢ group.inv has_one.one ∈ H
Tactic:
apply inv_one_eq_one
Proof state after:
no goals
Theorem: mult_left
Proof state before:
α : Type u_1
G : group α
a b c : α
⊢ b = c → a * b = a * c
Tactic:
intro h
Proof state after:
α : Type u_1
G : group α
a b c : α
h : b = c
⊢ a * b = a * c
Theorem: mult_left
Proof state before:
α : Type u_1
G : group α
a b c : α
h : b = c
⊢ a * b = a * c
Tactic:
rw [h]
Proof state after:
no goals
Theorem: mult_right
Proof state before:
α : Type u_1
G : group α
a b c : α
⊢ b = c → b * a = c * a
Tactic:
intro h
Proof state after:
α : Type u_1
G : group α
a b c : α
h : b = c
⊢ b * a = c * a
Theorem: mult_right
Proof state before:
α : Type u_1
G : group α
a b c : α
h : b = c
⊢ b * a = c * a
Tactic:
rw [h]
Proof state after:
no goals
Theorem: cancel_left
Proof state before:
α : Type u_1
G : group α
a b c : α
⊢ a * b = a * c → b = c
Tactic:
intro h
Proof state after:
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
⊢ b = c
Theorem: cancel_left
Proof state before:
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
⊢ b = c
Tactic:
have h' := mult_left G (G.inv a) (a * b) (a * c) h
Proof state after:
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
h' : group.inv a * (a * b) = group.inv a * (a * c)
⊢ b = c
Theorem: cancel_left
Proof state before:
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
h' : group.inv a * (a * b) = group.inv a * (a * c)
⊢ b = c
Tactic:
rw [←G.mul_assoc, ←G.mul_assoc, G.mul_left_inv, G.one_mul, G.one_mul] at h'
Proof state after:
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
h' : b = c
⊢ b = c
Theorem: cancel_left
Proof state before:
α : Type u_1
G : group α
a b c : α
h : a * b = a * c
h' : b = c
⊢ b = c
Tactic:
exact h'
Proof state after:
no goals
Theorem: cancel_right
Proof state before:
α : Type u_1
G : group α
a b c : α
⊢ b * a = c * a → b = c
Tactic:
intro h
Proof state after:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
⊢ b = c
Theorem: cancel_right
Proof state before:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
⊢ b = c
Tactic:
have h' := mult_right G (G.inv a) (b * a) (c * a) h
Proof state after:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b * a * group.inv a = c * a * group.inv a
⊢ b = c
Theorem: cancel_right
Proof state before:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b * a * group.inv a = c * a * group.inv a
⊢ b = c
Tactic:
rw [G.mul_assoc, G.mul_assoc, mul_right_inv, G.mul_one, G.mul_one] at h'
Proof state after:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b = c
⊢ b = c
Theorem: cancel_right
Proof state before:
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b = c
⊢ b = c
Tactic:
exact h'
Proof state after:
no goals
Theorem: hom_preserve_one
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
⊢ group_homomorphism.fn G H has_one.one = has_one.one
Tactic:
let φ := hom.fn
Proof state after:
α : 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 has_one.one = has_one.one
Theorem: hom_preserve_one
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 has_one.one = has_one.one
Tactic:
have hphi : φ = hom.fn := by 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
⊢ group_homomorphism.fn G H has_one.one = has_one.one
Theorem: hom_preserve_one
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
⊢ group_homomorphism.fn G H has_one.one = has_one.one
Tactic:
rw [← hphi]
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
⊢ φ has_one.one = has_one.one
Theorem: hom_preserve_one
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
⊢ φ has_one.one = has_one.one
Tactic:
have hg : φ (G.one) = (φ G.one) * (φ G.one) := by
  rw [← hom.preserve_comp]
  conv =>
    left
    right
    rw [← G.mul_one G.one]
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
hg : φ has_one.one = φ has_one.one * φ has_one.one
⊢ φ has_one.one = has_one.one
Theorem: hom_preserve_one
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
hg : φ has_one.one = φ has_one.one * φ has_one.one
⊢ φ has_one.one = has_one.one
Tactic:
conv at hg =>
  left
  rw [← H.mul_one (φ G.one)]
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
hg : φ has_one.one * has_one.one = φ has_one.one * φ has_one.one
⊢ φ has_one.one = has_one.one
Theorem: hom_preserve_one
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
hg : φ has_one.one * has_one.one = φ has_one.one * φ has_one.one
⊢ φ has_one.one = has_one.one
Tactic:
have hh := (cancel_left H (φ G.one) _ _) hg
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
hg : φ has_one.one * has_one.one = φ has_one.one * φ has_one.one
hh : has_one.one = φ has_one.one
⊢ φ has_one.one = has_one.one
Theorem: hom_preserve_one
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
hg : φ has_one.one * has_one.one = φ has_one.one * φ has_one.one
hh : has_one.one = φ has_one.one
⊢ φ has_one.one = has_one.one
Tactic:
rw [hh]
Proof state after:
no goals
Theorem: hom_preserve_one
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: hom_preserve_one
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
⊢ φ has_one.one = φ has_one.one * φ has_one.one
Tactic:
rw [← hom.preserve_comp]
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
⊢ φ has_one.one = group_homomorphism.fn G H (has_one.one * has_one.one)
Theorem: hom_preserve_one
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
⊢ φ has_one.one = group_homomorphism.fn G H (has_one.one * has_one.one)
Tactic:
conv =>
  left
  right
  rw [← G.mul_one G.one]
Proof state after:
no goals
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
⊢ ∀ (g : α), group_homomorphism.fn G H (group.inv g) = group.inv (group_homomorphism.fn G H g)
Tactic:
intro g
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
⊢ group_homomorphism.fn G H (group.inv g) = group.inv (group_homomorphism.fn G H g)
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
⊢ group_homomorphism.fn G H (group.inv g) = group.inv (group_homomorphism.fn G H g)
Tactic:
let φ := hom.fn
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
⊢ group_homomorphism.fn G H (group.inv g) = group.inv (group_homomorphism.fn G H g)
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
⊢ group_homomorphism.fn G H (group.inv g) = group.inv (group_homomorphism.fn G H g)
Tactic:
have hphi : φ = hom.fn := by simp
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ group_homomorphism.fn G H (group.inv g) = group.inv (group_homomorphism.fn G H g)
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ group_homomorphism.fn G H (group.inv g) = group.inv (group_homomorphism.fn G H g)
Tactic:
rw [← hphi]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g) = group.inv (φ g)
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g) = group.inv (φ g)
Tactic:
apply (cancel_right H (φ g) _ _)
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g) * φ g = group.inv (φ g) * φ g
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g) * φ g = group.inv (φ g) * φ g
Tactic:
rw [H.mul_left_inv]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g) * φ g = has_one.one
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g) * φ g = has_one.one
Tactic:
rw [← hom.preserve_comp (G.inv g) g]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ group_homomorphism.fn G H (group.inv g * g) = has_one.one
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ group_homomorphism.fn G H (group.inv g * g) = has_one.one
Tactic:
rw [← hphi]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g * g) = has_one.one
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ (group.inv g * g) = has_one.one
Tactic:
rw [G.mul_left_inv]
Proof state after:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ has_one.one = has_one.one
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ φ has_one.one = has_one.one
Tactic:
apply hom_preserve_one
Proof state after:
no goals
Theorem: hom_preserve_inv
Proof state before:
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
g : α
φ : α → β := 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), set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)
Tactic:
intros hom
Proof 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)
Theorem: trivial_kernel_equiv_inj
Proof 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
Proof 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)
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
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)
Tactic:
have hphi : φ = hom.fn := by 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
⊢ 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
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)
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
⊢ 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)
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:
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]
Proof state after:
no goals