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

My deepest appreciations go to Johan Commelin, Scott Morrison, and Floris van Doorn for helping me out on the Lean Prover Zulip.

I also thank Paul's Online Notes for the definition of lim_inf.

Practical tips I learned along the way:

• Be on Lean Prover Zulip!
• Once there, use the big search bar at the top to look for related questions
• Ask! They are super friendly!
• No parentheses needed for function application
• begin to start the proof, end to finish the proof (this is the more helpful "tactic mode")
• Don't forget the , after each step!
• rw name_of_definition at h ⊢, to expand the definition
• Use intros to automatically do universal instantiation. assume is the manual and clearer version.
• Use have when going forward (deducing) from the hypotheses; use rw when going back from the goal
• When using have, try by library_search when lost!
• When using rw, try Cmd-P or Ctrl-P to search for useful equalities!
  • Keywords: eq add mul lt norm neg ...
• let attaches temporary names to long stuff just like in Haskell or JavaScript
• When doing algebra, try norm_num and simp!
• If they fail, use rw with algebra theorems to do transformation

Regarding VS Code:

• Use the jroesch.lean plugin!
• On mac, I cannot copy from the "Lean Messages" view. Use Cmd-Shift-P > "Copy Contents to Comment" command!

Future:

• Learn about how to improve this
• Learn about calc mode

Deep thank you to Kenny Lau and Patrick Massot for their critique on the code!

Two things I forgot:

• *.intro is used to start a proof of * e.g. and.intro
• *.elim is used to get the inner content of (peel off) * e.g. exists.elim

More learned:

• unfold is specifically for unfolding definitions
• simpa [rules] using h is rw [rules] then simp then exact h; without h it tries every assumption
• use is a better exists.intro; use it to supply the positive cases all at once
• specialize is a special tool for peeling off ∀s
• rcases is a better exists.elim; use it to get the Prop we know already exist
• rcases H with ⟨W, H⟩ then use [W] is a great combo to use one ∃ to prove another

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