Theorem: Imo2019P1.additive_to_int_linear (Compfiles/Imo2019P1.lean)

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
⊢ ∃ c, ∀ (a : ℤ), f a = c * a
Tactic:
let g := AddMonoidHom.toIntLinearMap <| AddMonoidHom.mk' f h
State after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
⊢ ∃ c, ∀ (a : ℤ), f a = c * a

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
⊢ ∃ c, ∀ (a : ℤ), f a = c * a
Tactic:
refine ⟨f 1, fun a => ?_⟩
State after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
a : ℤ
⊢ f a = f 1 * a

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
a : ℤ
⊢ f a = f 1 * a
Tactic:
change g a = g 1 * a
State after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
a : ℤ
⊢ g a = g 1 * a

State before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x + y) = f x + f y
g : ℤ →ₗ[ℤ] ℤ := (AddMonoidHom.mk' f h).toIntLinearMap
a : ℤ
⊢ g a = g 1 * a
Tactic:
rw [mul_comm, ← smul_eq_mul, ← LinearMap.map_smul, smul_eq_mul, mul_one]
State after:
no goals