--- Título: En ℝ, si a ≤ b y c < d, entonces a + eᶜ + f ≤ b + eᵈ + f. Autor: José A. Alonso --- Demostrar con Lean4 que \(a\), \(b\), \(c\), \(d\) y \(f\) son números reales tales que \(a \leq b\) y \(c < d\), entonces \[a + e^c + f \leq b + e^d + f\] Para ello, completar la siguiente teoría de Lean4: 
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
variable (a b c d f : ℝ)

example
  (h1 : a ≤ b)
  (h2 : c < d)
  : a + exp c + f < b + exp d + f :=
by sorry
[mathjax] Demostraciones en lenguaje natural (LN) 1ª demostración en LN Aplicando a la hipótesis 3 (\(c < d\)) la monotonía de la exponencial, se tiene \[e^c < e^d\] que, junto a la hipótesis 1 (\(a \leq b\)) y la monotonía de la suma da \[a + e^c < b + e^d\] y, de nuevo por la monotonía de la suma, se tiene \[a + e^c + f < b + e^d + f\] 2ª demostración en LN Tenemos que demostrar que \[(a + e^c) + f < (b + e^d) + f\] que, por la monotonía de la suma, se reduce a las siguientes dos desigualdades: \begin{align} &a + e^c < b + e^d \tag{1} \\ &f \leq f \tag{2} \end{align} La (1), de nuevo por la monotonía de la suma, se reduce a las siguientes dos: \begin{align} &a \leq b \tag{1.1} \\ &e^c < e^d \tag{1.2} \end{align}
La (1.1) se tiene por la hipótesis 1.
La (1.2) se tiene aplicando la monotonía de la exponencial a la hipótesis 2. La (2) se tiene por la propiedad reflexiva. Demostraciones con Lean4 
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Real
variable (a b c d f : ℝ)

-- 1ª demostración
example
  (h1 : a ≤ b)
  (h2 : c < d)
  : a + exp c + f < b + exp d + f :=
by
  have h3 : exp c < exp d :=
    exp_lt_exp.mpr h2
  have h4 : a + exp c < b + exp d :=
    add_lt_add_of_le_of_lt h1 h3
  show a + exp c + f < b + exp d + f
  exact add_lt_add_right h4 f

-- 2ª demostración
example
  (h1 : a ≤ b)
  (h2 : c < d)
  : a + exp c + f < b + exp d + f :=
by
  apply add_lt_add_of_lt_of_le
  { apply add_lt_add_of_le_of_lt
    { exact h1 }
    { apply exp_lt_exp.mpr
      exact h2 } }
  { apply le_refl }

-- 3ª demostración
example
  (h1 : a ≤ b)
  (h2 : c < d)
  : a + exp c + f < b + exp d + f :=
by
  apply add_lt_add_of_lt_of_le
  . apply add_lt_add_of_le_of_lt h1
    apply exp_lt_exp.mpr h2
  rfl
Demostraciones interactivas Se puede interactuar con las demostraciones anteriores en Lean 4 Web. Referencias