-- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Iio 0) log

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
⊢ -x ≠ -y

Tactic:
contrapose! hxy

Result:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy : -x = -y
⊢ x = y

Proof state:
⊢ StrictConcaveOn ℝ (Iio 0) log

Tactic:
refine ⟨convex_Iio _, ?_⟩

Result:
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Iio 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Iio 0 → x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • log x + b • log y = a • log (-x) + b • log (-y)

Tactic:
simp_rw [log_neg_eq_log]

Result:
no goals

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ log (-(a • x + b • y)) = log (a • x + b • y)

Tactic:
rw [log_neg_eq_log]

Result:
no goals

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < -x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • log x + b • log y < log (a • x + b • y)

Tactic:
have hx' : 0 < -x := by linarith

Result:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
⊢ a • log x + b • log y < log (a • x + b • y)

Proof state:
case e_x
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • -x + b • -y = -(a • x + b • y)

Tactic:
simp only [Algebra.id.smul_eq_mul]

Result:
case e_x
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a * -x + b * -y = -(a * x + b * y)

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ log (a • -x + b • -y) = log (-(a • x + b • y))

Tactic:
congr 1

Result:
case e_x
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • -x + b • -y = -(a • x + b • y)

Proof state:
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Iio 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Iio 0 → x ≠ y → ∀ ⦃a b : ℝ⦄, 0 < a → 0 < b → a + b = 1 → a • log x + b • log y < log (a • x + b • y)

Tactic:
intro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab

Result:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • log x + b • log y < log (a • x + b • y)

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • log x + b • log y < log (a • x + b • y)

Tactic:
calc
  a • log x + b • log y = a • log (-x) + b • log (-y) := by simp_rw [log_neg_eq_log]
  _ < log (a • -x + b • -y) := strictConcaveOn_log_Ioi.2 hx' hy' hxy' ha hb hab
  _ = log (-(a • x + b • y)) := by congr 1; simp only [Algebra.id.smul_eq_mul]; ring
  _ = _ := by rw [log_neg_eq_log]

Result:
no goals

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
⊢ a • log x + b • log y < log (a • x + b • y)

Tactic:
have hy' : 0 < -y := by linarith

Result:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
⊢ a • log x + b • log y < log (a • x + b • y)

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy : -x = -y
⊢ x = y

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
⊢ 0 < -y

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
⊢ a • log x + b • log y < log (a • x + b • y)

Tactic:
have hxy' : -x ≠ -y := by contrapose! hxy; linarith

Result:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a • log x + b • log y < log (a • x + b • y)

Proof state:
case e_x
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx' : 0 < -x
hy' : 0 < -y
hxy' : -x ≠ -y
⊢ a * -x + b * -y = -(a * x + b * y)

Tactic:
ring

Result:
no goals