Matemáticas en Lean

-- ---------------------------------------------------------------------
-- Ejercicio. Calcular el valor de 2+3.
-- ---------------------------------------------------------------------

#eval 2 + 3

-- Comentario: Al poner el cursor sobre eval se escribe el resultado en el
-- minibuffer. 

-- ---------------------------------------------------------------------
-- Ejercicio: Calcular el tipo de la expresión 2+3.
-- ---------------------------------------------------------------------

#check 2 + 3

-- Comentario: Al colocar el cursor sobre check escribe en el minibuffer
--    2 + 3 : ℕ
-- que indica que el valor de la expresión es un número natural. 

-- ---------------------------------------------------------------------
-- Ejercicio 1. Definir la función f que le suma 3 a cada número natural.
-- ---------------------------------------------------------------------

def f (x : ℕ) := x + 3

-- ---------------------------------------------------------------------
-- Ejercicio 2. Calcular el tipo de f.
-- ---------------------------------------------------------------------

#check f

-- Comentario: Al colocar el cursor sobre check se obtiene
--    f : ℕ → ℕ

-- ---------------------------------------------------------------------
-- Ejercicio 3. Calcular el valor de f(2).
-- ---------------------------------------------------------------------

#eval f 2

-- Comentario: Al colocar el cursor sobre eval se obtiene
--    5

-- ---------------------------------------------------------------------
-- Ejercicio 1. Definir la proposión ultimo_teorema_de_Fermat que
-- expresa el último teorema de Fermat.
-- ---------------------------------------------------------------------

def ultimo_teorema_de_Fermat :=
  ∀ x y z n : ℕ, n > 2 → x * y * z ≠ 0 → x^n + y^n ≠ z^n

-- ---------------------------------------------------------------------
-- Ejercicio 2. Calcular el tipo de ultimo_teorema_de_Fermat
-- ---------------------------------------------------------------------

#check ultimo_teorema_de_Fermat

-- Comentario: Al colocar el cursor sobre check se obtiene
--    ultimo_teorema_de_Fermat : Prop

-- ---------------------------------------------------------------------
-- Ejercicio 1. Demostrar el teorema facil que afirma que 2 + 3 = 5.
-- ---------------------------------------------------------------------

theorem facil : 2 + 3 = 5 := rfl

-- Comentarios:
-- 1. Para activar la ventana de objetivos (*Lean Goal*) se escribe 
--    C-c C-g
-- 2. Se desactiva volviendo a escribir C-c C-g 
-- 3. La táctica rfl (ver https://bit.ly/2BYbiBH) comprueba que 2+3 y 5
--    son iguales por definición.

-- ---------------------------------------------------------------------
-- Ejercicio 2. Calcular el tipo de facil
-- ---------------------------------------------------------------------

#check facil

-- Comentario: Colocando el cursor sobre check se obtiene
--    facil : 2 + 3 = 5

-- ---------------------------------------------------------------------
-- Ejercicio 3. Enunciar el teorema dificil que afirma que se verifica
-- el último teorema de Fermat, omitiendo la demostración.
-- ---------------------------------------------------------------------

def ultimo_teorema_de_Fermat :=
  ∀ x y z n : ℕ, n > 2 → x * y * z ≠ 0 → x^n + y^n ≠ z^n

theorem dificil : ultimo_teorema_de_Fermat := sorry

-- Comentarios:
-- 1. La palabra sorry se usa para omitir la demostración.
-- 2. Se puede verificar la teoría pulsando 
--       C-x ! l 
--    Se obtiene
--       31   1 warning         declaration 'dificil' uses sorry

-- ---------------------------------------------------------------------
-- Ejercicio 3. Calcular el tipo de dificil.
-- ---------------------------------------------------------------------

#check dificil

-- Comentario: Colocando el cursor sobre check se obtiene
--    dificil : ultimo_teorema_de_Fermat

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que los procutos de los números naturales por
-- números pares son pares.
-- ---------------------------------------------------------------------

import data.nat.parity tactic

open nat

-- 1ª demostración
example : ∀ m n, even n → even (m * n) :=
  assume m n ⟨k, (hk : n = 2 * k)⟩,
  have hmn : m * n = 2 * (m * k),
    by rw [hk, mul_left_comm],
  show ∃ l, m * n = 2 * l,
    from ⟨_, hmn⟩

-- 2ª demostración (mediante término)
example : ∀ m n, even n → even (m * n) :=
  λ m n ⟨k, hk⟩, ⟨m * k, by rw [hk, mul_left_comm]⟩

-- 3ª demostración (mediante tácticas)
example : ∀ m n, even n → even (m * n) :=
  begin
    rintros m n ⟨k, hk⟩,
    use m * k,
    rw [hk, mul_left_comm]
  end

-- 4ª demostración (mediante tácticas en una línea)
example : ∀ m n, even n → even (m * n) :=
  by rintros m n ⟨k, hk⟩; use m * k; rw [hk, mul_left_comm]

-- 4ª demostración (automática)
example : ∀ m n, even n → even (m * n) :=
  by intros; simp * with parity_simps

-- Comentarios:
-- 1. Al poner el curso en la línea 1 sobre data.nat.parity y pulsar M-. 
--    se abre la teoría correspondiente.
-- 2. Se activa la ventana de objetivos (*Lean Goal*) pulsando C-c C-g
-- 3. Al mover el cursor sobre las pruebas se actualiza la ventana de
--    objetivos. 

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que los números reales tienen la siguente
-- propiedad 
--    (a * b) * c = b * (a * c)
-- ---------------------------------------------------------------------

import data.real.basic

-- 1ª demostración
-- ===============

example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
begin
  rw mul_comm a b,
  rw mul_assoc b a c,
end

-- Comentarios: 
-- 1. Al colocar el cursor sobre el nombre de un lema se ve su enunciado. 
-- 2. Para completar el nombre de un lema basta escribir parte de su
--    nombre y completar con S-SPC (es decir, simultáneamente las teclas
--    de mayúscula y la de espacio).
-- 3. los lemas usados son
--    + mul_com   : (∀ a b : G),   a * b = b * a
--    + mul_assoc : (∀ a b c : G), (a * b) * c = a * (b * c)
-- 4. La táctica (rw e) (ver https://bit.ly/3eUxbjD) reescribe una
--    expresión usando la ecuación e. 

-- El desarrollo de la prueba es:
-- 
--    inicio
--       a b c : ℝ
--       ⊢ (a * b) * c = b * (a * c)
--    rw mul_comm a b,
--       a b c : ℝ
--       ⊢ (a * b) * c = b * (a * c)   
--    rw mul_assoc b a c
--       no goals

-- 2ª demostración
-- ===============

example 
  (a b c : ℝ) 
  : (a * b) * c = b * (a * c) :=
calc
  (a * b) * c = (b * a) * c : by rw mul_comm a b
          ... = b * (a * c) : by rw mul_assoc b a c

-- Comentario: El entorno calc (ver https://bit.ly/2NRxiAU) permite
-- escribir demostraciones ecuacionales.

-- 3ª demostración
-- ===============

example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
by ring

-- Comentario: La táctica ring demuestra ecuaciones aplicando las
-- propiedades de anillos.

-- ---------------------------------------------------------------------
-- Ejercicio 1. Demostrar que los números reales tienen la siguente
-- propiedad 
--    (c * b) * a = b * (a * c)
-- ---------------------------------------------------------------------

-- Importación de librería
-- =======================

import data.real.basic

-- 1ª demostración
-- ===============

example 
  (a b c : ℝ) 
  : (c * b) * a = b * (a * c) :=
begin
  rw mul_comm c b,
  rw mul_assoc,
  rw mul_comm c a,
end

-- Desarrollo de la prueba:
-- -----------------------

--    a b c : ℝ
--    ⊢ (c * b) * a = b * (a * c)
-- rw mul_comm c b,
--    a b c : ℝ
--    ⊢ (b * c) * a = b * (a * c)
-- rw mul_assoc,
--    a b c : ℝ
--    ⊢ b * (c * a) = b * (a * c)
-- rw mul_comm c a,
--   no goals

-- 2ª demostración
-- ===============

example 
  (a b c : ℝ) 
  : (c * b) * a = b * (a * c) :=
calc
  (c * b) * a = (b * c) * a : by rw mul_comm c b
          ... = b * (c * a) : by rw mul_assoc
          ... = b * (a * c) : by rw mul_comm c a

-- 3ª demostración
-- ===============

example 
  (a b c : ℝ) 
  : (c * b) * a = b * (a * c) :=
by ring

-- ---------------------------------------------------------------------
-- Ejercicio 2. Demostrar que los números reales tienen la siguente
-- propiedad 
--    a * (b * c) = b * (a * c)
-- ---------------------------------------------------------------------

-- 1ª demostración
-- ===============

example 
  (a b c : ℝ) 
  : a * (b * c) = b * (a * c) :=
begin
  rw ←mul_assoc,
  rw mul_comm a b,
  rw mul_assoc,
end

-- Comentario. Con la táctica (rw ←e) se aplica reescritura sustituyendo
-- el término derecho de la igualdad e por el izquierdo.

-- Desarrollo de la prueba
-- -----------------------

--    a b c : ℝ
--    ⊢ a * (b * c) = b * (a * c)
-- rw ←mul_assoc,
--    a b c : ℝ
--    ⊢ (a * b) * c = b * (a * c)
-- rw mul_comm a b,
--    a b c : ℝ
--    ⊢ (b * a) * c = b * (a * c)
-- rw mul_assoc,
--    no goals

-- 2ª demostración
-- ===============

example 
  (a b c : ℝ) 
  : a * (b * c) = b * (a * c) :=
calc
  a * (b * c) = (a * b) * c : by rw ←mul_assoc
          ... = (b * a) * c : by rw mul_comm a b
          ... = b * (a * c) : by rw mul_assoc

-- 3ª demostración
-- ===============

example 
  (a b c : ℝ) 
  : a * (b * c) = b * (a * c) :=
by ring

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que si a, b, c, d, e y f son números reales
-- tales que 
--    a * b = c * d
--    e = f
-- Entonces,
--    a * (b * e) = c * (d * f)
-- ---------------------------------------------------------------------

import data.real.basic

-- 1ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h1 : a * b = c * d) 
  (h2 : e = f) 
  : a * (b * e) = c * (d * f) :=
begin
  rw h2,
  rw ←mul_assoc,
  rw h1,
  rw mul_assoc,
end

-- Comentario: La táctica (rw h2) reescribe el objetivo con la igualdad
-- de la nipótesis h2.

-- Desarrollo de la prueba
-- -----------------------

-- inicio
--    a b c d e f : ℝ,
--    h1 : a * b = c * d,
--    h2 : e = f
--    ⊢ a * (b * e) = c * (d * f)
-- rw h2,
--    S
--    ⊢ a * (b * f) = c * (d * f)
-- rw ←mul_assoc,
--    S
--    ⊢ (a * b) * f = c * (d * f)
-- rw h1,
--    S
--    ⊢ (c * d) * f = c * (d * f)
-- rw mul_assoc,
--    no goals
--
-- En el desarrollo anterior, S es el conjunto de las hipótesis; es
-- decir, 
--    S = {a b c d e f : ℝ,
--         h1 : a * b = c * d,
--         h2 : e = f}

-- 2ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h1 : a * b = c * d) 
  (h2 : e = f) 
  : a * (b * e) = c * (d * f) :=
calc
  a * (b * e) = a * (b * f) : by rw h2
          ... = (a * b) * f : by rw ←mul_assoc
          ... = (c * d) * f : by rw h1
          ... = c * (d * f) : by rw mul_assoc

-- 3ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h1 : a * b = c * d) 
  (h2 : e = f) 
  : a * (b * e) = c * (d * f) :=
by finish

-- Comentario: La táctica finish (ver https://bit.ly/3ionJHE) simplifica
-- el objetivo usando las hipótesis.

-- ---------------------------------------------------------------------
-- Ejercicio 1. Demostrar que si a, b, c, d, e y f son números reales
-- tales que 
--    b * c = e * f
-- entonces
--    ((a * b) * c) * d = ((a * e) * f) * d
-- ---------------------------------------------------------------------

import data.real.basic 

-- 1ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h : b * c = e * f) 
  : ((a * b) * c) * d = ((a * e) * f) * d :=
begin
  rw mul_assoc a,
  rw h,
  rw ←mul_assoc a,
end

-- El desarrollo de la prueba es
--
-- inicio
--    a b c d e f : ℝ,
--    h : b * c = e * f
--    ⊢ (a * (b * c)) * d = ((a * e) * f) * d
-- rw mul_assoc a,
--    S
--    ⊢ a * (b * c) * d = a * e * f * d
-- rw h,
--    S
--    ⊢ a * (e * f) * d = a * e * f * d
-- rw ←mul_assoc a,
--    no goals
--
-- En el desarrollo anterior, S es el conjunto de hipótesis; es decir,
--    S = {a b c d e f : ℝ,
--         h : b * c = e * f}

-- 2ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h : b * c = e * f) 
  : ((a * b) * c) * d = ((a * e) * f) * d :=
calc
  ((a * b) * c) * d = (a * (b * c)) * d : by rw mul_assoc a
                ... = (a * (e * f)) * d : by rw h
                ... = ((a * e) * f) * d : by rw ←mul_assoc a

-- 3ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h : b * c = e * f) 
  : ((a * b) * c) * d = ((a * e) * f) * d :=
by finish

-- ---------------------------------------------------------------------
-- Ejercicio 2. Demostrar que si a, b, c y d son números reales tales
-- que  
--    c = b * a - d 
--    d = a * b
-- entonces
--    c = 0
-- ---------------------------------------------------------------------

-- 1ª demostración
-- ===============

example 
  (a b c d : ℝ) 
  (h1 : c = b * a - d) 
  (h2 : d = a * b) 
  : c = 0 :=
begin
  rw h1,
  rw mul_comm,
  rw h2,
  rw sub_self,
end

-- Comentario: El último lema se puede encontrar escribiendo previamente
--    by library_search
-- y afirma que
--    ∀ (a : G), a - a = 0

-- Desarrollo de la prueba:
-- 
-- inicio
--    a b c d : ℝ,
--    h1 : c = b * a - d,
--    h2 : d = a * b
--    ⊢ c = 0
-- rw h1,
--    S
--    ⊢ b * a - d = 0
-- rw mul_comm,
--    S
--    ⊢ a * b - d = 0
-- rw h2,
--    S
--    ⊢ a * b - a * b = 0
-- rw sub_self,
--    no goals
--
-- En el desarrollo anterior, S es el conjunto de hipótesis; es decir,
--    S = {a b c d : ℝ,
--         h1 : c = b * a - d,
--         h2 : d = a * b}

-- 2ª demostración
-- ===============

example 
  (a b c d : ℝ) 
  (h1 : c = b * a - d) 
  (h2 : d = a * b) 
  : c = 0 :=
calc
  c   = b * a - d     : by rw h1
  ... = a * b - d     : by rw mul_comm
  ... = a * b - a * b : by rw h2
  ... = 0             : by rw sub_self

-- 3ª demostración
-- ===============

example 
  (a b c d : ℝ) 
  (h1 : c = b * a - d) 
  (h2 : d = a * b) 
  : c = 0 :=
by finish [mul_comm]

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que si a, b, c, d, e y f son números reales
-- tales que 
--    a * b = c * d
--    e = f
-- entonces
--    a * (b * e) = c * (d * f)
-- ---------------------------------------------------------------------

import data.real.basic

-- 1ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h1 : a * b = c * d) 
  (h2 : e = f) 
  : a * (b * e) = c * (d * f) :=
begin
  rw h2, 
  rw ←mul_assoc, 
  rw h1, 
  rw mul_assoc,
end

-- Desarrollo de la prueba
--
--    a b c d e f : ℝ,
--    h1 : a * b = c * d,
--    h2 : e = f
--    ⊢ a * (b * e) = c * (d * f)
-- rw h2, 
--    ⊢ a * (b * f) = c * (d * f)
-- rw ←mul_assoc, 
--    ⊢ (a * b) * f = c * (d * f)
-- rw h1, 
--    ⊢ (c * d) * f = c * (d * f)
-- rw mul_assoc,
--    no goals 

-- 2ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h1 : a * b = c * d) 
  (h2 : e = f) 
  : a * (b * e) = c * (d * f) :=
begin
  rw [h2, ←mul_assoc, h1, mul_assoc]
end

-- Comentario: Colocando el cursor en las comas se observa el progreso
-- en la ventana de objetivos.

-- 3ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h1 : a * b = c * d) 
  (h2 : e = f) 
  : a * (b * e) = c * (d * f) :=
by rw [h2, ←mul_assoc, h1, mul_assoc]

-- 4ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h1 : a * b = c * d) 
  (h2 : e = f) 
  : a * (b * e) = c * (d * f) :=
by finish

-- 5ª demostración
-- ===============

example 
  (a b c d e f : ℝ) 
  (h1 : a * b = c * d) 
  (h2 : e = f) 
  : a * (b * e) = c * (d * f) :=
calc
  a * (b * e) = a * (b * f) : by rw h2 
          ... = (a * b) * f : by rw ←mul_assoc
          ... = (c * d) * f : by rw h1
          ... = c * (d * f) : by rw mul_assoc

-- ---------------------------------------------------------------------
-- Ejercicio 1. Importar la librería básica de los números reales.
-- ---------------------------------------------------------------------

import data.real.basic

-- ---------------------------------------------------------------------
-- Ejercicio 2. Crear una sección.
-- ---------------------------------------------------------------------

section

-- ---------------------------------------------------------------------
-- Ejercicio 3. Declarar que a, b y c son variables sobre los números
-- reales. 
-- ---------------------------------------------------------------------

variables a b c : ℝ

-- ---------------------------------------------------------------------
-- Ejercicio 4. Calcular el tipo de a.
-- ---------------------------------------------------------------------

#check a

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    a : ℝ

-- ---------------------------------------------------------------------
-- Ejercicio 5. Calcular el tipo de a + b.
-- ---------------------------------------------------------------------

#check a + b

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    a + b : ℝ

-- ---------------------------------------------------------------------
-- Ejercicio 6. Comprobar que a es un número real.
-- ---------------------------------------------------------------------

#check (a : ℝ)

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    a : ℝ

-- ---------------------------------------------------------------------
-- Ejercicio 7. Calcular el tipo de 
--    mul_comm a b
-- ---------------------------------------------------------------------

#check mul_comm a b

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    mul_comm a b : a * b = b * a

-- ---------------------------------------------------------------------
-- Ejercicio 8. Comprobar que el tipo de 
--    mul_comm a b
-- es
--    a * b = b * a)
-- ---------------------------------------------------------------------

#check (mul_comm a b : a * b = b * a)

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    mul_comm a b : a * b = b * a

-- ---------------------------------------------------------------------
-- Ejercicio 9. Calcular el tipo de 
--    mul_assoc c a b
-- ---------------------------------------------------------------------

#check mul_assoc c a b

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    mul_assoc c a b : c * a * b = c * (a * b)

-- ---------------------------------------------------------------------
-- Ejercicio 10. Calcular el tipo de 
--    mul_comm a
-- ---------------------------------------------------------------------

#check mul_comm a

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    mul_comm a : ∀ (b : ℝ), a * b = b * a 

-- ---------------------------------------------------------------------
-- Ejercicio 11. Calcular el tipo de 
--    mul_comm
-- ---------------------------------------------------------------------

#check mul_comm

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    mul_comm : ∀ (a b : ?M_1), a * b = b * a

-- ---------------------------------------------------------------------
-- Ejercicio 12. Calcular el tipo de 
--    @mul_comm
-- ---------------------------------------------------------------------

#check @mul_comm

-- Comentario: Al colocar el cursor sobre check se obtiene 
--    mul_comm : ∀ {G : Type u_1} [_inst_1 : comm_semigroup G] (a b : G), 
--               a * b = b * a

end

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que si a y b son números reales, entonces
--    (a + b) * (a + b) = a * a + 2 * (a * b) + b * b
-- ---------------------------------------------------------------------

import data.real.basic

variables a b : ℝ

-- 1ª demostración
-- ===============

example : 
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
begin
  rw mul_add,
  rw add_mul, 
  rw add_mul,
  rw ← add_assoc,
  rw add_assoc (a * a),
  rw mul_comm b a, 
  rw ← two_mul,
end

-- El desarrollo de la prueba es
--
--    a b : ℝ
--    ⊢ (a + b) * (a + b) = a * a + 2 * (a * b) + b * b
-- rw mul_add,
--    ⊢ (a + b) * a + (a + b) * b = a * a + 2 * (a * b) + b * b
-- rw add_mul, 
--    ⊢ a * a + b * a + (a + b) * b = a * a + 2 * (a * b) + b * b
-- rw add_mul,
--    ⊢ a * a + b * a + (a * b + b * b) = a * a + 2 * (a * b) + b * b
-- rw ← add_assoc,
--    ⊢ a * a + b * a + a * b + b * b = a * a + 2 * (a * b) + b * b
-- rw add_assoc (a * a),
--    ⊢ a * a + (b * a + a * b) + b * b = a * a + 2 * (a * b) + b * b
-- rw mul_comm b a, 
--    ⊢ a * a + (a * b + a * b) + b * b = a * a + 2 * (a * b) + b * b
-- rw ← two_mul,
--    no goals

-- 2ª demostración
-- ===============

example : 
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
  (a + b) * (a + b) 
      = (a + b) * a + (a + b) * b       : by rw mul_add
  ... = a * a + b * a + (a + b) * b     : by rw add_mul 
  ... = a * a + b * a + (a * b + b * b) : by rw add_mul 
  ... = a * a + b * a + a * b + b * b   : by rw ← add_assoc
  ... = a * a + (b * a + a * b) + b * b : by rw add_assoc (a * a)
  ... = a * a + (a * b + a * b) + b * b : by rw mul_comm b a 
  ... = a * a + 2 * (a * b) + b * b   : by rw ← two_mul

-- 3ª demostración
-- ===============

example : 
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
begin
  rw [mul_add, add_mul, add_mul],
  rw [←add_assoc, add_assoc (a * a)],
  rw [mul_comm b a, ←two_mul],
end

-- El desarrollo de la prueba es
-- 
--    a b : ℝ
--    ⊢ a * a + (a * b + a * b) + b * b = a * a + 2 * (a * b) + b * b
-- rw [mul_add, add_mul, add_mul],
--    ⊢ a * a + b * a + (a * b + b * b) = a * a + 2 * (a * b) + b * b
-- rw [←add_assoc, add_assoc (a * a)],
--    ⊢ a * a + (b * a + a * b) + b * b = a * a + 2 * (a * b) + b * b
-- rw [mul_comm b a, ←two_mul]
--    no goals

-- 4ª demostración
-- ===============

example : 
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
  (a + b) * (a + b)
      = a * a + b * a + (a * b + b * b) : by rw [mul_add, add_mul, add_mul]
  ... = a * a + (b * a + a * b) + b * b : by rw [←add_assoc, add_assoc (a * a)]
  ... = a * a + 2 * (a * b) + b * b     : by rw [mul_comm b a, ←two_mul]

-- 4ª demostración
-- ===============

example : 
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by ring

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que si a, b, c y d son números reales, entonces
--    (a + b) * (c + d) = a * c + a * d + b * c + b * d
-- ---------------------------------------------------------------------

import data.real.basic

variables a b c d : ℝ

-- 1ª demostración
-- ===============

example 
  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
begin
   rw add_mul,
   rw mul_add,
   rw mul_add,
   rw ← add_assoc,
end

-- El desarrollo de la prueba es
--
--    a b c d : ℝ
--    ⊢ (a + b) * (c + d) = a * c + a * d + b * c + b * d
-- rw add_mul,
--    ⊢ a * (c + d) + b * (c + d) = a * c + a * d + b * c + b * d
-- rw mul_add,
--    ⊢ a * c + a * d + b * (c + d) = a * c + a * d + b * c + b * d
-- rw mul_add,
--    ⊢ a * c + a * d + (b * c + b * d) = a * c + a * d + b * c + b * d
-- rw ← add_assoc,
--    no goals

-- 2ª demostración
-- ===============

example 
  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
calc 
  (a + b) * (c + d) 
      = a * (c + d) + b * (c + d)       : by rw add_mul
  ... = a * c + a * d + b * (c + d)     : by rw mul_add
  ... = a * c + a * d + (b * c + b * d) : by rw mul_add
  ... = a * c + a * d + b * c + b * d   : by rw ←add_assoc

-- 3ª demostración 
-- ===============

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
by rw [add_mul, mul_add, mul_add, ←add_assoc]

-- 4ª demostración 
-- ===============

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
by ring

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que si a y b son números reales, entonces
--    (a + b) * (a - b) = a^2 - b^2 
-- ---------------------------------------------------------------------

import data.real.basic

variables a b c d : ℝ

-- 1ª demostración (por reescritura usando el lema anterior)
-- =========================================================

-- El lema anterior es
lemma aux : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
by ring

-- La demostración es
example : (a + b) * (a - b) = a^2 - b^2 :=
begin
  rw sub_eq_add_neg,
  rw aux,
  rw mul_neg_eq_neg_mul_symm,
  rw add_assoc (a * a),
  rw mul_comm b a,
  rw neg_add_self,
  rw add_zero,
  rw ← pow_two,
  rw mul_neg_eq_neg_mul_symm,
  rw ← pow_two,
  rw ← sub_eq_add_neg,
end

-- El desarrollo de la demostración es
--    ⊢ (a + b) * (a - b) = a ^ 2 - b ^ 2
-- rw sub_eq_add_neg,
--    ⊢ (a + b) * (a + -b) = a ^ 2 - b ^ 2
-- rw aux,
--    ⊢ a * a + a * -b + b * a + b * -b = a ^ 2 - b ^ 2
-- rw mul_neg_eq_neg_mul_symm,
--    ⊢ a * a + -(a * b) + b * a + b * -b = a ^ 2 - b ^ 2
-- rw add_assoc (a * a),
--    ⊢ a * a + (-(a * b) + b * a) + b * -b = a ^ 2 - b ^ 2
-- rw mul_comm b a,
--    ⊢ a * a + (-(a * b) + a * b) + b * -b = a ^ 2 - b ^ 2
-- rw neg_add_self,
--    ⊢ a * a + 0 + b * -b = a ^ 2 - b ^ 2
-- rw add_zero,
--    ⊢ a * a + b * -b = a ^ 2 - b ^ 2
-- rw ← pow_two,
--    ⊢ a ^ 2 + b * -b = a ^ 2 - b ^ 2
-- rw mul_neg_eq_neg_mul_symm,
--    ⊢ a ^ 2 + -(b * b) = a ^ 2 - b ^ 2
-- rw ← pow_two,
--    ⊢ a ^ 2 + -b ^ 2 = a ^ 2 - b ^ 2
-- rw ← sub_eq_add_neg,
--    no goals

-- 3ª demostración (por calc)
-- ==========================

example : (a + b) * (a - b) = a^2 - b^2 :=
calc
  (a + b) * (a - b)
      = a * (a - b) + b * (a - b)         : by rw add_mul
  ... = (a * a - a * b) + b * (a - b)     : by rw mul_sub
  ... = (a^2 - a * b) + b * (a - b)       : by rw ← pow_two
  ... = (a^2 - a * b) + (b * a - b * b)   : by rw mul_sub
  ... = (a^2 - a * b) + (b * a - b^2)     : by rw ← pow_two
  ... = (a^2 + -(a * b)) + (b * a - b^2)  : by exact rfl
  ... = a^2 + (-(a * b) + (b * a - b^2))  : by rw add_assoc
  ... = a^2 + (-(a * b) + (b * a + -b^2)) : by exact rfl
  ... = a^2 + ((-(a * b) + b * a) + -b^2) : by rw ← add_assoc 
                                               (-(a * b)) (b * a) (-b^2) 
  ... = a^2 + ((-(a * b) + a * b) + -b^2) : by rw mul_comm
  ... = a^2 + (0 + -b^2)                  : by rw neg_add_self (a * b)
  ... = (a^2 + 0) + -b^2                  : by rw ← add_assoc 
  ... = a^2 + -b^2                        : by rw add_zero
  ... = a^2 - b^2                         : by exact rfl

-- Comentario. Se han usado los siguientes lemas:
-- + pow_two a : a ^ 2 = a * a 
-- + mul_sub a b c : a * (b - c) = a * b - a * c 
-- + add_mul a b c : (a + b) * c = a * c + b * c 
-- + add_sub a b c : a + (b - c) = a + b - c
-- + sub_sub a b c : a - b - c = a - (b + c)
-- + add_zero a : a + 0 = a

-- 4ª demostración
-- ===============

example : (a + b) * (a - b) = a^2 - b^2 :=
by ring

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que si a, b, c y d son números reales tales que
--    c = d * a + b
--    b = a * d
-- entonces
--    c = 2 * a * d 
-- ---------------------------------------------------------------------

import data.real.basic

variables a b c d : ℝ

-- 1ª demostración
-- ===============

example 
  (h1 : c = d * a + b) 
  (h2 : b = a * d)
  : c = 2 * a * d :=
begin
  rw h2 at h1,
  clear h2,
  rw mul_comm d a at h1,
  rw ← two_mul (a*d) at h1,
  rewrite ← mul_assoc 2 a d at h1,
  exact h1,
end

-- Comentarios
-- 1. La táctica (rw e at h) rescribe la parte izquierda de la
--    ecuación e por la derecha en la hipótesis h.
-- 2. La táctica (exact p) tiene éxito si el tipo de p se unifica con el
--    objetivo. 
-- 3. La táctica (clear h) borra la hipótesis h.

-- El desarrollo de la prueba es
--    
--    a b c d : ℝ,
--    h1 : c = d * a + b,
--    h2 : b = a * d
--    ⊢ c = 2 * a * d
-- rw h2 at h1,
--    a b c d : ℝ,
--    h2 : b = a * d,
--    h1 : c = d * a + a * d
--    ⊢ c = 2 * a * d
-- clear h2,
--    a b c d : ℝ,
--    h1 : c = d * a + a * d
--    ⊢ c = 2 * a * d
-- rw mul_comm d a at h1,
--    a b c d : ℝ,
--    h1 : c = a * d + a * d
--    ⊢ c = 2 * a * d
-- rw ← two_mul (a*d) at h1,
--    a b c d : ℝ,
--    h1 : c = 2 * (a * d)
--    ⊢ c = 2 * a * d
-- rewrite ← mul_assoc 2 a d at h1,
--    a b c d : ℝ,
--    h1 : c = 2 * a * d
--    ⊢ c = 2 * a * d
-- exact h1
--    no goals

-- 2ª demostración
-- ===============

example 
  (h1 : c = d * a + b) 
  (h2 : b = a * d)
  : c = 2 * a * d :=
calc
  c = d * a + b       : by rw h1
  ... = d * a + a * d : by rw h2
  ... = a * d + a * d : by rw mul_comm d a
  ... = 2 * (a * d)   : by rw ← two_mul (a * d)
  ... = 2 * a * d     : by rw mul_assoc

-- 3ª demostración
-- ===============

example 
  (h1 : c = d * a + b) 
  (h2 : b = a * d)
  : c = 2 * a * d :=
by rw [h1, h2, mul_comm d a, ← two_mul (a * d), mul_assoc]

-- 4ª demostración
-- ===============

example 
  (h1 : c = d * a + b) 
  (h2 : b = a * d)
  : c = 2 * a * d :=
begin
  rw h1, 
  rw h2,
  ring,
end

-- El desarrollo de la prueba es
--    
--    a b c d : ℝ,
--    h1 : c = d * a + b,
--    h2 : b = a * d
--    ⊢ c = 2 * a * d
-- rw h1, 
--    ⊢ d * a + b = 2 * a * d
-- rw h2,
--    ⊢ d * a + a * d = 2 * a * d
-- ring,
--    no goals

-- 5ª demostración
-- ===============

example 
  (h1 : c = d * a + b) 
  (h2 : b = a * d)
  : c = 2 * a * d :=
begin
  rw [h1, h2],
  ring,
end

-- 6ª demostración
-- ===============

example 
  (h1 : c = d * a + b) 
  (h2 : b = a * d)
  : c = 2 * a * d :=
by rw [h1, h2]; ring

-- 7ª demostración
-- ===============

example 
  (h1 : c = d * a + b) 
  (h2 : b = a * d)
  : c = 2 * a * d :=
by finish * using [two_mul]

-- ---------------------------------------------------------------------
-- Ejercicio. Sean a, b, c y dnúmeros reales. Demostrar, con la táctica
-- ring, que 
--    (c * b) * a = b * (a * c) 
--    (a + b) * (a + b) = a * a + 2 * (a * b) + b * b
--    (a + b) * (a - b) = a^2 - b^2
-- Además, si
--    c = d * a + b
--    b = a * d
-- entonces
--    c = 2 * a * d
-- ---------------------------------------------------------------------

import data.real.basic

variables a b c d : ℝ

example : (c * b) * a = b * (a * c) :=
by ring

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by ring

example : (a + b) * (a - b) = a^2 - b^2 :=
by ring

example 
  (h1 : c = d * a + b) 
  (h2 : b = a * d) 
  : c = 2 * a * d :=
begin
  rw [h1, h2],
  ring
end

-- ---------------------------------------------------------------------
-- Ejercicio 1. Importar la teoría de los números reales. 
-- ----------------------------------------------------------------------

import data.real.basic

-- ---------------------------------------------------------------------
-- Ejercicio 2. Declarar a, b y c como variables sobre los reales. 
-- ----------------------------------------------------------------------

variables a b c : ℝ

-- ---------------------------------------------------------------------
-- Ejercicio 3. Declarar que
-- + h  es una variable de tipo a ≤ b 
-- + h' es una variable de tipo b ≤ c 
-- ----------------------------------------------------------------------

variables (h : a ≤ b) (h' : b ≤ c)

-- ---------------------------------------------------------------------
-- Ejercicio 4. Calcular el tipo de las siguientes expresiones:
--    + le_refl
--    + le_refl a
--    + le_trans
--    + le_trans h
--    + le_trans h h'
-- ----------------------------------------------------------------------

#check (le_refl : ∀ a : real, a ≤ a)
#check (le_refl a : a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (le_trans h : b ≤ c → a ≤ c)
#check (le_trans h h' : a ≤ c)

-- ---------------------------------------------------------------------
-- Ejercicio 1. Realizar las siguientes acciones:
--    1. Importar la teoría de los números reales
--    2. Declarar x, y y z como variables sobre R. 
-- ----------------------------------------------------------------------

import data.real.basic

variables (x y z : ℝ)

-- ---------------------------------------------------------------------
-- Ejercicio 2. Demostrar que si
--    x ≤ y
--    y ≤ z
-- entonces 
--    x ≤ z 
-- ----------------------------------------------------------------------

-- 1ª demostración
-- ===============

example 
  (h1 : x ≤ y) 
  (h2 : y ≤ z) 
  : x ≤ z :=
begin
  apply le_trans,
  { apply h1, },
  apply h2,
end

-- El desarrollo de la prueba es
--
--    x y z : ℝ,
--    h1 : x ≤ y,
--    h2 : y ≤ z
--    ⊢ x ≤ z
-- apply le_trans,
--    ⊢ x ≤ ?m_1
-- { apply h1 },
--    ⊢ y ≤ z
-- apply h2,
--    no goals

-- 2ª demostración
-- ===============

example 
  (h1 : x ≤ y) 
  (h2 : y ≤ z) 
  : x ≤ z :=
begin
  apply le_trans h1,
  apply h2,
end

-- El desarrollo de la prueba es
--
--    x y z : ℝ,
--    h1 : x ≤ y,
--    h2 : y ≤ z
--    ⊢ x ≤ z
-- apply le_trans h1,
--    ⊢ y ≤ z
-- apply h2,
--    no goals

-- 3ª demostración
-- ===============

example 
  (h1 : x ≤ y) 
  (h2 : y ≤ z) 
  : x ≤ z :=
by exact le_trans h1 h2

-- 4ª demostración
-- ===============

example 
  (h1 : x ≤ y) 
  (h2 : y ≤ z) 
  : x ≤ z :=
le_trans h1 h2

-- ---------------------------------------------------------------------
-- Ejercicio 4. Demostrar que
--    x ≤ x
-- ----------------------------------------------------------------------

-- 1ª demostración
example : x ≤ x :=
by apply le_refl

-- 2ª demostración
example : x ≤ x :=
by exact le_refl x

-- 3ª demostración
example (x : ℝ) : x ≤ x :=
le_refl x

-- ---------------------------------------------------------------------
-- Ejercicio 1. Realizar las siguientes acciones:
--    1. Importar la teoría de los números reales
--    2. Declarar a, b y c como variables sobre R. 
-- ----------------------------------------------------------------------

import data.real.basic

variables a b c : ℝ

-- ---------------------------------------------------------------------
-- Ejercicio 2. Calcular el tipo de las siguientes expresiones:
--    + le_refl
--    + le_trans
--    + lt_of_le_of_lt
--    + lt_of_lt_of_le
--    + lt_trans
-- ----------------------------------------------------------------------


#check (le_refl  : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)

-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que si a, b, c, d y e son números reales tales
-- que 
--    a ≤ b
--    b < c
--    c ≤ d
--    d < e
-- entonces
--    a < e 
-- ----------------------------------------------------------------------


import data.real.basic

variables a b c d e : ℝ

-- 1ª demostración
-- ===============

example 
  (h₀ : a ≤ b) 
  (h₁ : b < c) 
  (h₂ : c ≤ d)
  (h₃ : d < e) :
  a < e :=
begin
  apply lt_of_le_of_lt h₀,
  apply lt_trans h₁, 
  apply lt_of_le_of_lt h₂,
  exact h₃,
end

-- El desarrollo de la prueba es
--
--    a b c d e : ℝ,
--    h₀ : a ≤ b,
--    h₁ : b < c,
--    h₂ : c ≤ d,
--    h₃ : d < e
--    ⊢ a < e
-- apply lt_of_le_of_lt h₀,
--    ⊢ b < e
-- apply lt_trans h₁,
--    ⊢ c < e 
-- apply lt_of_le_of_lt h₂,
--    ⊢ d < e
-- exact h₃,
--    no goals

-- 2ª demostración
-- ===============

example 
  (h₀ : a ≤ b) 
  (h₁ : b < c) 
  (h₂ : c ≤ d)
  (h₃ : d < e) :
  a < e :=
calc
  a ≤ b   : h₀
  ... < c : h₁
  ... ≤ d : h₂
  ... < e : h₃

-- 3ª demostración
-- ===============

example 
  (h₀ : a ≤ b) 
  (h₁ : b < c) 
  (h₂ : c ≤ d)
  (h₃ : d < e) :
  a < e :=
by finish

-- ---------------------------------------------------------------------
-- Ejercicio 1. Sean a, b, c, d y e números reales. Demostrar que si
--    a ≤ b 
--    b < c 
--    c ≤ d
--    d < e
-- entonces
--    a < e
-- ----------------------------------------------------------------------

import data.real.basic

variables a b c d e : ℝ

example
  (h₀ : a ≤ b) 
  (h₁ : b < c) 
  (h₂ : c ≤ d)
  (h₃ : d < e)
  : a < e :=
by linarith

-- ---------------------------------------------------------------------
-- Ejercicio 2. Demostrar que si
--    2 * a ≤ 3 * b
--    1 ≤ a
--    d = 2 
-- entonces
--    d + a ≤ 5 * b
-- ----------------------------------------------------------------------

example 
  (h   : 2 * a ≤ 3 * b) 
  (h'  : 1 ≤ a) 
  (h'' : d = 2) 
  : d + a ≤ 5 * b :=
by linarith

-- ---------------------------------------------------------------------
-- Ejercicio. Sean a, b, y c números reales. Demostrar  que si
--    1 ≤ a 
--    b ≤ c
-- entonces
--    2 + a + exp b ≤ 3 * a + exp c
-- ----------------------------------------------------------------------


import analysis.special_functions.exp_log

open real

variables a b c : ℝ

example 
  (h  : 1 ≤ a) 
  (h' : b ≤ c) 
  : 2 + a + exp b ≤ 3 * a + exp c :=
by linarith [exp_le_exp.mpr h']

-- ---------------------------------------------------------------------
-- Ejercicio. Calcular el tipo de los siguientes lemas
--    exp_le_exp 
--    exp_lt_exp 
--    log_le_log 
--    log_lt_log 
--    add_le_add 
--    add_lt_add_of_le_of_lt 
--    add_nonneg 
--    add_pos 
--    add_pos_of_pos_of_nonneg 
--    exp_pos 
-- ----------------------------------------------------------------------

import analysis.special_functions.exp_log

open real

variables  a b c d : ℝ

#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (exp_lt_exp : exp a < exp b ↔ a < b)
#check (log_le_log : 0 < a → 0 < b → (log a ≤ log b ↔ a ≤ b))
#check (log_lt_log : 0 < a → a < b → log a < log b)
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d)
#check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b)
#check (add_pos : 0 < a → 0 < b → 0 < a + b)
#check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)

-- ---------------------------------------------------------------------
-- Ejercicio 1. Realizar las siguientes acciones
--    1. Importar la teoría de exponeciales y logaritmos.
--    2. Abrir la teoría de los reales
--    3. Declarar a y b como variables sobre los reales.
-- ----------------------------------------------------------------------

import analysis.special_functions.exp_log   -- 1
open real                                   -- 2
variables (a b : ℝ)                         -- 3

-- ---------------------------------------------------------------------
-- Ejercicio 2. Calcular el tipo del lema exp_le_exp
-- ----------------------------------------------------------------------

#check @exp_le_exp a b

-- Comentario: Al colocar el cursor sobre check se obtiene
--    exp_le_exp : a.exp ≤ b.exp ↔ a ≤ b

-- ---------------------------------------------------------------------
-- Ejercicio 3. Demostrar que si
--    a ≤ b 
--    exp a ≤ exp b 
-- ----------------------------------------------------------------------

-- 1ª demostración
example  
  (h : a ≤ b) 
  : exp a ≤ exp b :=
begin
  rw exp_le_exp,
  exact h
end

-- 2ª demostración
example  
  (h : a ≤ b) 
  : exp a ≤ exp b :=
exp_le_exp.mpr h

-- Nota: Con mpr se indica en modus pones inverso. Por ejemplo, si
-- h: A ↔ B, entonces h.mpr es B → A y h.mp es A → B

-- ---------------------------------------------------------------------
-- Ejercicio 1. Realizar las siguientes acciones
--    1. Importar la teoría de exponeciales y logaritmos.
--    2. Abrir la teoría de los reales
--    3. Declarar a, b, c, d y e como variables sobre los reales.
-- ----------------------------------------------------------------------

import analysis.special_functions.exp_log   -- 1
open real                                   -- 2
variables a b c d e : ℝ                     -- 3 

-- ---------------------------------------------------------------------
-- Ejercicio 2. Calcular el tipo de los siguientes lemas 
--    add_lt_add_of_le_of_lt
--    exp_lt_exp 
--    le_refl 
-- ----------------------------------------------------------------------

#check @add_lt_add_of_le_of_lt ℝ _ a b c d 
#check @exp_lt_exp a b
#check le_refl 

-- Comentario: Colocando el cursor sobre check se obtiene
--    add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d 
--    exp_lt_exp : a.exp < b.exp ↔ a < b 
--    le_refl : ∀ (a : ?M_1), a ≤ a  

-- ---------------------------------------------------------------------
-- Ejercicio 3. Demostrar que si
--    a ≤ b 
--    c < d
-- entonces
--    a + exp c + e < b + exp d + e :=
-- ----------------------------------------------------------------------

example 
  (h₀ : a ≤ b) 
  (h₁ : c < d) 
  : a + exp c + e < b + exp d + e :=
begin
  apply add_lt_add_of_lt_of_le,
  { apply add_lt_add_of_le_of_lt h₀,
    apply exp_lt_exp.mpr h₁, },
  apply le_refl
end

-- El desarrollo de la prueba es
-- 
--    a b c d e : ℝ,
--    h₀ : a ≤ b,
--    h₁ : c < d
--    ⊢ a + c.exp + e < b + d.exp + e
-- apply add_lt_add_of_lt_of_le,
-- | { apply add_lt_add_of_le_of_lt h₀,
-- |      ⊢ a + c.exp < b + d.exp
-- |   apply exp_lt_exp.mpr h₁ },
--    ⊢ e ≤ e 
-- apply le_refl
--    no_goals

-- ---------------------------------------------------------------------
-- Ejercicio 1. Realizar las siguientes acciones
--    1. Importar la teoría de exponeciales y logaritmos.
--    2. Abrir la teoría de los reales
--    3. Declarar a, b, c, d y e como variables sobre los reales.
-- ----------------------------------------------------------------------

import analysis.special_functions.exp_log   -- 1
open real                                   -- 2
variables a b c d e : ℝ                     -- 3 

-- ---------------------------------------------------------------------
-- Ejercicio 2. Demostrar que si
--    d ≤ e
-- entonces
--    c + exp (a + d) ≤ c + exp (a + e)
-- ----------------------------------------------------------------------

example 
  (h₀ : d ≤ e) 
  : c + exp (a + d) ≤ c + exp (a + e) :=
begin
  apply add_le_add,
   apply le_refl,
  apply exp_le_exp.mpr,
  apply add_le_add,
   apply le_refl,
  exact h₀,
end

-- El desarrollo de la prueba es
--
--    a c d e : ℝ,
--    h₀ : d ≤ e
--    ⊢ c + (a + d).exp ≤ c + (a + e).exp
-- apply add_le_add,
-- |   ⊢ c ≤ c
-- | apply le_refl,
--    ⊢ (a + d).exp ≤ (a + e).exp
-- apply exp_le_exp.mpr,
--    ⊢ a + d ≤ a + e
-- apply add_le_add,
-- |    ⊢ a ≤ a
-- | apply le_refl,
--    ⊢ d ≤ e
-- exact h₀,
--    no goals

-- ---------------------------------------------------------------------
-- Ejercicio 3. Demostrar que
--    0 < 1
-- ----------------------------------------------------------------------

example : (0 : ℝ) < 1 :=
by norm_num

-- Nota: La táctica norm_num normaliza expresiones numéricas. Ver 
-- https://bit.ly/3hoJMgQ

-- ---------------------------------------------------------------------
-- Ejercicio 4. Demostrar que si
--    a ≤ b
-- entonces 
--    log (1 + exp a) ≤ log (1 + exp b) :=
-- ----------------------------------------------------------------------

example 
  (h : a ≤ b) 
  : log (1 + exp a) ≤ log (1 + exp b) :=
begin
  have h₀ : 0 < 1 + exp a,
  { apply add_pos,
    norm_num,
    apply exp_pos, },
  have h₁ : 0 < 1 + exp b,
  { apply add_pos,
    norm_num,
    apply exp_pos },
  apply (log_le_log h₀ h₁).mpr,
  apply add_le_add,
   apply le_refl,
  apply exp_le_exp.mpr h,
end

-- El desarrollo de la prueba es
--
--    a b : ℝ,
--    h : a ≤ b
--    ⊢ (1 + a.exp).log ≤ (1 + b.exp).log
-- have h₀ : 0 < 1 + exp a,
-- |    ⊢ 0 < 1 + a.exp
-- | apply add_pos,
-- |    ⊢ 0 < 1
-- | norm_num,
-- |    ⊢ 0 < a.exp
-- | apply exp_pos },
--    a b : ℝ,
--    h : a ≤ b,
--    h₀ : 0 < 1 + a.exp
--    ⊢ (1 + a.exp).log ≤ (1 + b.exp).log
-- have h₁ : 0 < 1 + exp b,
--    ⊢ 0 < 1 + b.exp
-- | apply add_pos,
-- |    ⊢ 0 < 1
-- | norm_num,
-- |    0 < b.exp
-- | apply exp_pos },
--    a b : ℝ,
--    h : a ≤ b,
--    h₀ : 0 < 1 + a.exp,
--    h₁ : 0 < 1 + b.exp
--    ⊢ (1 + a.exp).log ≤ (1 + b.exp).log
-- apply (log_le_log h₀ h₁).mpr,
--    ⊢ 1 + a.exp ≤ 1 + b.exp
-- apply add_le_add,
-- |    ⊢ 1 ≤ 1
-- | apply le_refl,
--    ⊢ a.exp ≤ b.exp
-- apply exp_le_exp.mpr h,
--    no goals

-- Comentario. Los lemas empleados son
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (le_refl : ∀ (a : real), a ≤ a)
#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (add_pos : 0 < a → 0 < b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)
#check (log_le_log : 0 < a → 0 < b → (log a ≤ log b ↔ a ≤ b))

-- ---------------------------------------------------------------------
-- Ejercicio . Demostrar que, para todo númeo real a, 
--    0 ≤ a^2
-- ----------------------------------------------------------------------

import data.real.basic
import tactic

example (a : ℝ) : 0 ≤ a^2 :=
begin
  -- library_search,
  exact pow_two_nonneg a,
end

-- Notas:
-- + Nota 1: Al colocar el cursor sobre library_search (después de descomentar 
--   la línea) escribe el mensaje
--      Try this: exact pow_two_nonneg a
-- + Nota 2: Para usar library_search hay que importar tactic.

-- ---------------------------------------------------------------------
-- Ejercicio. Sean a, b y c números reales. Demostrar que si
--    a ≤ b
-- entonces
--    c - exp b ≤ c - exp a :=
-- ----------------------------------------------------------------------

import import analysis.special_functions.exp_log
import tactic

open real

variables a b c : ℝ

-- 1ª demostración
-- ===============

example 
  (h : a ≤ b) 
  : c - exp b ≤ c - exp a :=
begin
   apply add_le_add,
   apply le_refl,
   apply neg_le_neg,
   apply exp_le_exp.mpr h,
end

-- El desarrollo de la prueba es
-- 
--    a b c : ℝ,
--    h : a ≤ b
--    ⊢ c - b.exp ≤ c - a.exp
-- apply add_le_add,
-- |    ⊢ c ≤ c
-- | apply le_refl,
--    ⊢ -b.exp ≤ -a.exp
-- apply neg_le_neg,
--    ⊢ a.exp ≤ b.exp
-- apply exp_le_exp.mpr h,
--    no goals

-- 2ª demostración
-- ===============

example 
  (h : a ≤ b) 
  : c - exp b ≤ c - exp a :=
-- by library_search [exp_le_exp.mpr h] 
by exact sub_le_sub_left (exp_le_exp.mpr h) c

-- 3ª demostración
-- ===============

example 
  (h : a ≤ b) 
  : c - exp b ≤ c - exp a :=
by linarith [exp_le_exp.mpr h]

-- Los lemas usados son:
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (le_refl : ∀ (a : real), a ≤ a)
#check (neg_le_neg : a ≤ b → -b ≤ -a)

-- ---------------------------------------------------------------------
-- Ejercicio. Sean a y b números reales. Demostrar que
--    2*a*b ≤ a^2 + b^2
-- ----------------------------------------------------------------------

import data.real.basic 
import tactic

variables a b : ℝ

-- 1ª demostración
example : 2*a*b ≤ a^2 + b^2 :=
begin
  have h : 0 ≤ a^2 - 2*a*b + b^2,
  calc
    a^2 - 2*a*b + b^2 = (a - b)^2       : by ring
                  ... ≥ 0               : by apply pow_two_nonneg,
  calc
    2*a*b = 2*a*b + 0                   : by ring
      ... ≤ 2*a*b + (a^2 - 2*a*b + b^2) : add_le_add (le_refl _) h
      ... = a^2 + b^2                   : by ring
end

-- 2ª demostración
example : 2*a*b ≤ a^2 + b^2 :=
begin
  have : 0 ≤ a^2 - 2*a*b + b^2,
  calc
    a^2 - 2*a*b + b^2 = (a - b)^2 : by ring
    ... ≥ 0                       : by apply pow_two_nonneg,
  linarith,
end

-- ---------------------------------------------------------------------
-- Ejercicio. Sean a y b números reales. Demostrar que
--    abs (a*b) ≤ (a^2 + b^2) / 2 :=
-- ----------------------------------------------------------------------

import data.real.basic 

variables a b : ℝ

example : abs (a*b) ≤ (a^2 + b^2) / 2 :=
begin
  apply abs_le_of_le_of_neg_le,
  { have h1 : 0 ≤ a^2 - 2*a*b + b^2,
      calc 0 ≤ (a-b)^2                : by exact pow_two_nonneg (a - b)
         ... = a^2-2*a*b+b^2          : by ring,
    have h2 : 2*(a*b) ≤ a^2 + b^2,
      calc 2*(a*b) 
           ≤ 2*(a*b)+(a^2-2*a*b+b^2)  : by exact le_add_of_nonneg_right h1
       ... = a^2 + b^2                : by ring,
    by linarith [h2] },
  { have h3 : 0 ≤ a^2 + 2*a*b + b^2,
      calc 0 ≤ (a+b)^2                : by exact pow_two_nonneg (a + b)
         ... = a^2+2*a*b+b^2          : by ring,
    have h4 : -2*(a*b) ≤ a^2 + b^2,
      calc -2*(a*b) 
           ≤ -2*(a*b)+(a^2+2*a*b+b^2) : by exact le_add_of_nonneg_right h3
       ... = a^2 + b^2                : by ring,
    by linarith [h4] },
end