shortening ContinuousOn Proof

Stream: new members

[Sabbir Rahman]

Consider the following proof

import Mathlib

open Real Set

example : ContinuousOn (fun (x : ℝ) ↦ x - log (x + 10)) (Ici 10) := by
  apply ContinuousOn.sub
  . exact continuousOn_id' (Ici 10)
  . have : (fun (x : ℝ) ↦ log (x + 10)) = (fun (x : ℝ) ↦ log x) ∘ (fun (x : ℝ) ↦ x + 10) := by
      ext x;
      simp
    rw [this]
    apply ContinuousOn.comp (t := {0}ᶜ)
    . exact continuousOn_log
    . apply Continuous.continuousOn
      exact continuous_add_right 10
    . simp [MapsTo]
      rintro x h
      linarith

it's a valid proof for the continuity of log(x + 10) on [0, inf) (which I needed for a bigger problem) but is there any way to shorted or automate the proof? since facts like these are generally dismissed in one line when writing informal proof, I was trying to learn if there are tactics that can help in these cases

[Etienne Marion]

import Mathlib

open Real Set

example : ContinuousOn (fun (x : ℝ) ↦ x - log (x + 10)) (Ici 10) :=
  continuousOn_id.sub <| (continuous_add_right 10).continuousOn.log fun x hx ↦ by linarith [mem_Ici.1 hx]

I don't know about automation because you need to check some non-zeroness because of the log which can't be handled by fun_prop, but here is a shorter proof.

[Vlad Tsyrklevich]

continuity is very good, but unfortunately doesn't work for ContinuousOn. You can make your life a little easier by a change of variable

lemma aux : ContinuousOn (fun (x : ℝ) ↦ (x - 10) - log x) (Ici 20) :=
  Continuous.continuousOn (by continuity) |>.sub continuousOn_log |>.mono (by simp)

[Sabbir Rahman]

thanks for both of your help, indeed the proofs are shorter. I see two tactics fun_prop and continuity, but their purpose seems a bit overlapped. when should I use which? also it feels like if continuousOn_logwas tagged with fun_prop or continuity, it'd be better (though this is my simple guess and I am not aware how those tactics work)

[Ruben Van de Velde]

fun_prop is newer and more general and probably faster, but sometimes continuity solves goals that fun_prop can't (which is probably a bug)

[Sabbir Rahman]

I see, unfortunately both of the tactics have minmal help text in #help tactic where can I get a better guide to how they work?

[Etienne Marion]

The main problem is that continuity and fun_prop are finishing tactics, which means that they cannot apply some results and then leave you with side conditions to prove, that's why I think you can't fully automate the proof.

[Vlad Tsyrklevich]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/FunProp.html

[Vlad Tsyrklevich]

Reading that page, I guess there's a way to do it using fun_prop like so:

lemma aux {y} (h : y ≠ 0) : ContinuousAt (fun (x : ℝ) ↦ (x - 10) - log x) y := by
  fun_prop (disch := assumption)
lemma aux2 : ContinuousOn (fun (x : ℝ) ↦ (x - 10) - log x) (Ici 20) :=
  continuousOn_of_forall_continuousAt (fun x hx => aux (by simp at hx; linarith))

simp + linarith is probably overkill, I'm just being lazy

[Sabbir Rahman]

hmm, discharge seems useful, in fact by creating a lemma, original problem can be done even quicker

example : ContinuousOn (fun (x : ℝ) ↦ x - log (x + 10)) (Ici 10) := by
  have (x : ℝ) (h : x ∈ Ici 10) : x + 10 ≠ 0 := by simp at *; linarith
  fun_prop (disch := assumption)