Improve my proof about continuous functions

Stream: new members

[Martin C. Martin]

Here's a proof that a constant times a continuous function is also continuous. I would have thought there was already a proof of this in mathlib, but I couldn't find it. Also, the proof seems a little long, any thoughts on simplifying it?

import Mathlib.Topology.Basic
import Mathlib.Topology.Algebra.Monoid
import Mathlib.Data.Set.Intervals.Basic

import Mathlib.Data.Real.Basic
import Mathlib.Topology.Instances.Real

example (f : ℝ → ℝ) (hf : Continuous f) (c : ℝ): Continuous (fun x => c * (f x)) := by
  have : (fun x => c * (f x)) = (fun x => ((fun _ => c) x) * (f x)) := by simp
  rw [this]
  have hconst : Continuous (fun (_ : ℝ) => c) := continuous_const
  apply hconst.mul hf

[Kyle Miller]

You could use the continuity tactic:

example (f : ℝ → ℝ) (hf : Continuous f) (c : ℝ): Continuous (fun x => c * (f x)) := by
  continuity

[Kyle Miller]

If you use by? you can see what it came up with, for curiosity's sake:

example (f : ℝ → ℝ) (hf : Continuous f) (c : ℝ): Continuous (fun x => c * (f x)) :=
  Continuous.comp' (continuous_mul_left c) (of_eq_true (eq_true hf))

[Martin C. Martin]

wow that's shorter lol! Is there a way to get a "trace" of what theorems it uses?

[Kyle Miller]

I think you sent that question about the trace right when I sent that last message -- does that answer your question?

[Martin C. Martin]

Yes you're right. :) What is by? and how do I use it? Just using := by by? or := by? gives syntax error.

[Kyle Miller]

You just use by? instead of by

[Kyle Miller]

import Mathlib.Topology.Basic
import Mathlib.Topology.Algebra.Monoid
import Mathlib.Data.Set.Intervals.Basic

import Mathlib.Data.Real.Basic
import Mathlib.Topology.Instances.Real

example (f : ℝ → ℝ) (hf : Continuous f) (c : ℝ): Continuous (fun x => c * (f x)) := by?
  continuity

[Kyle Miller]

Alternatively, you should be able to put show_term before either the tactic or before the by

[Kyle Miller]

This isn't a trace per se, but it does show you what proof term it came up with, and you can read off the lemmas from there.

[Ruben Van de Velde]

TIL about by?

[Damiano Testa]

I'm going to start putting question marks everywhere in Lean code from today on.

[Ruben Van de Velde]

by sorry?

[Mauricio Collares]

I like sorry? as an alias for hint

[Kevin Buzzard]

Very easy for beginners to remember too