Theorem: hom_preserve_inv (src/Group.lean)

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

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

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

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

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

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

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

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

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

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

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