awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
linarith :
  HSub.hSub (α := ℝ) (↑q : ℝ) 1 = 0 →
    HSub.hSub (α := ℝ) 2 (↑q : ℝ) + (HMul.hMul (α := ℝ) 1 0 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹) + (0 - p) +
          (1 * p - (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹)) +
        (HSub.hSub (α := ℝ) (↑q : ℝ) 1 - 0) =
      0
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
linarith :
  1 - p = 0 →
    HMul.hMul (α := ℝ) 1 0 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ +
          (1 * p - (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹)) +
        (1 - p - 0) =
      0
⊢ 1 - p ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
rw : log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))
⊢ log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p)

Tactic:
rw [← log_mul (by linarith) (by linarith)]

Premises used: Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
x : Membership.mem (γ := Set ℝ) (Ioi 0) (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))
a : p < HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)
⊢ log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))

Tactic:
apply Real.strictMonoOn_log (mem_Ioi.mpr hp.1)

Premises used: Iff.mpr, Set.mem_Ioi, And.left, Real.strictMonoOn_log
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
linarith :
  HSub.hSub (α := ℝ) (↑q : ℝ) 1 ≤ 0 →
    HSub.hSub (α := ℝ) 2 (↑q : ℝ) + (HMul.hMul (α := ℝ) 1 0 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹) + (0 - p) +
          (1 * p - (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹)) +
        (HSub.hSub (α := ℝ) (↑q : ℝ) 1 - 0) =
      0
⊢ 0 < HSub.hSub (α := ℝ) (↑q : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))

Tactic:
simp_all only [mem_Ioi, mul_pos_iff_of_pos_left, show 0 < (q : ℝ) - 1 by linarith]

Premises used: Set.mem_Ioi, mul_pos_iff_of_pos_left
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ LT.lt (α := ℝ) 0 (↑q : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ LT.lt (α := ℝ) 0 (↑q : ℝ)

Tactic:
have qpos : 0 < (q : ℝ) := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ (↑q : ℝ) * p < (↑q : ℝ) * HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹

Tactic:
mul_lt_mul_of_pos_left hp.2 qpos

Premises used: mul_lt_mul_of_pos_left, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
h : HSub.hSub (α := ℝ) (↑q : ℝ) 1 = (↑q : ℝ) * HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ (↑q : ℝ) * p < HSub.hSub (α := ℝ) (↑q : ℝ) 1

Tactic:
convert! mul_lt_mul_of_pos_left hp.2 qpos using 1

Premises used: mul_lt_mul_of_pos_left, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 = (↑q : ℝ) * HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹

Tactic:
simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
            IsUnit.mul_inv_cancel]

Premises used: mul_sub, IsUnit.mul_inv_cancel, ne_of_gt, isUnit_iff_ne_zero, ne_eq, mul_one, not_false_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ (↑q : ℝ) * p < HSub.hSub (α := ℝ) (↑q : ℝ) 1

Tactic:
have : q * p < q - 1 := by
          convert! mul_lt_mul_of_pos_left hp.2 qpos using 1
          simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
            IsUnit.mul_inv_cancel]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this_2 : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
this : (↑q : ℝ) * p < HSub.hSub (α := ℝ) (↑q : ℝ) 1
linarith :
  HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) ≤ p →
    (↑q : ℝ) * p - HSub.hSub (α := ℝ) (↑q : ℝ) 1 + (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) - p) = 0
⊢ p < HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ p ≠ 1

Tactic:
(ne_of_gt (lt_add_neg_iff_lt.mp this : p < 1)).symm

Premises used: ne_of_gt, lt_add_neg_iff_lt, Ne.symm, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ p ≠ 1

Tactic:
exact (ne_of_gt (lt_add_neg_iff_lt.mp this : p < 1)).symm

Premises used: ne_of_gt, lt_add_neg_iff_lt, Ne.symm, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
apply : ContinuousOn (qaryEntropy q) (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
apply₁ : ∀ x ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1), deriv (qaryEntropy q) x < 0
⊢ qaryEntropy q p2 < qaryEntropy q p1

Tactic:
apply strictAntiOn_of_deriv_neg (convex_Icc (1 - 1 / (q : ℝ)) 1) _ _ hp1 hp2 p1le2

Premises used: HSub.hSub, HDiv.hDiv, Nat.cast, convex_Icc, strictAntiOn_of_deriv_neg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
⊢ ContinuousOn (qaryEntropy q) (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)

Tactic:
qaryEntropy_continuous.continuousOn

Premises used: Continuous.continuousOn, Real.qaryEntropy_continuous
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
⊢ ContinuousOn (qaryEntropy q) (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)

Tactic:
exact qaryEntropy_continuous.continuousOn

Premises used: Continuous.continuousOn, Real.qaryEntropy_continuous
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
⊢ LE.le (α := ℝ) 2 (↑q : ℝ)

Tactic:
have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qLe2
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
linarith : LE.le (α := ℝ) (↑q : ℝ) 1 → -1 + HSub.hSub (α := ℝ) 2 (↑q : ℝ) + HSub.hSub (α := ℝ) (↑q : ℝ) 1 = 0
⊢ LT.lt (α := ℝ) 1 (↑q : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
⊢ LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1

Tactic:
have qinv_lt_1 : (q : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ (by linarith)
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
⊢ 0 < 1 - p

Tactic:
simp_all only [sub_pos, interior_Icc, mem_Ioo]

Premises used: sub_pos, Set.mem_Ioo, interior_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
⊢ 0 < 1 - p

Tactic:
have zero_lt_1_sub_p : 0 < 1 - p := by simp_all only [sub_pos, interior_Icc, mem_Ioo]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
⊢ HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1

Tactic:
simp only [one_div, interior_Icc, mem_Ioo] at hp

Premises used: Set.mem_Ioo, interior_Icc, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
linarith :
  p = 0 →
    HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - HMul.hMul (α := ℝ) 1 1 +
          (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - 1 * p) +
        (p - 0) =
      0
⊢ p ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
rw : log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p < 0
rw₁ : p ≠ 1
⊢ deriv (qaryEntropy q) p < 0

Tactic:
rw [deriv_qaryEntropy (by linarith)]

Premises used: Real.deriv_qaryEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
simp : log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) < log p
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p < 0

Tactic:
simp only [sub_neg, gt_iff_lt]

Premises used: sub_neg, gt_iff_lt
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
linarith :
  HSub.hSub (α := ℝ) (↑q : ℝ) 1 = 0 →
    HSub.hSub (α := ℝ) 2 (↑q : ℝ) + (HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - HMul.hMul (α := ℝ) 1 1) + (0 - (1 - p)) +
          (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - 1 * p) +
        (HSub.hSub (α := ℝ) (↑q : ℝ) 1 - 0) =
      0
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
linarith : 1 - p = 0 → 0 - (1 - p) + (1 - p - 0) = 0
⊢ 1 - p ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
rw : log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)) < log p
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) < log p

Tactic:
rw [← log_mul (by linarith) (by linarith)]

Premises used: Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
nlinarith :
  HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) ≤ 0 →
    0 - (1 - p) + (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) - 0) + (0 - HSub.hSub (α := ℝ) 2 (↑q : ℝ) * (0 - (1 - p))) =
      0
⊢ 0 < HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
x : Membership.mem (γ := Set ℝ) (Ioi 0) p
a : HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) < p
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)) < log p

Tactic:
apply Real.strictMonoOn_log (mem_Ioi.mpr (show 0 < (↑q - 1) * (1 - p) by nlinarith))

Premises used: Iff.mpr, Set.mem_Ioi, Real.strictMonoOn_log
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
linarith :
  p ≤ 0 →
    HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - HMul.hMul (α := ℝ) 1 1 +
          (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - 1 * p) +
        (p - 0) =
      0
⊢ 0 < p

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ LT.lt (α := ℝ) 0 (↑q : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ LT.lt (α := ℝ) 0 (↑q : ℝ)

Tactic:
have qpos : 0 < (q : ℝ) := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
a : HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p < p
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) < p

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)

Tactic:
have h1 := mul_lt_mul_of_pos_right hp.1 qpos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = (↑q : ℝ) - HMul.hMul (α := ℝ) (↑q : ℝ)⁻¹ (↑q : ℝ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
⊢ (↑q : ℝ) - HMul.hMul (α := ℝ) (↑q : ℝ)⁻¹ (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1

Tactic:
simp [qpos.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
calc : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = (↑q : ℝ) - HMul.hMul (α := ℝ) (↑q : ℝ)⁻¹ (↑q : ℝ)
calc₁ : (↑q : ℝ) - HMul.hMul (α := ℝ) (↑q : ℝ)⁻¹ (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1
⊢ HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1

Tactic:
calc (1 - (q : ℝ)⁻¹) * ↑q
            _ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
            _ = q - 1 := by simp [qpos.ne']

Premises used: HSub.hSub, Nat.cast, Inv.inv, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1

Tactic:
have h2 : (1 - (q : ℝ)⁻¹) * ↑q = q - 1 := by calc (1 - (q : ℝ)⁻¹) * ↑q
            _ = q - (q : ℝ)⁻¹ * (q : ℝ) := by ring
            _ = q - 1 := by simp [qpos.ne']
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
h2 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h1 : HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ))
    (h2 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) = HSub.hSub (α := ℝ) (↑q : ℝ) 1),
    HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ)

Tactic:
rwa [h2] at h1