## Stream: new members

### Topic: Improve my proof about continuous functions

#### Martin C. Martin (Nov 22 2023 at 19:49):

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 (Nov 22 2023 at 19:52):

You could use the continuity tactic:

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


#### Kyle Miller (Nov 22 2023 at 19:52):

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 (Nov 22 2023 at 19:52):

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

#### Kyle Miller (Nov 22 2023 at 19:54):

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

#### Martin C. Martin (Nov 22 2023 at 19:55):

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

#### Kyle Miller (Nov 22 2023 at 19:56):

You just use by? instead of by

#### Kyle Miller (Nov 22 2023 at 19:57):

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 (Nov 22 2023 at 19:57):

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

#### Kyle Miller (Nov 22 2023 at 19:58):

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 (Nov 22 2023 at 20:03):

TIL about by?

#### Damiano Testa (Nov 22 2023 at 21:04):

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

#### Ruben Van de Velde (Nov 22 2023 at 21:05):

by sorry?

#### Mauricio Collares (Nov 23 2023 at 09:02):

I like sorry? as an alias for hint

#### Kevin Buzzard (Nov 23 2023 at 09:40):

Very easy for beginners to remember too

Last updated: Dec 20 2023 at 11:08 UTC