Theorem: hom_preserve_one (src/Group.lean)

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
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

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
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

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]
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

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]
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

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)]
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

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
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

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]
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
⊢ φ has_one.one = φ has_one.one * φ has_one.one
Tactic:
rw [← hom.preserve_comp]
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)

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]
State after:
no goals