simplipy-f64-edge

Rules only in rules_real.json (rejected in float64, e.g. because of overflow), real flavour; and exact ground identities found only there.

Case set `ba9dc4def822`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
sp-acj4-0-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-115-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-116-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-130-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-151-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-154-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-156-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-180-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-183-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-189-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-190-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-191-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-203-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-229-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-234-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-241-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-247-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-260-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-261-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
sp-acj4-266-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-267-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-29-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-3-real true	no verdict	no verdict	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓
sp-acj4-343-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-344-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-378-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-380-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-392-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-403-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-410-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-416-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-420-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-430-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-433-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-442-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-449-real true	no verdict	no verdict	no verdict	no verdict	true ✓	true ✓	no verdict	true ✓
sp-acj4-450-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-451-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-50-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-55-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-56-real contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
sp-acj4-6-real true	no verdict	no verdict	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓
sp-acj4-806-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-813-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-816-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓

sp-acj4-0-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \operatorname{arcosh}\left(\cosh x\right) = \left|x\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[0]: acosh cosh _0 -> abs _0

Lean proof: included

(case sp-acj4-0-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[0]: acosh cosh _0  ->  abs _0")
  (var x real)
  (ask (= (acosh (cosh x)) (abs x)))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.cosh_ofReal, AE.acosh_ofReal (Real.one_le_cosh r), AE.abs_ofReal, ← Real.cosh_abs, Real.arcosh_cosh (abs_nonneg r)]"))

sp-acj4-115-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x > 0,\quad \operatorname{surd}\left(x, -4\right) \neq 0$

Claim

$\displaystyle \frac{\log x}{-4} = \log\left(\operatorname{surd}\left(x, -4\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[115]: / log _0 (-4) -> log rootn _0 (-4)

Lean proof: included

(case sp-acj4-115-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[115]: / log _0 (-4)  ->  log rootn _0 (-4)")
  (var x real)
  (assume (nonzero x))
  (assume (> x 0))
  (assume (nonzero (surd x -4)))
  (ask (= (/ (log x) -4) (log (surd x -4))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : 0 < r := (by simpa using h1.2); refine ⟨⟨h0.2, h2.1.1, h2.2⟩, ?_⟩; rw [show (-4:ℂ) = ((-4:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg hr.le (by norm_num), AE.log_ofReal hr.le, AE.log_ofReal (by positivity), Real.log_rpow hr]; simp; ring"))

sp-acj4-116-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x > 0,\quad \operatorname{surd}\left(x, -6\right) \neq 0$

Claim

$\displaystyle \frac{\log x}{-6} = \log\left(\operatorname{surd}\left(x, -6\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[116]: / log _0 (-6) -> log rootn _0 (-6)

Lean proof: included

(case sp-acj4-116-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[116]: / log _0 (-6)  ->  log rootn _0 (-6)")
  (var x real)
  (assume (nonzero x))
  (assume (> x 0))
  (assume (nonzero (surd x -6)))
  (ask (= (/ (log x) -6) (log (surd x -6))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : 0 < r := (by simpa using h1.2); refine ⟨⟨h0.2, h2.1.1, h2.2⟩, ?_⟩; rw [show (-6:ℂ) = ((-6:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg hr.le (by norm_num), AE.log_ofReal hr.le, AE.log_ofReal (by positivity), Real.log_rpow hr]; simp; ring"))

sp-acj4-130-real

Given

$x \in \mathbb{R},\quad \cos x \neq 0,\quad \frac{1}{\cos x} \neq 0$

Claim

$\displaystyle \left|\log\left(\cos x\right)\right| \overset{?}{=} \log\left(\frac{1}{\cos x}\right)$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[130]: abs log cos _0 -> log inv cos _0

Lean proof: included

(case sp-acj4-130-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[130]: abs log cos _0  ->  log inv cos _0")
  (var x real)
  (assume (nonzero (cos x)))
  (assume (nonzero (/ (cos x))))
  (ask (= (abs (log (cos x))) (log (/ (cos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f130w2 | exact AE.w2_cos_two_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_ccos_two_ne]")))

sp-acj4-151-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\cos\left(\arcsin x\right)\right) \overset{?}{=} \left|\arcsin x\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[151]: acos cos asin _0 -> abs asin _0

Lean proof: included

(case sp-acj4-151-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[151]: acos cos asin _0  ->  abs asin _0")
  (var x real)
  (ask (= (acos (cos (asin x))) (abs (asin x))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f151w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-154-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\cos\left(\sin x\right)\right) = \left|\sin x\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[154]: acos cos sin _0 -> abs sin _0

Lean proof: included

(case sp-acj4-154-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[154]: acos cos sin _0  ->  abs sin _0")
  (var x real)
  (ask (= (acos (cos (sin x))) (abs (sin x))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.sin_ofReal, AE.cos_ofReal, AE.acos_ofReal (Real.neg_one_le_cos _) (Real.cos_le_one _), AE.abs_ofReal, ← Real.cos_abs, Real.arccos_cos (abs_nonneg _) (by linarith [abs_le.mpr ⟨Real.neg_one_le_sin r, Real.sin_le_one r⟩, Real.pi_gt_three])]"))

sp-acj4-156-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\sin\left(\arccos x\right)\right) \overset{?}{=} \left|\arcsin x\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[156]: acos sin acos _0 -> abs asin _0

Lean proof: included

(case sp-acj4-156-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[156]: acos sin acos _0  ->  abs asin _0")
  (var x real)
  (ask (= (acos (sin (acos x))) (abs (asin x))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f156w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

$x \in \mathbb{R},\quad \sinh\left(\operatorname{arcosh}\left(x\right)\right) \neq i,\quad \sinh\left(\operatorname{arcosh}\left(x\right)\right) \neq -i,\quad \cosh\left(\operatorname{arcosh}\left(x\right)\right) \neq 0$

Claim

$\displaystyle \arctan\left(\sinh\left(\operatorname{arcosh}\left(x\right)\right)\right) \overset{?}{=} \arcsin\left(\tanh\left(\operatorname{arcosh}\left(x\right)\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[180]: atan sinh acosh _0 -> asin tanh acosh _0

Lean proof: included

(case sp-acj4-180-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[180]: atan sinh acosh _0  ->  asin tanh acosh _0")
  (var x real)
  (assume (!= (sinh (acosh x)) i))
  (assume (!= (sinh (acosh x)) (- i)))
  (assume (nonzero (cosh (acosh x))))
  (ask (= (atan (sinh (acosh x))) (asin (tanh (acosh x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f180w2 | exact AE.w2_f180_hI | exact AE.w2_f180_hnI | exact AE.w2_f180_atanD | exact AE.w2_f180_cosh | exact AE.w2_f180_tanhD | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-183-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \sinh\left(\log x\right) \neq i,\quad \sinh\left(\log x\right) \neq -i,\quad \cosh\left(\log x\right) \neq 0$

Claim

$\displaystyle \arctan\left(\sinh\left(\log x\right)\right) \overset{?}{=} \arcsin\left(\tanh\left(\log x\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[183]: atan sinh log _0 -> asin tanh log _0

Lean proof: included

(case sp-acj4-183-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[183]: atan sinh log _0  ->  asin tanh log _0")
  (var x real)
  (assume (nonzero x))
  (assume (!= (sinh (log x)) i))
  (assume (!= (sinh (log x)) (- i)))
  (assume (nonzero (cosh (log x))))
  (ask (= (atan (sinh (log x))) (asin (tanh (log x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f183w2 | exact AE.w2_f183_hI | exact AE.w2_f183_hnI | exact AE.w2_f183_atanD | exact AE.w2_f183_cosh | exact AE.w2_f183_tanhD | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-189-real

Given

$x \in \mathbb{R},\quad \cos\left(\arcsin x\right) \neq 1,\quad \cos\left(\arcsin x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\cos\left(\arcsin x\right)\right) = \operatorname{arcosh}\left(\left|\frac{1}{x}\right|\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[189]: atanh cos asin _0 -> acosh abs inv _0

Lean proof: included

(case sp-acj4-189-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[189]: atanh cos asin _0  ->  acosh abs inv _0")
  (var x real)
  (assume (!= (cos (asin x)) 1))
  (assume (!= (cos (asin x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (cos (asin x))) (acosh (abs (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); refine ⟨⟨⟨⟨by simp, by simp⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.cos_eq, AE.cos_asin]; exact AE.atanh_sqrt_eq_acosh hr"))

sp-acj4-190-real

Given

$x \in \mathbb{R},\quad \cos\left(\arctan x\right) \neq 1,\quad \cos\left(\arctan x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\cos\left(\arctan x\right)\right) = \left|\operatorname{arsinh}\left(\frac{1}{x}\right)\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[190]: atanh cos atan _0 -> abs asinh inv _0

Lean proof: included

(case sp-acj4-190-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[190]: atanh cos atan _0  ->  abs asinh inv _0")
  (var x real)
  (assume (!= (cos (atan x)) 1))
  (assume (!= (cos (atan x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (cos (atan x))) (abs (asinh (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); have hS : 1 < Real.sqrt (1 + r ^ 2) := (Real.lt_sqrt zero_le_one).2 (by have := pow_pos (abs_pos.2 hr) 2; rw [sq_abs] at this; linarith); have hS0 : 0 < Real.sqrt (1 + r ^ 2) := (by linarith); refine ⟨⟨⟨⟨AE.atan.D_ofReal r, trivial⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.atan_ofReal, AE.cos_ofReal, Real.cos_arctan, AE.atanh_ofReal (by have := one_div_pos.2 hS0; linarith) ((div_lt_one hS0).2 hS), AE.inv_ofReal, AE.asinh_ofReal, AE.abs_ofReal, AE.artanh_eq_abs_arsinh hr]"))

sp-acj4-191-real

Given

$x \in \mathbb{R},\quad \sin\left(\arccos x\right) \neq 1,\quad \sin\left(\arccos x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\sin\left(\arccos x\right)\right) = \operatorname{arcosh}\left(\left|\frac{1}{x}\right|\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[191]: atanh sin acos _0 -> acosh abs inv _0

Lean proof: included

(case sp-acj4-191-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[191]: atanh sin acos _0  ->  acosh abs inv _0")
  (var x real)
  (assume (!= (sin (acos x)) 1))
  (assume (!= (sin (acos x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (sin (acos x))) (acosh (abs (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); refine ⟨⟨⟨⟨by simp, by simp⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.sin_eq, AE.sin_acos]; exact AE.atanh_sqrt_eq_acosh hr"))

sp-acj4-203-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle \cos\left(\log\left(\frac{1}{x}\right)\right) \overset{?}{=} \cos\left(\log x\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[203]: cos log inv _0 -> cos log _0

Lean proof: included

(case sp-acj4-203-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[203]: cos log inv _0  ->  cos log _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (cos (log (/ x))) (cos (log x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f203w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-229-real

Given

$x \in \mathbb{R},\quad \pi^{x} \neq 0$

Claim

$\displaystyle \frac{1}{\pi^{x}} = \frac{1}{\pi}^{x}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[229]: inv pow np.pi _0 -> pow inv np.pi _0

Lean proof: included

(case sp-acj4-229-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[229]: inv pow np.pi _0  ->  pow inv np.pi _0")
  (var x real)
  (assume (nonzero (pow pi x)))
  (ask (= (/ (pow pi x)) (pow (/ pi) x)))
  (expect true)
  (lean-proof "refine ⟨by simp_all [Real.pi_ne_zero], ?_⟩; simp only [AE.pi_def, AE.inv_def]; exact AE.inv_pow_base Real.pi_pos x"))

sp-acj4-234-real

Given

$x \in \mathbb{R},\quad x \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x^{x} \neq 0,\quad x \neq 0,\quad \frac{1}{x} \neq 0 \lor \operatorname{Re}\left(x\right) > 0$

Claim

$\displaystyle \frac{1}{x^{x}} \overset{?}{=} \frac{1}{x}^{x}$

Expected

contingent true at $x = 1$; false at $x = -\frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -\frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[234]: inv pow _0 _0 -> pow inv _0 _0

Lean proof: included

(case sp-acj4-234-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[234]: inv pow _0 _0  ->  pow inv _0 _0")
  (var x real)
  (assume (or (nonzero x) (> (re x) 0)))
  (assume (nonzero (pow x x)))
  (assume (nonzero x))
  (assume (or (nonzero (/ x)) (> (re x) 0)))
  (ask (= (/ (pow x x)) (pow (/ x) x)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f234w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-241-real

Given

$x \in \mathbb{R},\quad \operatorname{surd}\left(x, 3\right) \neq 0,\quad x \neq 0$

Claim

$\displaystyle \log\left(\operatorname{surd}\left(x, 3\right)\right) \overset{?}{=} \frac{\log x}{3}$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[241]: log rootn _0 3 -> / log _0 3

Lean proof: included

(case sp-acj4-241-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[241]: log rootn _0 3  ->  / log _0 3")
  (var x real)
  (assume (nonzero (surd x 3)))
  (assume (nonzero x))
  (ask (= (log (surd x 3)) (/ (log x) 3)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f241w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-247-real

Given

$x \in \mathbb{R},\quad \operatorname{surd}\left(x, 9\right) \neq 0,\quad x \neq 0$

Claim

$\displaystyle \log\left(\operatorname{surd}\left(x, 9\right)\right) \overset{?}{=} \frac{\log x}{9}$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[247]: log rootn _0 9 -> / log _0 9

Lean proof: included

(case sp-acj4-247-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[247]: log rootn _0 9  ->  / log _0 9")
  (var x real)
  (assume (nonzero (surd x 9)))
  (assume (nonzero x))
  (ask (= (log (surd x 9)) (/ (log x) 9)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f247w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-260-real

Given

$x \in \mathbb{R},\quad \cos x \neq 0,\quad \frac{1}{\cos x} \neq 0$

Claim

$\displaystyle -\log\left(\cos x\right) \overset{?}{=} \log\left(\frac{1}{\cos x}\right)$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[260]: neg log cos _0 -> log inv cos _0

Lean proof: included

(case sp-acj4-260-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[260]: neg log cos _0  ->  log inv cos _0")
  (var x real)
  (assume (nonzero (cos x)))
  (assume (nonzero (/ (cos x))))
  (ask (= (- (log (cos x))) (log (/ (cos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f260w2 | exact AE.w2_cos_two_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_ccos_two_ne]")))

sp-acj4-261-real

Given

$x \in \mathbb{R},\quad \cosh x \neq 0,\quad \frac{1}{\cosh x} \neq 0$

Claim

$\displaystyle -\log\left(\cosh x\right) = \log\left(\frac{1}{\cosh x}\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[261]: neg log cosh _0 -> log inv cosh _0

Lean proof: included

(case sp-acj4-261-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[261]: neg log cosh _0  ->  log inv cosh _0")
  (var x real)
  (assume (nonzero (cosh x)))
  (assume (nonzero (/ (cosh x))))
  (ask (= (- (log (cosh x))) (log (/ (cosh x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨h1.1.1, h1.1.1, h1.2⟩, ?_⟩; rw [AE.cosh_ofReal, AE.inv_ofReal, AE.log_ofReal (Real.cosh_pos r).le, AE.log_ofReal (inv_nonneg.2 (Real.cosh_pos r).le), Real.log_inv]; push_cast; ring"))

sp-acj4-266-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle -\sin\left(\log x\right) \overset{?}{=} \sin\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[266]: neg sin log _0 -> sin log inv _0

Lean proof: included

(case sp-acj4-266-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[266]: neg sin log _0  ->  sin log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (- (sin (log x))) (sin (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f266w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-267-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cos\left(\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cos\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle -\tan\left(\log x\right) \overset{?}{=} \tan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[267]: neg tan log _0 -> tan log inv _0

Lean proof: included

(case sp-acj4-267-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[267]: neg tan log _0  ->  tan log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cos (log x))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cos (log (/ x)))))
  (ask (= (- (tan (log x))) (tan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f267w2 | exact AE.w2_cos_log_neg_one | exact AE.w2_cos_log_inv_neg_one | exact AE.w2_tanD_log_neg_one | exact AE.w2_tanD_log_inv_neg_one | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-29-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x^{3} \neq 0$

Claim

$\displaystyle 3 \, \log x \overset{?}{=} \log\left(x^{3}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[29]: * 3 log _0 -> log pow _0 3

Lean proof: included

(case sp-acj4-29-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[29]: * 3 log _0  ->  log pow _0 3")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (pow x 3)))
  (ask (= (* 3 (log x)) (log (pow x 3))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f29w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-3-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \operatorname{arsinh}\left(\sinh x\right) = x$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[3]: asinh sinh _0 -> _0

Lean proof: included

(case sp-acj4-3-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[3]: asinh sinh _0  ->  _0")
  (var x real)
  (ask (= (asinh (sinh x)) x))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.sinh_ofReal, AE.asinh_ofReal, Real.arsinh_sinh]"))

sp-acj4-343-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \frac{1}{\pi}^{x} = \pi^{-x}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[343]: pow inv np.pi _0 -> pow np.pi neg _0

Lean proof: included

(case sp-acj4-343-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[343]: pow inv np.pi _0  ->  pow np.pi neg _0")
  (var x real)
  (ask (= (pow (/ pi) x) (pow pi (- x))))
  (expect true)
  (lean-proof "refine ⟨by simp [Real.pi_ne_zero], ?_⟩; simp only [AE.pi_def, AE.inv_def]; exact AE.pow_inv_base Real.pi_pos x"))

sp-acj4-344-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x \neq 0 \lor \operatorname{Re}\left(-x\right) > 0$

Claim

$\displaystyle \frac{1}{x}^{x} \overset{?}{=} x^{-x}$

Expected

contingent true at $x = 1$; false at $x = -\frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -\frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[344]: pow inv _0 _0 -> pow _0 neg _0

Lean proof: included

(case sp-acj4-344-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[344]: pow inv _0 _0  ->  pow _0 neg _0")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero (/ x)) (> (re x) 0)))
  (assume (or (nonzero x) (> (re (- x)) 0)))
  (ask (= (pow (/ x) x) (pow x (- x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f344w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-378-real

Given

$x \in \mathbb{R},\quad e^{x} \neq 0$

Claim

$\displaystyle \operatorname{surd}\left(e^{x}, -5\right) = e^{\frac{x}{-5}}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[378]: rootn exp _0 (-5) -> exp / _0 (-5)

Lean proof: included

(case sp-acj4-378-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[378]: rootn exp _0 (-5)  ->  exp / _0 (-5)")
  (var x real)
  (assume (nonzero (exp x)))
  (ask (= (surd (exp x) -5) (exp (/ x -5))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨(AE.surd.D_iff _ _).2 ⟨by simp [AE.exp_ofReal], (⟨-5, by norm_num⟩ : ∃ n : ℤ, (-5:ℂ) = n), by norm_num, Or.inl (by rw [AE.exp_ofReal, Complex.ofReal_re]; exact (Real.exp_pos r).le), Or.inl h0.2⟩, ?_⟩; rw [AE.exp_ofReal, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg (Real.exp_pos r).le (by norm_num), ← Real.exp_mul, show (r:ℂ) * AE.inv ((-5:ℤ):ℂ) = ((r * ((-5:ℤ):ℝ)⁻¹ : ℝ) : ℂ) by push_cast; simp, AE.exp_ofReal]"))

sp-acj4-380-real

Given

$x \in \mathbb{R},\quad e^{x} \neq 0$

Claim

$\displaystyle \operatorname{surd}\left(e^{x}, -7\right) = e^{\frac{x}{-7}}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[380]: rootn exp _0 (-7) -> exp / _0 (-7)

Lean proof: included

(case sp-acj4-380-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[380]: rootn exp _0 (-7)  ->  exp / _0 (-7)")
  (var x real)
  (assume (nonzero (exp x)))
  (ask (= (surd (exp x) -7) (exp (/ x -7))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨(AE.surd.D_iff _ _).2 ⟨by simp [AE.exp_ofReal], (⟨-7, by norm_num⟩ : ∃ n : ℤ, (-7:ℂ) = n), by norm_num, Or.inl (by rw [AE.exp_ofReal, Complex.ofReal_re]; exact (Real.exp_pos r).le), Or.inl h0.2⟩, ?_⟩; rw [AE.exp_ofReal, show (-7:ℂ) = ((-7:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg (Real.exp_pos r).le (by norm_num), ← Real.exp_mul, show (r:ℂ) * AE.inv ((-7:ℤ):ℂ) = ((r * ((-7:ℤ):ℝ)⁻¹ : ℝ) : ℂ) by push_cast; simp, AE.exp_ofReal]"))

sp-acj4-392-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \sin\left(\left|\arcsin x\right|\right) \overset{?}{=} \left|\cos\left(\arccos x\right)\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[392]: sin abs asin _0 -> abs cos acos _0

Lean proof: included

(case sp-acj4-392-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[392]: sin abs asin _0  ->  abs cos acos _0")
  (var x real)
  (ask (= (sin (abs (asin x))) (abs (cos (acos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f392w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-403-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle \sin\left(-\log x\right) \overset{?}{=} \sin\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[403]: sin neg log _0 -> sin log inv _0

Lean proof: included

(case sp-acj4-403-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[403]: sin neg log _0  ->  sin log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (sin (- (log x))) (sin (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f403w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-410-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \sinh x \neq 0$

Claim

$\displaystyle \sinh\left(e^{\log x}\right) = e^{\log\left(\sinh x\right)}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[410]: sinh exp log _0 -> exp log sinh _0

Lean proof: included

(case sp-acj4-410-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[410]: sinh exp log _0  ->  exp log sinh _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (sinh x)))
  (ask (= (sinh (exp (log x))) (exp (log (sinh x)))))
  (expect true)
  (lean-proof "have hs : Complex.sinh x ≠ 0 := (by simpa using h1.2); refine ⟨⟨⟨h0.2, trivial⟩, trivial, h1.2⟩, ?_⟩; simp only [AE.exp_def, AE.log_def, AE.sinh_eq]; rw [Complex.exp_log h0.2, Complex.exp_log hs]"))

sp-acj4-416-real

Given

$x \in \mathbb{R},\quad \cos\left(\arccos\left(\left|x\right|\right)\right) \neq 0,\quad \cos\left(\arccos x\right) \neq 0$

Claim

$\displaystyle \tan\left(\arccos\left(\left|x\right|\right)\right) \overset{?}{=} \left|\tan\left(\arccos x\right)\right|$

Expected

contingent true at $x = 1$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[416]: tan acos abs _0 -> abs tan acos _0

Lean proof: included

(case sp-acj4-416-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[416]: tan acos abs _0  ->  abs tan acos _0")
  (var x real)
  (assume (nonzero (cos (acos (abs x)))))
  (assume (nonzero (cos (acos x))))
  (ask (= (tan (acos (abs x))) (abs (tan (acos x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f416w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_cos_acos]")))

sp-acj4-420-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cos\left(-\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cos\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle \tan\left(-\log x\right) \overset{?}{=} \tan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[420]: tan neg log _0 -> tan log inv _0

Lean proof: included

(case sp-acj4-420-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[420]: tan neg log _0  ->  tan log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cos (- (log x)))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cos (log (/ x)))))
  (ask (= (tan (- (log x))) (tan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f420w2 | exact AE.w2_cos_neg_log_neg_one | exact AE.w2_cos_log_inv_neg_one | exact AE.w2_tanD_neg_log_neg_one | exact AE.w2_tanD_log_inv_neg_one | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-430-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x^{x} \neq 0$

Claim

$\displaystyle \log x \, x \overset{?}{=} \log\left(x^{x}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[430]: * log ?0 ?0 -> log pow ?0 ?0

Lean proof: included

(case sp-acj4-430-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[430]: * log ?0 ?0  ->  log pow ?0 ?0")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re x) 0)))
  (assume (nonzero (pow x x)))
  (ask (= (* (log x) x) (log (pow x x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f430w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-433-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad -\log x \neq i,\quad -\log x \neq -i,\quad \frac{1}{x} \neq 0,\quad \log\left(\frac{1}{x}\right) \neq i,\quad \log\left(\frac{1}{x}\right) \neq -i$

Claim

$\displaystyle \arctan\left(-\log x\right) \overset{?}{=} \arctan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[433]: atan neg log !0 -> atan log inv !0

Lean proof: included

(case sp-acj4-433-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[433]: atan neg log !0  ->  atan log inv !0")
  (var x real)
  (assume (nonzero x))
  (assume (!= (- (log x)) i))
  (assume (!= (- (log x)) (- i)))
  (assume (nonzero (/ x)))
  (assume (!= (log (/ x)) i))
  (assume (!= (log (/ x)) (- i)))
  (ask (= (atan (- (log x))) (atan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f433w2 | exact AE.w2_f433_h2 | exact AE.w2_f433_h3 | exact AE.w2_f433_h5 | exact AE.w2_f433_h6 | exact AE.w2_f433_atanD1 | exact AE.w2_f433_atanD2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-442-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \log x \neq 0,\quad \frac{1}{\log x} \neq 0$

Claim

$\displaystyle -\log\left(\log x\right) \overset{?}{=} \log\left(\frac{1}{\log x}\right)$

Expected

contingent true at $x = -1$; false at $x = \frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = -1$

witness (false): $x = \frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[442]: neg log log ?0 -> log inv log ?0

Lean proof: included

(case sp-acj4-442-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[442]: neg log log ?0  ->  log inv log ?0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (log x)))
  (assume (nonzero (/ (log x))))
  (ask (= (- (log (log x))) (log (/ (log x)))))
  (expect contingent)
  (witness true (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f442w1 | exact AE.w2_log_neg_one_ne | exact AE.w2_inv_log_neg_one_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f442w2 | exact AE.w2_log_half_ne | exact AE.w2_inv_log_half_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-449-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cosh\left(-\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cosh\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle \tanh\left(-\log x\right) = \tanh\left(\log\left(\frac{1}{x}\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[449]: tanh neg log !0 -> tanh log inv !0

Lean proof: included

(case sp-acj4-449-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[449]: tanh neg log !0  ->  tanh log inv !0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cosh (- (log x)))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cosh (log (/ x)))))
  (ask (= (tanh (- (log x))) (tanh (log (/ x)))))
  (expect true)
  (lean-proof "refine ⟨⟨⟨h0.2, (AE.tanh.D_iff _).2 (by simpa using h1.2)⟩, ⟨h0.2, h2.2⟩, (AE.tanh.D_iff _).2 (by simpa using h3.2)⟩, ?_⟩; simp only [AE.tanh_eq, AE.log_def, AE.inv_def]; exact AE.tanh_neg_log x h0.2"))

sp-acj4-450-real

Given

$x \in \mathbb{R},\quad x \neq 0$

Claim

$\displaystyle \frac{x}{x} = 1$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[450]: / $0 $0 -> 1

Lean proof: included

(case sp-acj4-450-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[450]: / $0 $0  ->  1")
  (var x real)
  (assume (nonzero x))
  (ask (= (/ x x) 1))
  (expect true)
  (lean-proof "simp_all"))

sp-acj4-451-real

Given

$x \in \mathbb{R},\quad x \neq 0$

Claim

$\displaystyle \frac{0}{x} = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[451]: / 0 $0 -> 0

Lean proof: included

(case sp-acj4-451-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[451]: / 0 $0  ->  0")
  (var x real)
  (assume (nonzero x))
  (ask (= (/ 0 x) 0))
  (expect true)
  (lean-proof "simp_all"))

sp-acj4-50-real

Given

$x \in \mathbb{R},\quad 6^{x} \neq 0$

Claim

$\displaystyle \log 6 \, x = \log\left(6^{x}\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[50]: * log 6 _0 -> log pow 6 _0

Lean proof: included

(case sp-acj4-50-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[50]: * log 6 _0  ->  log pow 6 _0")
  (var x real)
  (assume (nonzero (pow 6 x)))
  (ask (= (* (log 6) x) (log (pow 6 x))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨by norm_num, h0.1.1, h0.2⟩, ?_⟩; rw [show (6:ℂ) = ((6:ℝ):ℂ) by norm_num, AE.pow_ofReal (by norm_num) (Or.inl (by norm_num)), AE.log_ofReal (Real.rpow_nonneg (by norm_num) _), AE.log_ofReal (by norm_num), Real.log_rpow (by norm_num)]; push_cast; ring"))

sp-acj4-55-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(e^{1}\right) > 0,\quad x^{e^{1}} \neq 0$

Claim

$\displaystyle \log x \, e^{1} \overset{?}{=} \log\left(x^{e^{1}}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[55]: * log _0 np.e -> log pow _0 np.e

Lean proof: included

(case sp-acj4-55-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[55]: * log _0 np.e  ->  log pow _0 np.e")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re (exp 1)) 0)))
  (assume (nonzero (pow x (exp 1))))
  (ask (= (* (log x) (exp 1)) (log (pow x (exp 1)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f55w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-56-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(\pi\right) > 0,\quad x^{\pi} \neq 0$

Claim

$\displaystyle \log x \, \pi \overset{?}{=} \log\left(x^{\pi}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[56]: * log _0 np.pi -> log pow _0 np.pi

Lean proof: included

(case sp-acj4-56-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[56]: * log _0 np.pi  ->  log pow _0 np.pi")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re pi) 0)))
  (assume (nonzero (pow x pi)))
  (ask (= (* (log x) pi) (log (pow x pi))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f56w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-6-real

Given

$x \in \mathbb{R},\quad \tanh x \neq 1,\quad \tanh x \neq -1$

Claim

$\displaystyle \operatorname{artanh}\left(\tanh x\right) = x$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[6]: atanh tanh !0 -> !0

Lean proof: included

(case sp-acj4-6-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[6]: atanh tanh !0  ->  !0")
  (var x real)
  (assume (!= (tanh x) 1))
  (assume (!= (tanh x) -1))
  (ask (= (atanh (tanh x)) x))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨h0.1, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ?_⟩; rw [AE.tanh_ofReal, AE.atanh_ofReal (Real.neg_one_lt_tanh r) (Real.tanh_lt_one r), Real.artanh_tanh]"))

sp-acj4-806-ground

Given

nothing

Claim

$\displaystyle \cosh 0 = 1$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[806]: cosh 0 -> 1

Lean proof: included

(case sp-acj4-806-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[806]: cosh 0  ->  1")
  (ask (= (cosh 0) 1))
  (expect true)
  (lean-proof "simp"))

sp-acj4-813-ground

Given

nothing

Claim

$\displaystyle \sinh 0 = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[813]: sinh 0 -> 0

Lean proof: included

(case sp-acj4-813-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[813]: sinh 0  ->  0")
  (ask (= (sinh 0) 0))
  (expect true)
  (lean-proof "simp"))

sp-acj4-816-ground

Given

nothing

Claim

$\displaystyle \tanh 0 = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[816]: tanh 0 -> 0

Lean proof: included

(case sp-acj4-816-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[816]: tanh 0  ->  0")
  (ask (= (tanh 0) 0))
  (expect true)
  (lean-proof "simp"))

Case set `3ba0dfac4bca`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
sp-acj4-0-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-115-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-116-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-130-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-151-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-154-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-156-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-180-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-183-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-189-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-190-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-191-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-203-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-229-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-234-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-241-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-247-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-260-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-261-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
sp-acj4-266-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-267-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-29-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-3-real true	no verdict	no verdict	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓
sp-acj4-343-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-344-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-378-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-380-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-392-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-403-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-410-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-416-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-420-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-430-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-433-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-442-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-449-real true	no verdict	no verdict	no verdict	no verdict	true ✓	true ✓	no verdict	true ✓
sp-acj4-450-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-451-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-50-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-55-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-56-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-6-real true	no verdict	no verdict	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓
sp-acj4-806-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-813-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-816-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓

sp-acj4-0-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \operatorname{arcosh}\left(\cosh x\right) = \left|x\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[0]: acosh cosh _0 -> abs _0

Lean proof: included

(case sp-acj4-0-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[0]: acosh cosh _0  ->  abs _0")
  (var x real)
  (ask (= (acosh (cosh x)) (abs x)))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.cosh_ofReal, AE.acosh_ofReal (Real.one_le_cosh r), AE.abs_ofReal, ← Real.cosh_abs, Real.arcosh_cosh (abs_nonneg r)]"))

sp-acj4-115-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x > 0,\quad \operatorname{surd}\left(x, -4\right) \neq 0$

Claim

$\displaystyle \frac{\log x}{-4} = \log\left(\operatorname{surd}\left(x, -4\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[115]: / log _0 (-4) -> log rootn _0 (-4)

Lean proof: included

(case sp-acj4-115-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[115]: / log _0 (-4)  ->  log rootn _0 (-4)")
  (var x real)
  (assume (nonzero x))
  (assume (> x 0))
  (assume (nonzero (surd x -4)))
  (ask (= (/ (log x) -4) (log (surd x -4))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : 0 < r := (by simpa using h1.2); refine ⟨⟨h0.2, h2.1.1, h2.2⟩, ?_⟩; rw [show (-4:ℂ) = ((-4:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg hr.le (by norm_num), AE.log_ofReal hr.le, AE.log_ofReal (by positivity), Real.log_rpow hr]; simp; ring"))

sp-acj4-116-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x > 0,\quad \operatorname{surd}\left(x, -6\right) \neq 0$

Claim

$\displaystyle \frac{\log x}{-6} = \log\left(\operatorname{surd}\left(x, -6\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[116]: / log _0 (-6) -> log rootn _0 (-6)

Lean proof: included

(case sp-acj4-116-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[116]: / log _0 (-6)  ->  log rootn _0 (-6)")
  (var x real)
  (assume (nonzero x))
  (assume (> x 0))
  (assume (nonzero (surd x -6)))
  (ask (= (/ (log x) -6) (log (surd x -6))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : 0 < r := (by simpa using h1.2); refine ⟨⟨h0.2, h2.1.1, h2.2⟩, ?_⟩; rw [show (-6:ℂ) = ((-6:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg hr.le (by norm_num), AE.log_ofReal hr.le, AE.log_ofReal (by positivity), Real.log_rpow hr]; simp; ring"))

sp-acj4-130-real

Given

$x \in \mathbb{R},\quad \cos x \neq 0,\quad \frac{1}{\cos x} \neq 0$

Claim

$\displaystyle \left|\log\left(\cos x\right)\right| \overset{?}{=} \log\left(\frac{1}{\cos x}\right)$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[130]: abs log cos _0 -> log inv cos _0

Lean proof: included

(case sp-acj4-130-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[130]: abs log cos _0  ->  log inv cos _0")
  (var x real)
  (assume (nonzero (cos x)))
  (assume (nonzero (/ (cos x))))
  (ask (= (abs (log (cos x))) (log (/ (cos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f130w2 | exact AE.w2_cos_two_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_ccos_two_ne]")))

sp-acj4-151-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\cos\left(\arcsin x\right)\right) \overset{?}{=} \left|\arcsin x\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[151]: acos cos asin _0 -> abs asin _0

Lean proof: included

(case sp-acj4-151-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[151]: acos cos asin _0  ->  abs asin _0")
  (var x real)
  (ask (= (acos (cos (asin x))) (abs (asin x))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f151w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-154-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\cos\left(\sin x\right)\right) = \left|\sin x\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[154]: acos cos sin _0 -> abs sin _0

Lean proof: included

(case sp-acj4-154-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[154]: acos cos sin _0  ->  abs sin _0")
  (var x real)
  (ask (= (acos (cos (sin x))) (abs (sin x))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.sin_ofReal, AE.cos_ofReal, AE.acos_ofReal (Real.neg_one_le_cos _) (Real.cos_le_one _), AE.abs_ofReal, ← Real.cos_abs, Real.arccos_cos (abs_nonneg _) (by linarith [abs_le.mpr ⟨Real.neg_one_le_sin r, Real.sin_le_one r⟩, Real.pi_gt_three])]"))

sp-acj4-156-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\sin\left(\arccos x\right)\right) \overset{?}{=} \left|\arcsin x\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[156]: acos sin acos _0 -> abs asin _0

Lean proof: included

(case sp-acj4-156-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[156]: acos sin acos _0  ->  abs asin _0")
  (var x real)
  (ask (= (acos (sin (acos x))) (abs (asin x))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f156w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-180-real

Given

Claim

$\displaystyle \arctan\left(\sinh\left(\operatorname{arcosh}\left(x\right)\right)\right) \overset{?}{=} \arcsin\left(\tanh\left(\operatorname{arcosh}\left(x\right)\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[180]: atan sinh acosh _0 -> asin tanh acosh _0

Lean proof: included

(case sp-acj4-180-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[180]: atan sinh acosh _0  ->  asin tanh acosh _0")
  (var x real)
  (assume (!= (sinh (acosh x)) i))
  (assume (!= (sinh (acosh x)) (- i)))
  (assume (nonzero (cosh (acosh x))))
  (ask (= (atan (sinh (acosh x))) (asin (tanh (acosh x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f180w2 | exact AE.w2_f180_hI | exact AE.w2_f180_hnI | exact AE.w2_f180_atanD | exact AE.w2_f180_cosh | exact AE.w2_f180_tanhD | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-183-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \sinh\left(\log x\right) \neq i,\quad \sinh\left(\log x\right) \neq -i,\quad \cosh\left(\log x\right) \neq 0$

Claim

$\displaystyle \arctan\left(\sinh\left(\log x\right)\right) \overset{?}{=} \arcsin\left(\tanh\left(\log x\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[183]: atan sinh log _0 -> asin tanh log _0

Lean proof: included

(case sp-acj4-183-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[183]: atan sinh log _0  ->  asin tanh log _0")
  (var x real)
  (assume (nonzero x))
  (assume (!= (sinh (log x)) i))
  (assume (!= (sinh (log x)) (- i)))
  (assume (nonzero (cosh (log x))))
  (ask (= (atan (sinh (log x))) (asin (tanh (log x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f183w2 | exact AE.w2_f183_hI | exact AE.w2_f183_hnI | exact AE.w2_f183_atanD | exact AE.w2_f183_cosh | exact AE.w2_f183_tanhD | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-189-real

Given

$x \in \mathbb{R},\quad \cos\left(\arcsin x\right) \neq 1,\quad \cos\left(\arcsin x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\cos\left(\arcsin x\right)\right) = \operatorname{arcosh}\left(\left|\frac{1}{x}\right|\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[189]: atanh cos asin _0 -> acosh abs inv _0

Lean proof: included

(case sp-acj4-189-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[189]: atanh cos asin _0  ->  acosh abs inv _0")
  (var x real)
  (assume (!= (cos (asin x)) 1))
  (assume (!= (cos (asin x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (cos (asin x))) (acosh (abs (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); refine ⟨⟨⟨⟨by simp, by simp⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.cos_eq, AE.cos_asin]; exact AE.atanh_sqrt_eq_acosh hr"))

sp-acj4-190-real

Given

$x \in \mathbb{R},\quad \cos\left(\arctan x\right) \neq 1,\quad \cos\left(\arctan x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\cos\left(\arctan x\right)\right) = \left|\operatorname{arsinh}\left(\frac{1}{x}\right)\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[190]: atanh cos atan _0 -> abs asinh inv _0

Lean proof: included

(case sp-acj4-190-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[190]: atanh cos atan _0  ->  abs asinh inv _0")
  (var x real)
  (assume (!= (cos (atan x)) 1))
  (assume (!= (cos (atan x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (cos (atan x))) (abs (asinh (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); have hS : 1 < Real.sqrt (1 + r ^ 2) := (Real.lt_sqrt zero_le_one).2 (by have := pow_pos (abs_pos.2 hr) 2; rw [sq_abs] at this; linarith); have hS0 : 0 < Real.sqrt (1 + r ^ 2) := (by linarith); refine ⟨⟨⟨⟨AE.atan.D_ofReal r, trivial⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.atan_ofReal, AE.cos_ofReal, Real.cos_arctan, AE.atanh_ofReal (by have := one_div_pos.2 hS0; linarith) ((div_lt_one hS0).2 hS), AE.inv_ofReal, AE.asinh_ofReal, AE.abs_ofReal, AE.artanh_eq_abs_arsinh hr]"))

sp-acj4-191-real

Given

$x \in \mathbb{R},\quad \sin\left(\arccos x\right) \neq 1,\quad \sin\left(\arccos x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\sin\left(\arccos x\right)\right) = \operatorname{arcosh}\left(\left|\frac{1}{x}\right|\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[191]: atanh sin acos _0 -> acosh abs inv _0

Lean proof: included

(case sp-acj4-191-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[191]: atanh sin acos _0  ->  acosh abs inv _0")
  (var x real)
  (assume (!= (sin (acos x)) 1))
  (assume (!= (sin (acos x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (sin (acos x))) (acosh (abs (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); refine ⟨⟨⟨⟨by simp, by simp⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.sin_eq, AE.sin_acos]; exact AE.atanh_sqrt_eq_acosh hr"))

sp-acj4-203-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle \cos\left(\log\left(\frac{1}{x}\right)\right) \overset{?}{=} \cos\left(\log x\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[203]: cos log inv _0 -> cos log _0

Lean proof: included

(case sp-acj4-203-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[203]: cos log inv _0  ->  cos log _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (cos (log (/ x))) (cos (log x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f203w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-229-real

Given

$x \in \mathbb{R},\quad \pi^{x} \neq 0$

Claim

$\displaystyle \frac{1}{\pi^{x}} = \frac{1}{\pi}^{x}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[229]: inv pow np.pi _0 -> pow inv np.pi _0

Lean proof: included

(case sp-acj4-229-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[229]: inv pow np.pi _0  ->  pow inv np.pi _0")
  (var x real)
  (assume (nonzero (pow pi x)))
  (ask (= (/ (pow pi x)) (pow (/ pi) x)))
  (expect true)
  (lean-proof "refine ⟨by simp_all [Real.pi_ne_zero], ?_⟩; simp only [AE.pi_def, AE.inv_def]; exact AE.inv_pow_base Real.pi_pos x"))

sp-acj4-234-real

Given

$x \in \mathbb{R},\quad x \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x^{x} \neq 0,\quad x \neq 0,\quad \frac{1}{x} \neq 0 \lor \operatorname{Re}\left(x\right) > 0$

Claim

$\displaystyle \frac{1}{x^{x}} \overset{?}{=} \frac{1}{x}^{x}$

Expected

contingent true at $x = 1$; false at $x = -\frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -\frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[234]: inv pow _0 _0 -> pow inv _0 _0

Lean proof: included

(case sp-acj4-234-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[234]: inv pow _0 _0  ->  pow inv _0 _0")
  (var x real)
  (assume (or (nonzero x) (> (re x) 0)))
  (assume (nonzero (pow x x)))
  (assume (nonzero x))
  (assume (or (nonzero (/ x)) (> (re x) 0)))
  (ask (= (/ (pow x x)) (pow (/ x) x)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f234w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-241-real

Given

$x \in \mathbb{R},\quad \operatorname{surd}\left(x, 3\right) \neq 0,\quad x \neq 0$

Claim

$\displaystyle \log\left(\operatorname{surd}\left(x, 3\right)\right) \overset{?}{=} \frac{\log x}{3}$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[241]: log rootn _0 3 -> / log _0 3

Lean proof: included

(case sp-acj4-241-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[241]: log rootn _0 3  ->  / log _0 3")
  (var x real)
  (assume (nonzero (surd x 3)))
  (assume (nonzero x))
  (ask (= (log (surd x 3)) (/ (log x) 3)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f241w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-247-real

Given

$x \in \mathbb{R},\quad \operatorname{surd}\left(x, 9\right) \neq 0,\quad x \neq 0$

Claim

$\displaystyle \log\left(\operatorname{surd}\left(x, 9\right)\right) \overset{?}{=} \frac{\log x}{9}$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[247]: log rootn _0 9 -> / log _0 9

Lean proof: included

(case sp-acj4-247-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[247]: log rootn _0 9  ->  / log _0 9")
  (var x real)
  (assume (nonzero (surd x 9)))
  (assume (nonzero x))
  (ask (= (log (surd x 9)) (/ (log x) 9)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f247w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-260-real

Given

$x \in \mathbb{R},\quad \cos x \neq 0,\quad \frac{1}{\cos x} \neq 0$

Claim

$\displaystyle -\log\left(\cos x\right) \overset{?}{=} \log\left(\frac{1}{\cos x}\right)$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[260]: neg log cos _0 -> log inv cos _0

Lean proof: included

(case sp-acj4-260-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[260]: neg log cos _0  ->  log inv cos _0")
  (var x real)
  (assume (nonzero (cos x)))
  (assume (nonzero (/ (cos x))))
  (ask (= (- (log (cos x))) (log (/ (cos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f260w2 | exact AE.w2_cos_two_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_ccos_two_ne]")))

sp-acj4-261-real

Given

$x \in \mathbb{R},\quad \cosh x \neq 0,\quad \frac{1}{\cosh x} \neq 0$

Claim

$\displaystyle -\log\left(\cosh x\right) = \log\left(\frac{1}{\cosh x}\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[261]: neg log cosh _0 -> log inv cosh _0

Lean proof: included

(case sp-acj4-261-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[261]: neg log cosh _0  ->  log inv cosh _0")
  (var x real)
  (assume (nonzero (cosh x)))
  (assume (nonzero (/ (cosh x))))
  (ask (= (- (log (cosh x))) (log (/ (cosh x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨h1.1.1, h1.1.1, h1.2⟩, ?_⟩; rw [AE.cosh_ofReal, AE.inv_ofReal, AE.log_ofReal (Real.cosh_pos r).le, AE.log_ofReal (inv_nonneg.2 (Real.cosh_pos r).le), Real.log_inv]; push_cast; ring"))

sp-acj4-266-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle -\sin\left(\log x\right) \overset{?}{=} \sin\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[266]: neg sin log _0 -> sin log inv _0

Lean proof: included

(case sp-acj4-266-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[266]: neg sin log _0  ->  sin log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (- (sin (log x))) (sin (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f266w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-267-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cos\left(\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cos\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle -\tan\left(\log x\right) \overset{?}{=} \tan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[267]: neg tan log _0 -> tan log inv _0

Lean proof: included

(case sp-acj4-267-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[267]: neg tan log _0  ->  tan log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cos (log x))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cos (log (/ x)))))
  (ask (= (- (tan (log x))) (tan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f267w2 | exact AE.w2_cos_log_neg_one | exact AE.w2_cos_log_inv_neg_one | exact AE.w2_tanD_log_neg_one | exact AE.w2_tanD_log_inv_neg_one | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-29-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x^{3} \neq 0$

Claim

$\displaystyle 3 \, \log x \overset{?}{=} \log\left(x^{3}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[29]: * 3 log _0 -> log pow _0 3

Lean proof: included

(case sp-acj4-29-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[29]: * 3 log _0  ->  log pow _0 3")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (pow x 3)))
  (ask (= (* 3 (log x)) (log (pow x 3))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f29w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-3-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \operatorname{arsinh}\left(\sinh x\right) = x$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[3]: asinh sinh _0 -> _0

Lean proof: included

(case sp-acj4-3-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[3]: asinh sinh _0  ->  _0")
  (var x real)
  (ask (= (asinh (sinh x)) x))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.sinh_ofReal, AE.asinh_ofReal, Real.arsinh_sinh]"))

sp-acj4-343-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \frac{1}{\pi}^{x} = \pi^{-x}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[343]: pow inv np.pi _0 -> pow np.pi neg _0

Lean proof: included

(case sp-acj4-343-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[343]: pow inv np.pi _0  ->  pow np.pi neg _0")
  (var x real)
  (ask (= (pow (/ pi) x) (pow pi (- x))))
  (expect true)
  (lean-proof "refine ⟨by simp [Real.pi_ne_zero], ?_⟩; simp only [AE.pi_def, AE.inv_def]; exact AE.pow_inv_base Real.pi_pos x"))

sp-acj4-344-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x \neq 0 \lor \operatorname{Re}\left(-x\right) > 0$

Claim

$\displaystyle \frac{1}{x}^{x} \overset{?}{=} x^{-x}$

Expected

contingent true at $x = 1$; false at $x = -\frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -\frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[344]: pow inv _0 _0 -> pow _0 neg _0

Lean proof: included

(case sp-acj4-344-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[344]: pow inv _0 _0  ->  pow _0 neg _0")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero (/ x)) (> (re x) 0)))
  (assume (or (nonzero x) (> (re (- x)) 0)))
  (ask (= (pow (/ x) x) (pow x (- x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f344w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-378-real

Given

$x \in \mathbb{R},\quad e^{x} \neq 0$

Claim

$\displaystyle \operatorname{surd}\left(e^{x}, -5\right) = e^{\frac{x}{-5}}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[378]: rootn exp _0 (-5) -> exp / _0 (-5)

Lean proof: included

(case sp-acj4-378-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[378]: rootn exp _0 (-5)  ->  exp / _0 (-5)")
  (var x real)
  (assume (nonzero (exp x)))
  (ask (= (surd (exp x) -5) (exp (/ x -5))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨(AE.surd.D_iff _ _).2 ⟨by simp [AE.exp_ofReal], (⟨-5, by norm_num⟩ : ∃ n : ℤ, (-5:ℂ) = n), by norm_num, Or.inl (by rw [AE.exp_ofReal, Complex.ofReal_re]; exact (Real.exp_pos r).le), Or.inl h0.2⟩, ?_⟩; rw [AE.exp_ofReal, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg (Real.exp_pos r).le (by norm_num), ← Real.exp_mul, show (r:ℂ) * AE.inv ((-5:ℤ):ℂ) = ((r * ((-5:ℤ):ℝ)⁻¹ : ℝ) : ℂ) by push_cast; simp, AE.exp_ofReal]"))

sp-acj4-380-real

Given

$x \in \mathbb{R},\quad e^{x} \neq 0$

Claim

$\displaystyle \operatorname{surd}\left(e^{x}, -7\right) = e^{\frac{x}{-7}}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[380]: rootn exp _0 (-7) -> exp / _0 (-7)

Lean proof: included

(case sp-acj4-380-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[380]: rootn exp _0 (-7)  ->  exp / _0 (-7)")
  (var x real)
  (assume (nonzero (exp x)))
  (ask (= (surd (exp x) -7) (exp (/ x -7))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨(AE.surd.D_iff _ _).2 ⟨by simp [AE.exp_ofReal], (⟨-7, by norm_num⟩ : ∃ n : ℤ, (-7:ℂ) = n), by norm_num, Or.inl (by rw [AE.exp_ofReal, Complex.ofReal_re]; exact (Real.exp_pos r).le), Or.inl h0.2⟩, ?_⟩; rw [AE.exp_ofReal, show (-7:ℂ) = ((-7:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg (Real.exp_pos r).le (by norm_num), ← Real.exp_mul, show (r:ℂ) * AE.inv ((-7:ℤ):ℂ) = ((r * ((-7:ℤ):ℝ)⁻¹ : ℝ) : ℂ) by push_cast; simp, AE.exp_ofReal]"))

sp-acj4-392-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \sin\left(\left|\arcsin x\right|\right) \overset{?}{=} \left|\cos\left(\arccos x\right)\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[392]: sin abs asin _0 -> abs cos acos _0

Lean proof: included

(case sp-acj4-392-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[392]: sin abs asin _0  ->  abs cos acos _0")
  (var x real)
  (ask (= (sin (abs (asin x))) (abs (cos (acos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f392w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-403-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle \sin\left(-\log x\right) \overset{?}{=} \sin\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[403]: sin neg log _0 -> sin log inv _0

Lean proof: included

(case sp-acj4-403-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[403]: sin neg log _0  ->  sin log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (sin (- (log x))) (sin (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f403w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-410-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \sinh x \neq 0$

Claim

$\displaystyle \sinh\left(e^{\log x}\right) = e^{\log\left(\sinh x\right)}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[410]: sinh exp log _0 -> exp log sinh _0

Lean proof: included

(case sp-acj4-410-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[410]: sinh exp log _0  ->  exp log sinh _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (sinh x)))
  (ask (= (sinh (exp (log x))) (exp (log (sinh x)))))
  (expect true)
  (lean-proof "have hs : Complex.sinh x ≠ 0 := (by simpa using h1.2); refine ⟨⟨⟨h0.2, trivial⟩, trivial, h1.2⟩, ?_⟩; simp only [AE.exp_def, AE.log_def, AE.sinh_eq]; rw [Complex.exp_log h0.2, Complex.exp_log hs]"))

sp-acj4-416-real

Given

$x \in \mathbb{R},\quad \cos\left(\arccos\left(\left|x\right|\right)\right) \neq 0,\quad \cos\left(\arccos x\right) \neq 0$

Claim

$\displaystyle \tan\left(\arccos\left(\left|x\right|\right)\right) \overset{?}{=} \left|\tan\left(\arccos x\right)\right|$

Expected

contingent true at $x = 1$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[416]: tan acos abs _0 -> abs tan acos _0

Lean proof: included

(case sp-acj4-416-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[416]: tan acos abs _0  ->  abs tan acos _0")
  (var x real)
  (assume (nonzero (cos (acos (abs x)))))
  (assume (nonzero (cos (acos x))))
  (ask (= (tan (acos (abs x))) (abs (tan (acos x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f416w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_cos_acos]")))

sp-acj4-420-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cos\left(-\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cos\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle \tan\left(-\log x\right) \overset{?}{=} \tan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[420]: tan neg log _0 -> tan log inv _0

Lean proof: included

(case sp-acj4-420-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[420]: tan neg log _0  ->  tan log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cos (- (log x)))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cos (log (/ x)))))
  (ask (= (tan (- (log x))) (tan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f420w2 | exact AE.w2_cos_neg_log_neg_one | exact AE.w2_cos_log_inv_neg_one | exact AE.w2_tanD_neg_log_neg_one | exact AE.w2_tanD_log_inv_neg_one | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-430-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x^{x} \neq 0$

Claim

$\displaystyle \log x \, x \overset{?}{=} \log\left(x^{x}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[430]: * log ?0 ?0 -> log pow ?0 ?0

Lean proof: included

(case sp-acj4-430-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[430]: * log ?0 ?0  ->  log pow ?0 ?0")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re x) 0)))
  (assume (nonzero (pow x x)))
  (ask (= (* (log x) x) (log (pow x x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f430w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-433-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad -\log x \neq i,\quad -\log x \neq -i,\quad \frac{1}{x} \neq 0,\quad \log\left(\frac{1}{x}\right) \neq i,\quad \log\left(\frac{1}{x}\right) \neq -i$

Claim

$\displaystyle \arctan\left(-\log x\right) \overset{?}{=} \arctan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[433]: atan neg log !0 -> atan log inv !0

Lean proof: included

(case sp-acj4-433-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[433]: atan neg log !0  ->  atan log inv !0")
  (var x real)
  (assume (nonzero x))
  (assume (!= (- (log x)) i))
  (assume (!= (- (log x)) (- i)))
  (assume (nonzero (/ x)))
  (assume (!= (log (/ x)) i))
  (assume (!= (log (/ x)) (- i)))
  (ask (= (atan (- (log x))) (atan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f433w2 | exact AE.w2_f433_h2 | exact AE.w2_f433_h3 | exact AE.w2_f433_h5 | exact AE.w2_f433_h6 | exact AE.w2_f433_atanD1 | exact AE.w2_f433_atanD2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-442-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \log x \neq 0,\quad \frac{1}{\log x} \neq 0$

Claim

$\displaystyle -\log\left(\log x\right) \overset{?}{=} \log\left(\frac{1}{\log x}\right)$

Expected

contingent true at $x = -1$; false at $x = \frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = -1$

witness (false): $x = \frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[442]: neg log log ?0 -> log inv log ?0

Lean proof: included

(case sp-acj4-442-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[442]: neg log log ?0  ->  log inv log ?0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (log x)))
  (assume (nonzero (/ (log x))))
  (ask (= (- (log (log x))) (log (/ (log x)))))
  (expect contingent)
  (witness true (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f442w1 | exact AE.w2_log_neg_one_ne | exact AE.w2_inv_log_neg_one_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f442w2 | exact AE.w2_log_half_ne | exact AE.w2_inv_log_half_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-449-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cosh\left(-\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cosh\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle \tanh\left(-\log x\right) = \tanh\left(\log\left(\frac{1}{x}\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[449]: tanh neg log !0 -> tanh log inv !0

Lean proof: included

(case sp-acj4-449-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[449]: tanh neg log !0  ->  tanh log inv !0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cosh (- (log x)))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cosh (log (/ x)))))
  (ask (= (tanh (- (log x))) (tanh (log (/ x)))))
  (expect true)
  (lean-proof "refine ⟨⟨⟨h0.2, (AE.tanh.D_iff _).2 (by simpa using h1.2)⟩, ⟨h0.2, h2.2⟩, (AE.tanh.D_iff _).2 (by simpa using h3.2)⟩, ?_⟩; simp only [AE.tanh_eq, AE.log_def, AE.inv_def]; exact AE.tanh_neg_log x h0.2"))

sp-acj4-450-real

Given

$x \in \mathbb{R},\quad x \neq 0$

Claim

$\displaystyle \frac{x}{x} = 1$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[450]: / $0 $0 -> 1

Lean proof: included

(case sp-acj4-450-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[450]: / $0 $0  ->  1")
  (var x real)
  (assume (nonzero x))
  (ask (= (/ x x) 1))
  (expect true)
  (lean-proof "simp_all"))

sp-acj4-451-real

Given

$x \in \mathbb{R},\quad x \neq 0$

Claim

$\displaystyle \frac{0}{x} = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[451]: / 0 $0 -> 0

Lean proof: included

(case sp-acj4-451-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[451]: / 0 $0  ->  0")
  (var x real)
  (assume (nonzero x))
  (ask (= (/ 0 x) 0))
  (expect true)
  (lean-proof "simp_all"))

sp-acj4-50-real

Given

$x \in \mathbb{R},\quad 6^{x} \neq 0$

Claim

$\displaystyle \log 6 \, x = \log\left(6^{x}\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[50]: * log 6 _0 -> log pow 6 _0

Lean proof: included

(case sp-acj4-50-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[50]: * log 6 _0  ->  log pow 6 _0")
  (var x real)
  (assume (nonzero (pow 6 x)))
  (ask (= (* (log 6) x) (log (pow 6 x))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨by norm_num, h0.1.1, h0.2⟩, ?_⟩; rw [show (6:ℂ) = ((6:ℝ):ℂ) by norm_num, AE.pow_ofReal (by norm_num) (Or.inl (by norm_num)), AE.log_ofReal (Real.rpow_nonneg (by norm_num) _), AE.log_ofReal (by norm_num), Real.log_rpow (by norm_num)]; push_cast; ring"))

sp-acj4-55-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(e^{1}\right) > 0,\quad x^{e^{1}} \neq 0$

Claim

$\displaystyle \log x \, e^{1} \overset{?}{=} \log\left(x^{e^{1}}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[55]: * log _0 np.e -> log pow _0 np.e

Lean proof: included

(case sp-acj4-55-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[55]: * log _0 np.e  ->  log pow _0 np.e")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re (exp 1)) 0)))
  (assume (nonzero (pow x (exp 1))))
  (ask (= (* (log x) (exp 1)) (log (pow x (exp 1)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f55w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-56-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(\pi\right) > 0,\quad x^{\pi} \neq 0$

Claim

$\displaystyle \log x \, \pi \overset{?}{=} \log\left(x^{\pi}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[56]: * log _0 np.pi -> log pow _0 np.pi

Lean proof: included

(case sp-acj4-56-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[56]: * log _0 np.pi  ->  log pow _0 np.pi")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re pi) 0)))
  (assume (nonzero (pow x pi)))
  (ask (= (* (log x) pi) (log (pow x pi))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f56w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-6-real

Given

$x \in \mathbb{R},\quad \tanh x \neq 1,\quad \tanh x \neq -1$

Claim

$\displaystyle \operatorname{artanh}\left(\tanh x\right) = x$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[6]: atanh tanh !0 -> !0

Lean proof: included

(case sp-acj4-6-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[6]: atanh tanh !0  ->  !0")
  (var x real)
  (assume (!= (tanh x) 1))
  (assume (!= (tanh x) -1))
  (ask (= (atanh (tanh x)) x))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨h0.1, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ?_⟩; rw [AE.tanh_ofReal, AE.atanh_ofReal (Real.neg_one_lt_tanh r) (Real.tanh_lt_one r), Real.artanh_tanh]"))

sp-acj4-806-ground

Given

nothing

Claim

$\displaystyle \cosh 0 = 1$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[806]: cosh 0 -> 1

Lean proof: included

(case sp-acj4-806-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[806]: cosh 0  ->  1")
  (ask (= (cosh 0) 1))
  (expect true)
  (lean-proof "simp"))

sp-acj4-813-ground

Given

nothing

Claim

$\displaystyle \sinh 0 = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[813]: sinh 0 -> 0

Lean proof: included

(case sp-acj4-813-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[813]: sinh 0  ->  0")
  (ask (= (sinh 0) 0))
  (expect true)
  (lean-proof "simp"))

sp-acj4-816-ground

Given

nothing

Claim

$\displaystyle \tanh 0 = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[816]: tanh 0 -> 0

Lean proof: included

(case sp-acj4-816-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[816]: tanh 0  ->  0")
  (ask (= (tanh 0) 0))
  (expect true)
  (lean-proof "simp"))

Case set `ee702ae2fe06`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
sp-acj4-0-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-115-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-116-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-130-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-151-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-154-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-156-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-180-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-183-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-189-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-190-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-191-real true	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-203-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-229-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-234-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-241-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-247-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-260-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-261-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
sp-acj4-266-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-267-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-29-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-3-real true	no verdict	no verdict	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓
sp-acj4-343-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-344-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-378-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-380-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-392-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-403-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-410-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-416-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-420-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-430-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-433-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-442-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-449-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
sp-acj4-450-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-451-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-50-real true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-55-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-56-real contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
sp-acj4-6-real true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-806-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-813-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-816-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓

sp-acj4-0-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \operatorname{arcosh}\left(\cosh x\right) = \left|x\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[0]: acosh cosh _0 -> abs _0

Lean proof: included

(case sp-acj4-0-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[0]: acosh cosh _0  ->  abs _0")
  (var x real)
  (ask (= (acosh (cosh x)) (abs x)))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.cosh_ofReal, AE.acosh_ofReal (Real.one_le_cosh r), AE.abs_ofReal, ← Real.cosh_abs, Real.arcosh_cosh (abs_nonneg r)]"))

sp-acj4-115-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x > 0,\quad \operatorname{surd}\left(x, -4\right) \neq 0$

Claim

$\displaystyle \frac{\log x}{-4} = \log\left(\operatorname{surd}\left(x, -4\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[115]: / log _0 (-4) -> log rootn _0 (-4)

Lean proof: included

(case sp-acj4-115-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[115]: / log _0 (-4)  ->  log rootn _0 (-4)")
  (var x real)
  (assume (nonzero x))
  (assume (> x 0))
  (assume (nonzero (surd x -4)))
  (ask (= (/ (log x) -4) (log (surd x -4))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : 0 < r := (by simpa using h1.2); refine ⟨⟨h0.2, h2.1.1, h2.2⟩, ?_⟩; rw [show (-4:ℂ) = ((-4:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg hr.le (by norm_num), AE.log_ofReal hr.le, AE.log_ofReal (by positivity), Real.log_rpow hr]; simp; ring"))

sp-acj4-116-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x > 0,\quad \operatorname{surd}\left(x, -6\right) \neq 0$

Claim

$\displaystyle \frac{\log x}{-6} = \log\left(\operatorname{surd}\left(x, -6\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[116]: / log _0 (-6) -> log rootn _0 (-6)

Lean proof: included

(case sp-acj4-116-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[116]: / log _0 (-6)  ->  log rootn _0 (-6)")
  (var x real)
  (assume (nonzero x))
  (assume (> x 0))
  (assume (nonzero (surd x -6)))
  (ask (= (/ (log x) -6) (log (surd x -6))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : 0 < r := (by simpa using h1.2); refine ⟨⟨h0.2, h2.1.1, h2.2⟩, ?_⟩; rw [show (-6:ℂ) = ((-6:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg hr.le (by norm_num), AE.log_ofReal hr.le, AE.log_ofReal (by positivity), Real.log_rpow hr]; simp; ring"))

sp-acj4-130-real

Given

$x \in \mathbb{R},\quad \cos x \neq 0,\quad \frac{1}{\cos x} \neq 0$

Claim

$\displaystyle \left|\log\left(\cos x\right)\right| \overset{?}{=} \log\left(\frac{1}{\cos x}\right)$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[130]: abs log cos _0 -> log inv cos _0

Lean proof: included

(case sp-acj4-130-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[130]: abs log cos _0  ->  log inv cos _0")
  (var x real)
  (assume (nonzero (cos x)))
  (assume (nonzero (/ (cos x))))
  (ask (= (abs (log (cos x))) (log (/ (cos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f130w2 | exact AE.w2_cos_two_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_ccos_two_ne]")))

sp-acj4-151-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\cos\left(\arcsin x\right)\right) \overset{?}{=} \left|\arcsin x\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[151]: acos cos asin _0 -> abs asin _0

Lean proof: included

(case sp-acj4-151-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[151]: acos cos asin _0  ->  abs asin _0")
  (var x real)
  (ask (= (acos (cos (asin x))) (abs (asin x))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f151w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-154-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\cos\left(\sin x\right)\right) = \left|\sin x\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[154]: acos cos sin _0 -> abs sin _0

Lean proof: included

(case sp-acj4-154-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[154]: acos cos sin _0  ->  abs sin _0")
  (var x real)
  (ask (= (acos (cos (sin x))) (abs (sin x))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.sin_ofReal, AE.cos_ofReal, AE.acos_ofReal (Real.neg_one_le_cos _) (Real.cos_le_one _), AE.abs_ofReal, ← Real.cos_abs, Real.arccos_cos (abs_nonneg _) (by linarith [abs_le.mpr ⟨Real.neg_one_le_sin r, Real.sin_le_one r⟩, Real.pi_gt_three])]"))

sp-acj4-156-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \arccos\left(\sin\left(\arccos x\right)\right) \overset{?}{=} \left|\arcsin x\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[156]: acos sin acos _0 -> abs asin _0

Lean proof: included

(case sp-acj4-156-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[156]: acos sin acos _0  ->  abs asin _0")
  (var x real)
  (ask (= (acos (sin (acos x))) (abs (asin x))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f156w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-180-real

Given

Claim

$\displaystyle \arctan\left(\sinh\left(\operatorname{arcosh}\left(x\right)\right)\right) \overset{?}{=} \arcsin\left(\tanh\left(\operatorname{arcosh}\left(x\right)\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[180]: atan sinh acosh _0 -> asin tanh acosh _0

Lean proof: included

(case sp-acj4-180-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[180]: atan sinh acosh _0  ->  asin tanh acosh _0")
  (var x real)
  (assume (!= (sinh (acosh x)) i))
  (assume (!= (sinh (acosh x)) (- i)))
  (assume (nonzero (cosh (acosh x))))
  (ask (= (atan (sinh (acosh x))) (asin (tanh (acosh x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f180w2 | exact AE.w2_f180_hI | exact AE.w2_f180_hnI | exact AE.w2_f180_atanD | exact AE.w2_f180_cosh | exact AE.w2_f180_tanhD | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-183-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \sinh\left(\log x\right) \neq i,\quad \sinh\left(\log x\right) \neq -i,\quad \cosh\left(\log x\right) \neq 0$

Claim

$\displaystyle \arctan\left(\sinh\left(\log x\right)\right) \overset{?}{=} \arcsin\left(\tanh\left(\log x\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[183]: atan sinh log _0 -> asin tanh log _0

Lean proof: included

(case sp-acj4-183-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[183]: atan sinh log _0  ->  asin tanh log _0")
  (var x real)
  (assume (nonzero x))
  (assume (!= (sinh (log x)) i))
  (assume (!= (sinh (log x)) (- i)))
  (assume (nonzero (cosh (log x))))
  (ask (= (atan (sinh (log x))) (asin (tanh (log x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f183w2 | exact AE.w2_f183_hI | exact AE.w2_f183_hnI | exact AE.w2_f183_atanD | exact AE.w2_f183_cosh | exact AE.w2_f183_tanhD | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-189-real

Given

$x \in \mathbb{R},\quad \cos\left(\arcsin x\right) \neq 1,\quad \cos\left(\arcsin x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\cos\left(\arcsin x\right)\right) = \operatorname{arcosh}\left(\left|\frac{1}{x}\right|\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[189]: atanh cos asin _0 -> acosh abs inv _0

Lean proof: included

(case sp-acj4-189-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[189]: atanh cos asin _0  ->  acosh abs inv _0")
  (var x real)
  (assume (!= (cos (asin x)) 1))
  (assume (!= (cos (asin x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (cos (asin x))) (acosh (abs (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); refine ⟨⟨⟨⟨by simp, by simp⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.cos_eq, AE.cos_asin]; exact AE.atanh_sqrt_eq_acosh hr"))

sp-acj4-190-real

Given

$x \in \mathbb{R},\quad \cos\left(\arctan x\right) \neq 1,\quad \cos\left(\arctan x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\cos\left(\arctan x\right)\right) = \left|\operatorname{arsinh}\left(\frac{1}{x}\right)\right|$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[190]: atanh cos atan _0 -> abs asinh inv _0

Lean proof: included

(case sp-acj4-190-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[190]: atanh cos atan _0  ->  abs asinh inv _0")
  (var x real)
  (assume (!= (cos (atan x)) 1))
  (assume (!= (cos (atan x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (cos (atan x))) (abs (asinh (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); have hS : 1 < Real.sqrt (1 + r ^ 2) := (Real.lt_sqrt zero_le_one).2 (by have := pow_pos (abs_pos.2 hr) 2; rw [sq_abs] at this; linarith); have hS0 : 0 < Real.sqrt (1 + r ^ 2) := (by linarith); refine ⟨⟨⟨⟨AE.atan.D_ofReal r, trivial⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.atan_ofReal, AE.cos_ofReal, Real.cos_arctan, AE.atanh_ofReal (by have := one_div_pos.2 hS0; linarith) ((div_lt_one hS0).2 hS), AE.inv_ofReal, AE.asinh_ofReal, AE.abs_ofReal, AE.artanh_eq_abs_arsinh hr]"))

sp-acj4-191-real

Given

$x \in \mathbb{R},\quad \sin\left(\arccos x\right) \neq 1,\quad \sin\left(\arccos x\right) \neq -1,\quad x \neq 0$

Claim

$\displaystyle \operatorname{artanh}\left(\sin\left(\arccos x\right)\right) = \operatorname{arcosh}\left(\left|\frac{1}{x}\right|\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[191]: atanh sin acos _0 -> acosh abs inv _0

Lean proof: included

(case sp-acj4-191-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[191]: atanh sin acos _0  ->  acosh abs inv _0")
  (var x real)
  (assume (!= (sin (acos x)) 1))
  (assume (!= (sin (acos x)) -1))
  (assume (nonzero x))
  (ask (= (atanh (sin (acos x))) (acosh (abs (/ x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : r ≠ 0 := (by simpa using h2.2); refine ⟨⟨⟨⟨by simp, by simp⟩, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ⟨h2.2, by simp⟩, by simp⟩, ?_⟩; rw [AE.sin_eq, AE.sin_acos]; exact AE.atanh_sqrt_eq_acosh hr"))

sp-acj4-203-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle \cos\left(\log\left(\frac{1}{x}\right)\right) \overset{?}{=} \cos\left(\log x\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[203]: cos log inv _0 -> cos log _0

Lean proof: included

(case sp-acj4-203-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[203]: cos log inv _0  ->  cos log _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (cos (log (/ x))) (cos (log x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f203w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-229-real

Given

$x \in \mathbb{R},\quad \pi^{x} \neq 0$

Claim

$\displaystyle \frac{1}{\pi^{x}} = \frac{1}{\pi}^{x}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[229]: inv pow np.pi _0 -> pow inv np.pi _0

Lean proof: included

(case sp-acj4-229-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[229]: inv pow np.pi _0  ->  pow inv np.pi _0")
  (var x real)
  (assume (nonzero (pow pi x)))
  (ask (= (/ (pow pi x)) (pow (/ pi) x)))
  (expect true)
  (lean-proof "refine ⟨by simp_all [Real.pi_ne_zero], ?_⟩; simp only [AE.pi_def, AE.inv_def]; exact AE.inv_pow_base Real.pi_pos x"))

sp-acj4-234-real

Given

$x \in \mathbb{R},\quad x \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x^{x} \neq 0,\quad x \neq 0,\quad \frac{1}{x} \neq 0 \lor \operatorname{Re}\left(x\right) > 0$

Claim

$\displaystyle \frac{1}{x^{x}} \overset{?}{=} \frac{1}{x}^{x}$

Expected

contingent true at $x = 1$; false at $x = -\frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -\frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[234]: inv pow _0 _0 -> pow inv _0 _0

Lean proof: included

(case sp-acj4-234-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[234]: inv pow _0 _0  ->  pow inv _0 _0")
  (var x real)
  (assume (or (nonzero x) (> (re x) 0)))
  (assume (nonzero (pow x x)))
  (assume (nonzero x))
  (assume (or (nonzero (/ x)) (> (re x) 0)))
  (ask (= (/ (pow x x)) (pow (/ x) x)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f234w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-241-real

Given

$x \in \mathbb{R},\quad \operatorname{surd}\left(x, 3\right) \neq 0,\quad x \neq 0$

Claim

$\displaystyle \log\left(\operatorname{surd}\left(x, 3\right)\right) \overset{?}{=} \frac{\log x}{3}$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[241]: log rootn _0 3 -> / log _0 3

Lean proof: included

(case sp-acj4-241-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[241]: log rootn _0 3  ->  / log _0 3")
  (var x real)
  (assume (nonzero (surd x 3)))
  (assume (nonzero x))
  (ask (= (log (surd x 3)) (/ (log x) 3)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f241w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-247-real

Given

$x \in \mathbb{R},\quad \operatorname{surd}\left(x, 9\right) \neq 0,\quad x \neq 0$

Claim

$\displaystyle \log\left(\operatorname{surd}\left(x, 9\right)\right) \overset{?}{=} \frac{\log x}{9}$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[247]: log rootn _0 9 -> / log _0 9

Lean proof: included

(case sp-acj4-247-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[247]: log rootn _0 9  ->  / log _0 9")
  (var x real)
  (assume (nonzero (surd x 9)))
  (assume (nonzero x))
  (ask (= (log (surd x 9)) (/ (log x) 9)))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f247w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-260-real

Given

$x \in \mathbb{R},\quad \cos x \neq 0,\quad \frac{1}{\cos x} \neq 0$

Claim

$\displaystyle -\log\left(\cos x\right) \overset{?}{=} \log\left(\frac{1}{\cos x}\right)$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[260]: neg log cos _0 -> log inv cos _0

Lean proof: included

(case sp-acj4-260-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[260]: neg log cos _0  ->  log inv cos _0")
  (var x real)
  (assume (nonzero (cos x)))
  (assume (nonzero (/ (cos x))))
  (ask (= (- (log (cos x))) (log (/ (cos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f260w2 | exact AE.w2_cos_two_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_ccos_two_ne]")))

sp-acj4-261-real

Given

$x \in \mathbb{R},\quad \cosh x \neq 0,\quad \frac{1}{\cosh x} \neq 0$

Claim

$\displaystyle -\log\left(\cosh x\right) = \log\left(\frac{1}{\cosh x}\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[261]: neg log cosh _0 -> log inv cosh _0

Lean proof: included

(case sp-acj4-261-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[261]: neg log cosh _0  ->  log inv cosh _0")
  (var x real)
  (assume (nonzero (cosh x)))
  (assume (nonzero (/ (cosh x))))
  (ask (= (- (log (cosh x))) (log (/ (cosh x)))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨h1.1.1, h1.1.1, h1.2⟩, ?_⟩; rw [AE.cosh_ofReal, AE.inv_ofReal, AE.log_ofReal (Real.cosh_pos r).le, AE.log_ofReal (inv_nonneg.2 (Real.cosh_pos r).le), Real.log_inv]; push_cast; ring"))

sp-acj4-266-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle -\sin\left(\log x\right) \overset{?}{=} \sin\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[266]: neg sin log _0 -> sin log inv _0

Lean proof: included

(case sp-acj4-266-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[266]: neg sin log _0  ->  sin log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (- (sin (log x))) (sin (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f266w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-267-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cos\left(\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cos\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle -\tan\left(\log x\right) \overset{?}{=} \tan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[267]: neg tan log _0 -> tan log inv _0

Lean proof: included

(case sp-acj4-267-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[267]: neg tan log _0  ->  tan log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cos (log x))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cos (log (/ x)))))
  (ask (= (- (tan (log x))) (tan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f267w2 | exact AE.w2_cos_log_neg_one | exact AE.w2_cos_log_inv_neg_one | exact AE.w2_tanD_log_neg_one | exact AE.w2_tanD_log_inv_neg_one | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-29-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x^{3} \neq 0$

Claim

$\displaystyle 3 \, \log x \overset{?}{=} \log\left(x^{3}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[29]: * 3 log _0 -> log pow _0 3

Lean proof: included

(case sp-acj4-29-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[29]: * 3 log _0  ->  log pow _0 3")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (pow x 3)))
  (ask (= (* 3 (log x)) (log (pow x 3))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f29w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-3-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \operatorname{arsinh}\left(\sinh x\right) = x$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[3]: asinh sinh _0 -> _0

Lean proof: included

(case sp-acj4-3-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[3]: asinh sinh _0  ->  _0")
  (var x real)
  (ask (= (asinh (sinh x)) x))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.sinh_ofReal, AE.asinh_ofReal, Real.arsinh_sinh]"))

sp-acj4-343-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \frac{1}{\pi}^{x} = \pi^{-x}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[343]: pow inv np.pi _0 -> pow np.pi neg _0

Lean proof: included

(case sp-acj4-343-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[343]: pow inv np.pi _0  ->  pow np.pi neg _0")
  (var x real)
  (ask (= (pow (/ pi) x) (pow pi (- x))))
  (expect true)
  (lean-proof "refine ⟨by simp [Real.pi_ne_zero], ?_⟩; simp only [AE.pi_def, AE.inv_def]; exact AE.pow_inv_base Real.pi_pos x"))

sp-acj4-344-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x \neq 0 \lor \operatorname{Re}\left(-x\right) > 0$

Claim

$\displaystyle \frac{1}{x}^{x} \overset{?}{=} x^{-x}$

Expected

contingent true at $x = 1$; false at $x = -\frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -\frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[344]: pow inv _0 _0 -> pow _0 neg _0

Lean proof: included

(case sp-acj4-344-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[344]: pow inv _0 _0  ->  pow _0 neg _0")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero (/ x)) (> (re x) 0)))
  (assume (or (nonzero x) (> (re (- x)) 0)))
  (ask (= (pow (/ x) x) (pow x (- x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f344w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-378-real

Given

$x \in \mathbb{R},\quad e^{x} \neq 0$

Claim

$\displaystyle \operatorname{surd}\left(e^{x}, -5\right) = e^{\frac{x}{-5}}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[378]: rootn exp _0 (-5) -> exp / _0 (-5)

Lean proof: included

(case sp-acj4-378-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[378]: rootn exp _0 (-5)  ->  exp / _0 (-5)")
  (var x real)
  (assume (nonzero (exp x)))
  (ask (= (surd (exp x) -5) (exp (/ x -5))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨(AE.surd.D_iff _ _).2 ⟨by simp [AE.exp_ofReal], (⟨-5, by norm_num⟩ : ∃ n : ℤ, (-5:ℂ) = n), by norm_num, Or.inl (by rw [AE.exp_ofReal, Complex.ofReal_re]; exact (Real.exp_pos r).le), Or.inl h0.2⟩, ?_⟩; rw [AE.exp_ofReal, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg (Real.exp_pos r).le (by norm_num), ← Real.exp_mul, show (r:ℂ) * AE.inv ((-5:ℤ):ℂ) = ((r * ((-5:ℤ):ℝ)⁻¹ : ℝ) : ℂ) by push_cast; simp, AE.exp_ofReal]"))

sp-acj4-380-real

Given

$x \in \mathbb{R},\quad e^{x} \neq 0$

Claim

$\displaystyle \operatorname{surd}\left(e^{x}, -7\right) = e^{\frac{x}{-7}}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[380]: rootn exp _0 (-7) -> exp / _0 (-7)

Lean proof: included

(case sp-acj4-380-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[380]: rootn exp _0 (-7)  ->  exp / _0 (-7)")
  (var x real)
  (assume (nonzero (exp x)))
  (ask (= (surd (exp x) -7) (exp (/ x -7))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨(AE.surd.D_iff _ _).2 ⟨by simp [AE.exp_ofReal], (⟨-7, by norm_num⟩ : ∃ n : ℤ, (-7:ℂ) = n), by norm_num, Or.inl (by rw [AE.exp_ofReal, Complex.ofReal_re]; exact (Real.exp_pos r).le), Or.inl h0.2⟩, ?_⟩; rw [AE.exp_ofReal, show (-7:ℂ) = ((-7:ℤ):ℂ) by norm_num, AE.surd_ofReal_nonneg (Real.exp_pos r).le (by norm_num), ← Real.exp_mul, show (r:ℂ) * AE.inv ((-7:ℤ):ℂ) = ((r * ((-7:ℤ):ℝ)⁻¹ : ℝ) : ℂ) by push_cast; simp, AE.exp_ofReal]"))

sp-acj4-392-real

Given

$x \in \mathbb{R}$

Claim

$\displaystyle \sin\left(\left|\arcsin x\right|\right) \overset{?}{=} \left|\cos\left(\arccos x\right)\right|$

Expected

contingent true at $x = 0$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 0$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[392]: sin abs asin _0 -> abs cos acos _0

Lean proof: included

(case sp-acj4-392-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[392]: sin abs asin _0  ->  abs cos acos _0")
  (var x real)
  (ask (= (sin (abs (asin x))) (abs (cos (acos x)))))
  (expect contingent)
  (witness true (x 0) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f392w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-403-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \frac{1}{x} \neq 0$

Claim

$\displaystyle \sin\left(-\log x\right) \overset{?}{=} \sin\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[403]: sin neg log _0 -> sin log inv _0

Lean proof: included

(case sp-acj4-403-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[403]: sin neg log _0  ->  sin log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (/ x)))
  (ask (= (sin (- (log x))) (sin (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f403w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-410-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \sinh x \neq 0$

Claim

$\displaystyle \sinh\left(e^{\log x}\right) = e^{\log\left(\sinh x\right)}$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[410]: sinh exp log _0 -> exp log sinh _0

Lean proof: included

(case sp-acj4-410-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[410]: sinh exp log _0  ->  exp log sinh _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (sinh x)))
  (ask (= (sinh (exp (log x))) (exp (log (sinh x)))))
  (expect true)
  (lean-proof "have hs : Complex.sinh x ≠ 0 := (by simpa using h1.2); refine ⟨⟨⟨h0.2, trivial⟩, trivial, h1.2⟩, ?_⟩; simp only [AE.exp_def, AE.log_def, AE.sinh_eq]; rw [Complex.exp_log h0.2, Complex.exp_log hs]"))

sp-acj4-416-real

Given

$x \in \mathbb{R},\quad \cos\left(\arccos\left(\left|x\right|\right)\right) \neq 0,\quad \cos\left(\arccos x\right) \neq 0$

Claim

$\displaystyle \tan\left(\arccos\left(\left|x\right|\right)\right) \overset{?}{=} \left|\tan\left(\arccos x\right)\right|$

Expected

contingent true at $x = 1$; false at $x = 2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = 2$

SimpliPy acj-4 (MIT) rules_real.json[416]: tan acos abs _0 -> abs tan acos _0

Lean proof: included

(case sp-acj4-416-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[416]: tan acos abs _0  ->  abs tan acos _0")
  (var x real)
  (assume (nonzero (cos (acos (abs x)))))
  (assume (nonzero (cos (acos x))))
  (ask (= (tan (acos (abs x))) (abs (tan (acos x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f416w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos, AE.w2_cos_acos]")))

sp-acj4-420-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cos\left(-\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cos\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle \tan\left(-\log x\right) \overset{?}{=} \tan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[420]: tan neg log _0 -> tan log inv _0

Lean proof: included

(case sp-acj4-420-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[420]: tan neg log _0  ->  tan log inv _0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cos (- (log x)))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cos (log (/ x)))))
  (ask (= (tan (- (log x))) (tan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f420w2 | exact AE.w2_cos_neg_log_neg_one | exact AE.w2_cos_log_inv_neg_one | exact AE.w2_tanD_neg_log_neg_one | exact AE.w2_tanD_log_inv_neg_one | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-430-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(x\right) > 0,\quad x^{x} \neq 0$

Claim

$\displaystyle \log x \, x \overset{?}{=} \log\left(x^{x}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[430]: * log ?0 ?0 -> log pow ?0 ?0

Lean proof: included

(case sp-acj4-430-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[430]: * log ?0 ?0  ->  log pow ?0 ?0")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re x) 0)))
  (assume (nonzero (pow x x)))
  (ask (= (* (log x) x) (log (pow x x))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f430w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-433-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad -\log x \neq i,\quad -\log x \neq -i,\quad \frac{1}{x} \neq 0,\quad \log\left(\frac{1}{x}\right) \neq i,\quad \log\left(\frac{1}{x}\right) \neq -i$

Claim

$\displaystyle \arctan\left(-\log x\right) \overset{?}{=} \arctan\left(\log\left(\frac{1}{x}\right)\right)$

Expected

contingent true at $x = 1$; false at $x = -2$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -2$

SimpliPy acj-4 (MIT) rules_real.json[433]: atan neg log !0 -> atan log inv !0

Lean proof: included

(case sp-acj4-433-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[433]: atan neg log !0  ->  atan log inv !0")
  (var x real)
  (assume (nonzero x))
  (assume (!= (- (log x)) i))
  (assume (!= (- (log x)) (- i)))
  (assume (nonzero (/ x)))
  (assume (!= (log (/ x)) i))
  (assume (!= (log (/ x)) (- i)))
  (ask (= (atan (- (log x))) (atan (log (/ x)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f433w2 | exact AE.w2_f433_h2 | exact AE.w2_f433_h3 | exact AE.w2_f433_h5 | exact AE.w2_f433_h6 | exact AE.w2_f433_atanD1 | exact AE.w2_f433_atanD2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-442-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \log x \neq 0,\quad \frac{1}{\log x} \neq 0$

Claim

$\displaystyle -\log\left(\log x\right) \overset{?}{=} \log\left(\frac{1}{\log x}\right)$

Expected

contingent true at $x = -1$; false at $x = \frac{1}{2}$

equal at some admissible points, different at others

witness (true): $x = -1$

witness (false): $x = \frac{1}{2}$

SimpliPy acj-4 (MIT) rules_real.json[442]: neg log log ?0 -> log inv log ?0

Lean proof: included

(case sp-acj4-442-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[442]: neg log log ?0  ->  log inv log ?0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (log x)))
  (assume (nonzero (/ (log x))))
  (ask (= (- (log (log x))) (log (/ (log x)))))
  (expect contingent)
  (witness true (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f442w1 | exact AE.w2_log_neg_one_ne | exact AE.w2_inv_log_neg_one_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x 1/2) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f442w2 | exact AE.w2_log_half_ne | exact AE.w2_inv_log_half_ne | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-449-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad \cosh\left(-\log x\right) \neq 0,\quad \frac{1}{x} \neq 0,\quad \cosh\left(\log\left(\frac{1}{x}\right)\right) \neq 0$

Claim

$\displaystyle \tanh\left(-\log x\right) = \tanh\left(\log\left(\frac{1}{x}\right)\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[449]: tanh neg log !0 -> tanh log inv !0

Lean proof: included

(case sp-acj4-449-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[449]: tanh neg log !0  ->  tanh log inv !0")
  (var x real)
  (assume (nonzero x))
  (assume (nonzero (cosh (- (log x)))))
  (assume (nonzero (/ x)))
  (assume (nonzero (cosh (log (/ x)))))
  (ask (= (tanh (- (log x))) (tanh (log (/ x)))))
  (expect true)
  (lean-proof "refine ⟨⟨⟨h0.2, (AE.tanh.D_iff _).2 (by simpa using h1.2)⟩, ⟨h0.2, h2.2⟩, (AE.tanh.D_iff _).2 (by simpa using h3.2)⟩, ?_⟩; simp only [AE.tanh_eq, AE.log_def, AE.inv_def]; exact AE.tanh_neg_log x h0.2"))

sp-acj4-450-real

Given

$x \in \mathbb{R},\quad x \neq 0$

Claim

$\displaystyle \frac{x}{x} = 1$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[450]: / $0 $0 -> 1

Lean proof: included

(case sp-acj4-450-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[450]: / $0 $0  ->  1")
  (var x real)
  (assume (nonzero x))
  (ask (= (/ x x) 1))
  (expect true)
  (lean-proof "simp_all"))

sp-acj4-451-real

Given

$x \in \mathbb{R},\quad x \neq 0$

Claim

$\displaystyle \frac{0}{x} = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[451]: / 0 $0 -> 0

Lean proof: included

(case sp-acj4-451-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[451]: / 0 $0  ->  0")
  (var x real)
  (assume (nonzero x))
  (ask (= (/ 0 x) 0))
  (expect true)
  (lean-proof "simp_all"))

sp-acj4-50-real

Given

$x \in \mathbb{R},\quad 6^{x} \neq 0$

Claim

$\displaystyle \log 6 \, x = \log\left(6^{x}\right)$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[50]: * log 6 _0 -> log pow 6 _0

Lean proof: included

(case sp-acj4-50-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[50]: * log 6 _0  ->  log pow 6 _0")
  (var x real)
  (assume (nonzero (pow 6 x)))
  (ask (= (* (log 6) x) (log (pow 6 x))))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨by norm_num, h0.1.1, h0.2⟩, ?_⟩; rw [show (6:ℂ) = ((6:ℝ):ℂ) by norm_num, AE.pow_ofReal (by norm_num) (Or.inl (by norm_num)), AE.log_ofReal (Real.rpow_nonneg (by norm_num) _), AE.log_ofReal (by norm_num), Real.log_rpow (by norm_num)]; push_cast; ring"))

sp-acj4-55-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(e^{1}\right) > 0,\quad x^{e^{1}} \neq 0$

Claim

$\displaystyle \log x \, e^{1} \overset{?}{=} \log\left(x^{e^{1}}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[55]: * log _0 np.e -> log pow _0 np.e

Lean proof: included

(case sp-acj4-55-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[55]: * log _0 np.e  ->  log pow _0 np.e")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re (exp 1)) 0)))
  (assume (nonzero (pow x (exp 1))))
  (ask (= (* (log x) (exp 1)) (log (pow x (exp 1)))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f55w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-56-real

Given

$x \in \mathbb{R},\quad x \neq 0,\quad x \neq 0 \lor \operatorname{Re}\left(\pi\right) > 0,\quad x^{\pi} \neq 0$

Claim

$\displaystyle \log x \, \pi \overset{?}{=} \log\left(x^{\pi}\right)$

Expected

contingent true at $x = 1$; false at $x = -1$

equal at some admissible points, different at others

witness (true): $x = 1$

witness (false): $x = -1$

SimpliPy acj-4 (MIT) rules_real.json[56]: * log _0 np.pi -> log pow _0 np.pi

Lean proof: included

(case sp-acj4-56-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[56]: * log _0 np.pi  ->  log pow _0 np.pi")
  (var x real)
  (assume (nonzero x))
  (assume (or (nonzero x) (> (re pi) 0)))
  (assume (nonzero (pow x pi)))
  (ask (= (* (log x) pi) (log (pow x pi))))
  (expect contingent)
  (witness true (x 1) (lean-proof "norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]"))
  (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_f56w2 | norm_num [AE.abs_eq, AE.pow, AE.w2_asin_zero, AE.w2_asin_one, AE.w2_acos_zero, AE.w2_acos_one, AE.w2_atan_zero, AE.w2_atanh_zero, AE.w2_asinh_zero, AE.w2_acosh_one, AE.surd, AE.w2_zero_ne_I, AE.w2_isInt_three, AE.w2_isInt_five, AE.w2_isInt_nine, AE.w2_isInt_neg_five, AE.w2_odd_three, AE.w2_odd_five, AE.w2_odd_nine, AE.w2_odd_neg_five, Real.pi_pos, Complex.exp_re, Real.exp_pos]")))

sp-acj4-6-real

Given

$x \in \mathbb{R},\quad \tanh x \neq 1,\quad \tanh x \neq -1$

Claim

$\displaystyle \operatorname{artanh}\left(\tanh x\right) = x$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[6]: atanh tanh !0 -> !0

Lean proof: included

(case sp-acj4-6-real (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[6]: atanh tanh !0  ->  !0")
  (var x real)
  (assume (!= (tanh x) 1))
  (assume (!= (tanh x) -1))
  (ask (= (atanh (tanh x)) x))
  (expect true)
  (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨h0.1, (AE.atanh.D_iff _).2 ⟨h0.2, h1.2⟩⟩, ?_⟩; rw [AE.tanh_ofReal, AE.atanh_ofReal (Real.neg_one_lt_tanh r) (Real.tanh_lt_one r), Real.artanh_tanh]"))

sp-acj4-806-ground

Given

nothing

Claim

$\displaystyle \cosh 0 = 1$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[806]: cosh 0 -> 1

Lean proof: included

(case sp-acj4-806-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[806]: cosh 0  ->  1")
  (ask (= (cosh 0) 1))
  (expect true)
  (lean-proof "simp"))

sp-acj4-813-ground

Given

nothing

Claim

$\displaystyle \sinh 0 = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[813]: sinh 0 -> 0

Lean proof: included

(case sp-acj4-813-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[813]: sinh 0  ->  0")
  (ask (= (sinh 0) 0))
  (expect true)
  (lean-proof "simp"))

sp-acj4-816-ground

Given

nothing

Claim

$\displaystyle \tanh 0 = 0$

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[816]: tanh 0 -> 0

Lean proof: included

(case sp-acj4-816-ground (category simplipy-f64-edge)
  (note "SimpliPy acj-4 (MIT) rules_real.json[816]: tanh 0  ->  0")
  (ask (= (tanh 0) 0))
  (expect true)
  (lean-proof "simp"))

simplipy-f64-edge

Case set ba9dc4def822

Case set 3ba0dfac4bca

Case set ee702ae2fe06

Case set `ba9dc4def822`

Case set `3ba0dfac4bca`

Case set `ee702ae2fe06`