My first non-trivial proof in Lean Prover! ㊗️🎉

lim_inf_cons_mul_eq.0.lean

import tactic.norm_num
import data.real.basic
import analysis.normed_space.basic

open normed_field

def lim_inf (f : ℝ → ℝ) (L : ℝ) :=
  ∀ ε > 0, ∃ N > (0 : ℝ),
    ∀ x, x > N → ∥f x - L∥ < ε

theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ (C : ℝ), lim_inf (λ x, C * a x) (C * L) :=
begin
assume C : ℝ,
rw lim_inf at *, /- unfold definitions -/
assume (ε : ℝ) (Hε : ε > 0),
by_cases HC : C = 0, {
  fapply exists.intro, exact 1,
  fapply exists.intro, norm_num,
  assume (x : ℝ) (Hx : x > 1),
  rw HC, /- ∥0 * a x - 0 * L∥ < ε -/
  norm_num, /- 0 < ε -/
  exact Hε
}, {
  have HinvC : C⁻¹ ≠ 0, by exact inv_ne_zero HC,
  have HnC : ∥C⁻¹∥ > 0, by exact abs_pos_iff.mpr HinvC,
  have HnCε : ∥C⁻¹∥ * ε > 0, by exact mul_pos' HnC Hε,
  let HE := H (∥C⁻¹∥ * ε) HnCε,
  apply exists.elim HE,
  intros N H1,
  apply exists.elim H1,
  intros HN H2,
  apply exists.intro N,
  apply exists.intro HN,
  assume (x : ℝ) (Hx : x > N),
  let H3 := H2 x Hx,
  have E1: C * (a x - L) = C * a x - C * L, by exact mul_sub C (a x) L,
  rw ←E1,
  norm_num, simp at H3 ⊢,
  rw ←(mul_lt_mul_left HnC),
  rw ←mul_assoc,
  rw ←norm_mul,
  rw (inv_mul_cancel HC),
  simp,
  exact H3
}
end

lim_inf_cons_mul_eq.kennys_revision.lean

theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ (C : ℝ), lim_inf (λ x, C * a x) (C * L) :=
begin
  assume C : ℝ,
  unfold lim_inf at H ⊢, /- unfold definitions -/
  assume (ε : ℝ) (Hε : ε > 0),
  by_cases HC : C = 0,
  { use [1, by norm_num],
    assume (x : ℝ) (Hx : x > 1),
    rw HC, /- ∥0 * a x - 0 * L∥ < ε -/
    simpa using Hε },
  { have HinvC : C⁻¹ ≠ 0, from inv_ne_zero HC,
    have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero HinvC,
    have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε,
    specialize H (∥C⁻¹∥ * ε) HnCε,
    rcases H with ⟨N, HN, H⟩,
    use [N, HN],
    assume (x : ℝ) (Hx : x > N),
    specialize H x Hx,
    rw [← mul_sub, ← mul_lt_mul_left HnC, ← norm_mul, ← mul_assoc, inv_mul_cancel HC, one_mul],
    exact H }
end

lim_inf_cons_mul_eq.patrick_calc.lean

/- Revised by Patrick Massot -/
theorem lim_inf_cons_mul_eq_patrick_calc (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
  ∀ C, lim_inf (λ x, C * a x) (C * L) :=
begin
  intros C ε Hε,
  by_cases HC : C = 0,
  { use [1, by norm_num],
    intros,
    simpa [HC] using Hε },
  { have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero (inv_ne_zero HC),
    have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε,
    rcases H (∥C⁻¹∥ * ε) HnCε with ⟨N, HN, H⟩,
    use [N, HN],
    intros x Hx,
    calc  ∥ C * a x - C * L ∥
        = ∥ C * (a x - L) ∥ : by rw mul_sub
    ... = ∥ C ∥ * ∥a x - L ∥ : norm_mul _ _
    ... < ∥ C ∥ * (∥C⁻¹∥ * ε) : mul_lt_mul_of_pos_left (H x Hx) (abs_pos_of_ne_zero HC)
    ... = ε : by rw [← mul_assoc, ← norm_mul, mul_inv_cancel HC, norm_one, one_mul] }
end

lim_inf_cons_mul_eq.patricks_compression.lean

theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
  ∀ C, lim_inf (λ x, C * a x) (C * L) :=
begin
  intros C ε Hε,
  by_cases HC : C = 0,
  { use [1, by norm_num],
    intros,
    simpa [HC] using Hε },
  { have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero (inv_ne_zero HC),
    have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε,
    rcases H (∥C⁻¹∥ * ε) HnCε with ⟨N, HN, H⟩,
    use [N, HN],
    intros x Hx,
    rw [← mul_sub, ← mul_lt_mul_left HnC, ← norm_mul, ← mul_assoc, inv_mul_cancel HC, one_mul],
    exact H x Hx }
end

Forgot to state the theorem I was proving! Not everyone can read Lean yet. Written in maths the theorem is:

$$\lim_{n\to\infty} C \cdot a_n = C \cdot \lim_{n\to\infty} a_n \text{ for } C \in \mathbb{R}$$