simplipy-ground

Exact variable-free identities found in both rule files (constant folding).

Case set `ba9dc4def822`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
sp-acj4-1007-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1107-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1148-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1149-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1177-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1195-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1217-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1238-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1247-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1254-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1258-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5372-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5382-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5385-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-819-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-837-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-848-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-868-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-911-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-927-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓

sp-acj4-1007-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\sin 5} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1007] + rules.json[700]: / 0 sin 5 -> 0

Lean proof: included

(case sp-acj4-1007-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1007] + rules.json[700]: / 0 sin 5  ->  0")
  (ask (= (/ 0 (sin 5)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (5:ℂ) = ((5:ℝ):ℂ) by norm_num, AE.sin_ofReal]; have h : Real.sin 5 < 0 := by { rw [← Real.sin_sub_two_pi]; exact Real.sin_neg_of_neg_of_neg_pi_lt (by linarith [Real.pi_gt_three]) (by linarith [Real.pi_lt_d2]) }; exact_mod_cast h.ne"))

sp-acj4-1107-ground

Given

nothing

Claim

\(\displaystyle \arcsin\left(\sin\left(\frac{1}{10}\right)\right) = \frac{1}{10}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1107] + rules.json[800]: asin sin inv 10 -> 0.1

Lean proof: included

(case sp-acj4-1107-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1107] + rules.json[800]: asin sin inv 10  ->  0.1")
  (ask (= (asin (sin (/ 10))) 1/10))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [show AE.inv (10:ℂ) = ((1/10:ℝ):ℂ) by push_cast; simp, AE.sin_ofReal, AE.asin_ofReal (Real.neg_one_le_sin _) (Real.sin_le_one _), Real.arcsin_sin (by linarith [Real.pi_gt_three]) (by linarith [Real.pi_gt_three])]; push_cast; ring"))

sp-acj4-1148-ground

Given

nothing

Claim

\(\displaystyle \cosh\left(\log\left(\frac{1}{4}\right)\right) = \frac{17}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1148] + rules.json[838]: cosh log inv 4 -> 2.125

Lean proof: included

(case sp-acj4-1148-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1148] + rules.json[838]: cosh log inv 4  ->  2.125")
  (ask (= (cosh (log (/ 4))) 17/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.cosh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-1149-ground

Given

nothing

Claim

\(\displaystyle e^{\left|\log 2\right|} = 2\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1149] + rules.json[840]: exp abs log 2 -> 2

Lean proof: included

(case sp-acj4-1149-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1149] + rules.json[840]: exp abs log 2  ->  2")
  (ask (= (exp (abs (log 2))) 2))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [AE.abs_eq, show (2:ℂ) = ((2:ℝ):ℂ) by norm_num, AE.log_ofReal (by norm_num), Complex.norm_real, Real.norm_eq_abs, abs_of_pos (Real.log_pos (by norm_num))]; simp; exact Complex.exp_log (by norm_num)"))

sp-acj4-1177-ground

Given

nothing

Claim

\(\displaystyle 0^{\operatorname{arsinh}\left(10\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1177] + rules.json[913]: pow 0 asinh 10 -> 0

Lean proof: included

(case sp-acj4-1177-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1177] + rules.json[913]: pow 0 asinh 10  ->  0")
  (ask (= (pow 0 (asinh 10)) 0))
  (expect true)
  (lean-proof "have h : AE.asinh (10:ℂ) = (Real.arsinh 10 : ℂ) := (by exact_mod_cast AE.asinh_ofReal 10); simp [h, Real.arsinh_pos_iff]"))

sp-acj4-1195-ground

Given

nothing

Claim

\(\displaystyle 0^{\arctan 7} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1195] + rules.json[931]: pow 0 atan 7 -> 0

Lean proof: included

(case sp-acj4-1195-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1195] + rules.json[931]: pow 0 atan 7  ->  0")
  (ask (= (pow 0 (atan 7)) 0))
  (expect true)
  (lean-proof "have h : AE.atan (7:ℂ) = (Real.arctan 7 : ℂ) := (by exact_mod_cast AE.atan_ofReal 7); have hd : AE.atan.D (7:ℂ) := (by exact_mod_cast AE.atan.D_ofReal 7); have hp : 0 < Real.arctan 7 := Real.arctan_pos.mpr (by norm_num); refine ⟨⟨hd, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-1217-ground

Given

nothing

Claim

\(\displaystyle 0^{e^{-1}} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1217] + rules.json[953]: pow 0 exp (-1) -> 0

Lean proof: included

(case sp-acj4-1217-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1217] + rules.json[953]: pow 0 exp (-1)  ->  0")
  (ask (= (pow 0 (exp -1)) 0))
  (expect true)
  (lean-proof "simp [Complex.exp_re, Real.exp_pos]"))

sp-acj4-1238-ground

Given

nothing

Claim

\(\displaystyle 0^{\frac{1}{\pi}} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1238] + rules.json[974]: pow 0 inv np.pi -> 0

Lean proof: included

(case sp-acj4-1238-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1238] + rules.json[974]: pow 0 inv np.pi  ->  0")
  (ask (= (pow 0 (/ pi)) 0))
  (expect true)
  (lean-proof "simp [Real.pi_ne_zero, Complex.inv_re, Complex.normSq_ofReal]; positivity"))

sp-acj4-1247-ground

Given

nothing

Claim

\(\displaystyle 0^{\log 9} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1247] + rules.json[983]: pow 0 log 9 -> 0

Lean proof: included

(case sp-acj4-1247-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1247] + rules.json[983]: pow 0 log 9  ->  0")
  (ask (= (pow 0 (log 9)) 0))
  (expect true)
  (lean-proof "simp [Complex.log_re]; exact Real.log_pos (by norm_num)"))

sp-acj4-1254-ground

Given

nothing

Claim

\(\displaystyle 0^{\sin 2} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1254] + rules.json[990]: pow 0 sin 2 -> 0

Lean proof: included

(case sp-acj4-1254-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1254] + rules.json[990]: pow 0 sin 2  ->  0")
  (ask (= (pow 0 (sin 2)) 0))
  (expect true)
  (lean-proof "have h : AE.sin (2:ℂ) = (Real.sin 2 : ℂ) := (by exact_mod_cast AE.sin_ofReal 2); have hp : 0 < Real.sin 2 := Real.sin_pos_of_pos_of_lt_pi (by norm_num) (by linarith [Real.pi_gt_three]); refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-1258-ground

Given

nothing

Claim

\(\displaystyle 0^{\sin 9} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1258] + rules.json[994]: pow 0 sin 9 -> 0

Lean proof: included

(case sp-acj4-1258-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1258] + rules.json[994]: pow 0 sin 9  ->  0")
  (ask (= (pow 0 (sin 9)) 0))
  (expect true)
  (lean-proof "have h : AE.sin (9:ℂ) = (Real.sin 9 : ℂ) := (by exact_mod_cast AE.sin_ofReal 9); have hp : 0 < Real.sin 9 := (by rw [← Real.sin_sub_two_pi]; exact Real.sin_pos_of_pos_of_lt_pi (by linarith [Real.pi_lt_d2]) (by linarith [Real.pi_gt_three])); refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-5372-ground

Given

nothing

Claim

\(\displaystyle \sin\left(\arcsin\left(\frac{1}{-4}\right)\right) = -\frac{1}{4}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5372] + rules.json[5127]: sin asin inv (-4) -> -0.25

Lean proof: included

(case sp-acj4-5372-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5372] + rules.json[5127]: sin asin inv (-4)  ->  -0.25")
  (ask (= (sin (asin (/ -4))) -1/4))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [show AE.inv (-4:ℂ) = ((-1/4:ℝ):ℂ) by push_cast; simp; ring, AE.asin_ofReal (by norm_num) (by norm_num), AE.sin_ofReal, Real.sin_arcsin (by norm_num) (by norm_num)]; push_cast; ring"))

sp-acj4-5382-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(\log\left(\frac{1}{4}\right)\right) = -\frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5382] + rules.json[5137]: sinh log inv 4 -> -1.875

Lean proof: included

(case sp-acj4-5382-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5382] + rules.json[5137]: sinh log inv 4  ->  -1.875")
  (ask (= (sinh (log (/ 4))) -15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-5385-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(-\log 4\right) = -\frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5385] + rules.json[5140]: sinh neg log 4 -> -1.875

Lean proof: included

(case sp-acj4-5385-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5385] + rules.json[5140]: sinh neg log 4  ->  -1.875")
  (ask (= (sinh (- (log 4))) -15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-819-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\pi} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[819] + rules.json[481]: / 0 np.pi -> 0

Lean proof: included

(case sp-acj4-819-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[819] + rules.json[481]: / 0 np.pi  ->  0")
  (ask (= (/ 0 pi) 0))
  (expect true)
  (lean-proof "simp [Real.pi_ne_zero]"))

sp-acj4-837-ground

Given

nothing

Claim

\(\displaystyle 0^{\pi} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[837] + rules.json[502]: pow 0 np.pi -> 0

Lean proof: included

(case sp-acj4-837-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[837] + rules.json[502]: pow 0 np.pi  ->  0")
  (ask (= (pow 0 pi) 0))
  (expect true)
  (lean-proof "simp [Real.pi_pos]"))

sp-acj4-848-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(\log 4\right) = \frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[848] + rules.json[512]: sinh log 4 -> 1.875

Lean proof: included

(case sp-acj4-848-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[848] + rules.json[512]: sinh log 4  ->  1.875")
  (ask (= (sinh (log 4)) 15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-868-ground

Given

nothing

Claim

\(\displaystyle 0 \, \operatorname{arcosh}\left(7\right) = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[868] + rules.json[561]: * 0 acosh 7 -> 0

Lean proof: included

(case sp-acj4-868-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[868] + rules.json[561]: * 0 acosh 7  ->  0")
  (ask (= (* 0 (acosh 7)) 0))
  (expect true)
  (lean-proof "simp"))

sp-acj4-911-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\arcsin\left(-1\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[911] + rules.json[604]: / 0 asin (-1) -> 0

Lean proof: included

(case sp-acj4-911-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[911] + rules.json[604]: / 0 asin (-1)  ->  0")
  (ask (= (/ 0 (asin -1)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (-1:ℂ) = ((-1:ℝ):ℂ) by push_cast; rfl, AE.asin_ofReal (by norm_num) (by norm_num), Real.arcsin_neg_one]; simp [Real.pi_ne_zero]"))

sp-acj4-927-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\operatorname{arsinh}\left(4\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[927] + rules.json[620]: / 0 asinh 4 -> 0

Lean proof: included

(case sp-acj4-927-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[927] + rules.json[620]: / 0 asinh 4  ->  0")
  (ask (= (/ 0 (asinh 4)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (4:ℂ) = ((4:ℝ):ℂ) by norm_num, AE.asinh_ofReal]; exact_mod_cast (Real.arsinh_pos_iff.mpr (by norm_num)).ne'"))

Case set `3ba0dfac4bca`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
sp-acj4-1007-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1107-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1148-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1149-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1177-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1195-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1217-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1238-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1247-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1254-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1258-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5372-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5382-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5385-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-819-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-837-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-848-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-868-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-911-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-927-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓

sp-acj4-1007-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\sin 5} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1007] + rules.json[700]: / 0 sin 5 -> 0

Lean proof: included

(case sp-acj4-1007-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1007] + rules.json[700]: / 0 sin 5  ->  0")
  (ask (= (/ 0 (sin 5)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (5:ℂ) = ((5:ℝ):ℂ) by norm_num, AE.sin_ofReal]; have h : Real.sin 5 < 0 := by { rw [← Real.sin_sub_two_pi]; exact Real.sin_neg_of_neg_of_neg_pi_lt (by linarith [Real.pi_gt_three]) (by linarith [Real.pi_lt_d2]) }; exact_mod_cast h.ne"))

sp-acj4-1107-ground

Given

nothing

Claim

\(\displaystyle \arcsin\left(\sin\left(\frac{1}{10}\right)\right) = \frac{1}{10}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1107] + rules.json[800]: asin sin inv 10 -> 0.1

Lean proof: included

(case sp-acj4-1107-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1107] + rules.json[800]: asin sin inv 10  ->  0.1")
  (ask (= (asin (sin (/ 10))) 1/10))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [show AE.inv (10:ℂ) = ((1/10:ℝ):ℂ) by push_cast; simp, AE.sin_ofReal, AE.asin_ofReal (Real.neg_one_le_sin _) (Real.sin_le_one _), Real.arcsin_sin (by linarith [Real.pi_gt_three]) (by linarith [Real.pi_gt_three])]; push_cast; ring"))

sp-acj4-1148-ground

Given

nothing

Claim

\(\displaystyle \cosh\left(\log\left(\frac{1}{4}\right)\right) = \frac{17}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1148] + rules.json[838]: cosh log inv 4 -> 2.125

Lean proof: included

(case sp-acj4-1148-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1148] + rules.json[838]: cosh log inv 4  ->  2.125")
  (ask (= (cosh (log (/ 4))) 17/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.cosh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-1149-ground

Given

nothing

Claim

\(\displaystyle e^{\left|\log 2\right|} = 2\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1149] + rules.json[840]: exp abs log 2 -> 2

Lean proof: included

(case sp-acj4-1149-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1149] + rules.json[840]: exp abs log 2  ->  2")
  (ask (= (exp (abs (log 2))) 2))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [AE.abs_eq, show (2:ℂ) = ((2:ℝ):ℂ) by norm_num, AE.log_ofReal (by norm_num), Complex.norm_real, Real.norm_eq_abs, abs_of_pos (Real.log_pos (by norm_num))]; simp; exact Complex.exp_log (by norm_num)"))

sp-acj4-1177-ground

Given

nothing

Claim

\(\displaystyle 0^{\operatorname{arsinh}\left(10\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1177] + rules.json[913]: pow 0 asinh 10 -> 0

Lean proof: included

(case sp-acj4-1177-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1177] + rules.json[913]: pow 0 asinh 10  ->  0")
  (ask (= (pow 0 (asinh 10)) 0))
  (expect true)
  (lean-proof "have h : AE.asinh (10:ℂ) = (Real.arsinh 10 : ℂ) := (by exact_mod_cast AE.asinh_ofReal 10); simp [h, Real.arsinh_pos_iff]"))

sp-acj4-1195-ground

Given

nothing

Claim

\(\displaystyle 0^{\arctan 7} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1195] + rules.json[931]: pow 0 atan 7 -> 0

Lean proof: included

(case sp-acj4-1195-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1195] + rules.json[931]: pow 0 atan 7  ->  0")
  (ask (= (pow 0 (atan 7)) 0))
  (expect true)
  (lean-proof "have h : AE.atan (7:ℂ) = (Real.arctan 7 : ℂ) := (by exact_mod_cast AE.atan_ofReal 7); have hd : AE.atan.D (7:ℂ) := (by exact_mod_cast AE.atan.D_ofReal 7); have hp : 0 < Real.arctan 7 := Real.arctan_pos.mpr (by norm_num); refine ⟨⟨hd, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-1217-ground

Given

nothing

Claim

\(\displaystyle 0^{e^{-1}} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1217] + rules.json[953]: pow 0 exp (-1) -> 0

Lean proof: included

(case sp-acj4-1217-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1217] + rules.json[953]: pow 0 exp (-1)  ->  0")
  (ask (= (pow 0 (exp -1)) 0))
  (expect true)
  (lean-proof "simp [Complex.exp_re, Real.exp_pos]"))

sp-acj4-1238-ground

Given

nothing

Claim

\(\displaystyle 0^{\frac{1}{\pi}} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1238] + rules.json[974]: pow 0 inv np.pi -> 0

Lean proof: included

(case sp-acj4-1238-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1238] + rules.json[974]: pow 0 inv np.pi  ->  0")
  (ask (= (pow 0 (/ pi)) 0))
  (expect true)
  (lean-proof "simp [Real.pi_ne_zero, Complex.inv_re, Complex.normSq_ofReal]; positivity"))

sp-acj4-1247-ground

Given

nothing

Claim

\(\displaystyle 0^{\log 9} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1247] + rules.json[983]: pow 0 log 9 -> 0

Lean proof: included

(case sp-acj4-1247-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1247] + rules.json[983]: pow 0 log 9  ->  0")
  (ask (= (pow 0 (log 9)) 0))
  (expect true)
  (lean-proof "simp [Complex.log_re]; exact Real.log_pos (by norm_num)"))

sp-acj4-1254-ground

Given

nothing

Claim

\(\displaystyle 0^{\sin 2} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1254] + rules.json[990]: pow 0 sin 2 -> 0

Lean proof: included

(case sp-acj4-1254-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1254] + rules.json[990]: pow 0 sin 2  ->  0")
  (ask (= (pow 0 (sin 2)) 0))
  (expect true)
  (lean-proof "have h : AE.sin (2:ℂ) = (Real.sin 2 : ℂ) := (by exact_mod_cast AE.sin_ofReal 2); have hp : 0 < Real.sin 2 := Real.sin_pos_of_pos_of_lt_pi (by norm_num) (by linarith [Real.pi_gt_three]); refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-1258-ground

Given

nothing

Claim

\(\displaystyle 0^{\sin 9} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1258] + rules.json[994]: pow 0 sin 9 -> 0

Lean proof: included

(case sp-acj4-1258-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1258] + rules.json[994]: pow 0 sin 9  ->  0")
  (ask (= (pow 0 (sin 9)) 0))
  (expect true)
  (lean-proof "have h : AE.sin (9:ℂ) = (Real.sin 9 : ℂ) := (by exact_mod_cast AE.sin_ofReal 9); have hp : 0 < Real.sin 9 := (by rw [← Real.sin_sub_two_pi]; exact Real.sin_pos_of_pos_of_lt_pi (by linarith [Real.pi_lt_d2]) (by linarith [Real.pi_gt_three])); refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-5372-ground

Given

nothing

Claim

\(\displaystyle \sin\left(\arcsin\left(\frac{1}{-4}\right)\right) = -\frac{1}{4}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5372] + rules.json[5127]: sin asin inv (-4) -> -0.25

Lean proof: included

(case sp-acj4-5372-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5372] + rules.json[5127]: sin asin inv (-4)  ->  -0.25")
  (ask (= (sin (asin (/ -4))) -1/4))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [show AE.inv (-4:ℂ) = ((-1/4:ℝ):ℂ) by push_cast; simp; ring, AE.asin_ofReal (by norm_num) (by norm_num), AE.sin_ofReal, Real.sin_arcsin (by norm_num) (by norm_num)]; push_cast; ring"))

sp-acj4-5382-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(\log\left(\frac{1}{4}\right)\right) = -\frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5382] + rules.json[5137]: sinh log inv 4 -> -1.875

Lean proof: included

(case sp-acj4-5382-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5382] + rules.json[5137]: sinh log inv 4  ->  -1.875")
  (ask (= (sinh (log (/ 4))) -15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-5385-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(-\log 4\right) = -\frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5385] + rules.json[5140]: sinh neg log 4 -> -1.875

Lean proof: included

(case sp-acj4-5385-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5385] + rules.json[5140]: sinh neg log 4  ->  -1.875")
  (ask (= (sinh (- (log 4))) -15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-819-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\pi} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[819] + rules.json[481]: / 0 np.pi -> 0

Lean proof: included

(case sp-acj4-819-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[819] + rules.json[481]: / 0 np.pi  ->  0")
  (ask (= (/ 0 pi) 0))
  (expect true)
  (lean-proof "simp [Real.pi_ne_zero]"))

sp-acj4-837-ground

Given

nothing

Claim

\(\displaystyle 0^{\pi} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[837] + rules.json[502]: pow 0 np.pi -> 0

Lean proof: included

(case sp-acj4-837-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[837] + rules.json[502]: pow 0 np.pi  ->  0")
  (ask (= (pow 0 pi) 0))
  (expect true)
  (lean-proof "simp [Real.pi_pos]"))

sp-acj4-848-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(\log 4\right) = \frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[848] + rules.json[512]: sinh log 4 -> 1.875

Lean proof: included

(case sp-acj4-848-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[848] + rules.json[512]: sinh log 4  ->  1.875")
  (ask (= (sinh (log 4)) 15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-868-ground

Given

nothing

Claim

\(\displaystyle 0 \, \operatorname{arcosh}\left(7\right) = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[868] + rules.json[561]: * 0 acosh 7 -> 0

Lean proof: included

(case sp-acj4-868-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[868] + rules.json[561]: * 0 acosh 7  ->  0")
  (ask (= (* 0 (acosh 7)) 0))
  (expect true)
  (lean-proof "simp"))

sp-acj4-911-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\arcsin\left(-1\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[911] + rules.json[604]: / 0 asin (-1) -> 0

Lean proof: included

(case sp-acj4-911-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[911] + rules.json[604]: / 0 asin (-1)  ->  0")
  (ask (= (/ 0 (asin -1)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (-1:ℂ) = ((-1:ℝ):ℂ) by push_cast; rfl, AE.asin_ofReal (by norm_num) (by norm_num), Real.arcsin_neg_one]; simp [Real.pi_ne_zero]"))

sp-acj4-927-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\operatorname{arsinh}\left(4\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[927] + rules.json[620]: / 0 asinh 4 -> 0

Lean proof: included

(case sp-acj4-927-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[927] + rules.json[620]: / 0 asinh 4  ->  0")
  (ask (= (/ 0 (asinh 4)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (4:ℂ) = ((4:ℝ):ℂ) by norm_num, AE.asinh_ofReal]; exact_mod_cast (Real.arsinh_pos_iff.mpr (by norm_num)).ne'"))

Case set `ee702ae2fe06`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
sp-acj4-1007-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1107-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1148-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1149-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1177-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1195-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1217-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1238-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1247-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1254-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-1258-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5372-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5382-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-5385-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-819-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-837-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-848-ground true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-868-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-911-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
sp-acj4-927-ground true	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓

sp-acj4-1007-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\sin 5} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1007] + rules.json[700]: / 0 sin 5 -> 0

Lean proof: included

(case sp-acj4-1007-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1007] + rules.json[700]: / 0 sin 5  ->  0")
  (ask (= (/ 0 (sin 5)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (5:ℂ) = ((5:ℝ):ℂ) by norm_num, AE.sin_ofReal]; have h : Real.sin 5 < 0 := by { rw [← Real.sin_sub_two_pi]; exact Real.sin_neg_of_neg_of_neg_pi_lt (by linarith [Real.pi_gt_three]) (by linarith [Real.pi_lt_d2]) }; exact_mod_cast h.ne"))

sp-acj4-1107-ground

Given

nothing

Claim

\(\displaystyle \arcsin\left(\sin\left(\frac{1}{10}\right)\right) = \frac{1}{10}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1107] + rules.json[800]: asin sin inv 10 -> 0.1

Lean proof: included

(case sp-acj4-1107-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1107] + rules.json[800]: asin sin inv 10  ->  0.1")
  (ask (= (asin (sin (/ 10))) 1/10))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [show AE.inv (10:ℂ) = ((1/10:ℝ):ℂ) by push_cast; simp, AE.sin_ofReal, AE.asin_ofReal (Real.neg_one_le_sin _) (Real.sin_le_one _), Real.arcsin_sin (by linarith [Real.pi_gt_three]) (by linarith [Real.pi_gt_three])]; push_cast; ring"))

sp-acj4-1148-ground

Given

nothing

Claim

\(\displaystyle \cosh\left(\log\left(\frac{1}{4}\right)\right) = \frac{17}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1148] + rules.json[838]: cosh log inv 4 -> 2.125

Lean proof: included

(case sp-acj4-1148-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1148] + rules.json[838]: cosh log inv 4  ->  2.125")
  (ask (= (cosh (log (/ 4))) 17/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.cosh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-1149-ground

Given

nothing

Claim

\(\displaystyle e^{\left|\log 2\right|} = 2\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1149] + rules.json[840]: exp abs log 2 -> 2

Lean proof: included

(case sp-acj4-1149-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1149] + rules.json[840]: exp abs log 2  ->  2")
  (ask (= (exp (abs (log 2))) 2))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [AE.abs_eq, show (2:ℂ) = ((2:ℝ):ℂ) by norm_num, AE.log_ofReal (by norm_num), Complex.norm_real, Real.norm_eq_abs, abs_of_pos (Real.log_pos (by norm_num))]; simp; exact Complex.exp_log (by norm_num)"))

sp-acj4-1177-ground

Given

nothing

Claim

\(\displaystyle 0^{\operatorname{arsinh}\left(10\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1177] + rules.json[913]: pow 0 asinh 10 -> 0

Lean proof: included

(case sp-acj4-1177-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1177] + rules.json[913]: pow 0 asinh 10  ->  0")
  (ask (= (pow 0 (asinh 10)) 0))
  (expect true)
  (lean-proof "have h : AE.asinh (10:ℂ) = (Real.arsinh 10 : ℂ) := (by exact_mod_cast AE.asinh_ofReal 10); simp [h, Real.arsinh_pos_iff]"))

sp-acj4-1195-ground

Given

nothing

Claim

\(\displaystyle 0^{\arctan 7} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1195] + rules.json[931]: pow 0 atan 7 -> 0

Lean proof: included

(case sp-acj4-1195-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1195] + rules.json[931]: pow 0 atan 7  ->  0")
  (ask (= (pow 0 (atan 7)) 0))
  (expect true)
  (lean-proof "have h : AE.atan (7:ℂ) = (Real.arctan 7 : ℂ) := (by exact_mod_cast AE.atan_ofReal 7); have hd : AE.atan.D (7:ℂ) := (by exact_mod_cast AE.atan.D_ofReal 7); have hp : 0 < Real.arctan 7 := Real.arctan_pos.mpr (by norm_num); refine ⟨⟨hd, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-1217-ground

Given

nothing

Claim

\(\displaystyle 0^{e^{-1}} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1217] + rules.json[953]: pow 0 exp (-1) -> 0

Lean proof: included

(case sp-acj4-1217-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1217] + rules.json[953]: pow 0 exp (-1)  ->  0")
  (ask (= (pow 0 (exp -1)) 0))
  (expect true)
  (lean-proof "simp [Complex.exp_re, Real.exp_pos]"))

sp-acj4-1238-ground

Given

nothing

Claim

\(\displaystyle 0^{\frac{1}{\pi}} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1238] + rules.json[974]: pow 0 inv np.pi -> 0

Lean proof: included

(case sp-acj4-1238-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1238] + rules.json[974]: pow 0 inv np.pi  ->  0")
  (ask (= (pow 0 (/ pi)) 0))
  (expect true)
  (lean-proof "simp [Real.pi_ne_zero, Complex.inv_re, Complex.normSq_ofReal]; positivity"))

sp-acj4-1247-ground

Given

nothing

Claim

\(\displaystyle 0^{\log 9} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1247] + rules.json[983]: pow 0 log 9 -> 0

Lean proof: included

(case sp-acj4-1247-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1247] + rules.json[983]: pow 0 log 9  ->  0")
  (ask (= (pow 0 (log 9)) 0))
  (expect true)
  (lean-proof "simp [Complex.log_re]; exact Real.log_pos (by norm_num)"))

sp-acj4-1254-ground

Given

nothing

Claim

\(\displaystyle 0^{\sin 2} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1254] + rules.json[990]: pow 0 sin 2 -> 0

Lean proof: included

(case sp-acj4-1254-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1254] + rules.json[990]: pow 0 sin 2  ->  0")
  (ask (= (pow 0 (sin 2)) 0))
  (expect true)
  (lean-proof "have h : AE.sin (2:ℂ) = (Real.sin 2 : ℂ) := (by exact_mod_cast AE.sin_ofReal 2); have hp : 0 < Real.sin 2 := Real.sin_pos_of_pos_of_lt_pi (by norm_num) (by linarith [Real.pi_gt_three]); refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-1258-ground

Given

nothing

Claim

\(\displaystyle 0^{\sin 9} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[1258] + rules.json[994]: pow 0 sin 9 -> 0

Lean proof: included

(case sp-acj4-1258-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[1258] + rules.json[994]: pow 0 sin 9  ->  0")
  (ask (= (pow 0 (sin 9)) 0))
  (expect true)
  (lean-proof "have h : AE.sin (9:ℂ) = (Real.sin 9 : ℂ) := (by exact_mod_cast AE.sin_ofReal 9); have hp : 0 < Real.sin 9 := (by rw [← Real.sin_sub_two_pi]; exact Real.sin_pos_of_pos_of_lt_pi (by linarith [Real.pi_lt_d2]) (by linarith [Real.pi_gt_three])); refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [h, AE.pow.D_iff]; right; rw [Complex.ofReal_re]; exact hp"))

sp-acj4-5372-ground

Given

nothing

Claim

\(\displaystyle \sin\left(\arcsin\left(\frac{1}{-4}\right)\right) = -\frac{1}{4}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5372] + rules.json[5127]: sin asin inv (-4) -> -0.25

Lean proof: included

(case sp-acj4-5372-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5372] + rules.json[5127]: sin asin inv (-4)  ->  -0.25")
  (ask (= (sin (asin (/ -4))) -1/4))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; rw [show AE.inv (-4:ℂ) = ((-1/4:ℝ):ℂ) by push_cast; simp; ring, AE.asin_ofReal (by norm_num) (by norm_num), AE.sin_ofReal, Real.sin_arcsin (by norm_num) (by norm_num)]; push_cast; ring"))

sp-acj4-5382-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(\log\left(\frac{1}{4}\right)\right) = -\frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5382] + rules.json[5137]: sinh log inv 4 -> -1.875

Lean proof: included

(case sp-acj4-5382-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5382] + rules.json[5137]: sinh log inv 4  ->  -1.875")
  (ask (= (sinh (log (/ 4))) -15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-5385-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(-\log 4\right) = -\frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[5385] + rules.json[5140]: sinh neg log 4 -> -1.875

Lean proof: included

(case sp-acj4-5385-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[5385] + rules.json[5140]: sinh neg log 4  ->  -1.875")
  (ask (= (sinh (- (log 4))) -15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-819-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\pi} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[819] + rules.json[481]: / 0 np.pi -> 0

Lean proof: included

(case sp-acj4-819-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[819] + rules.json[481]: / 0 np.pi  ->  0")
  (ask (= (/ 0 pi) 0))
  (expect true)
  (lean-proof "simp [Real.pi_ne_zero]"))

sp-acj4-837-ground

Given

nothing

Claim

\(\displaystyle 0^{\pi} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[837] + rules.json[502]: pow 0 np.pi -> 0

Lean proof: included

(case sp-acj4-837-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[837] + rules.json[502]: pow 0 np.pi  ->  0")
  (ask (= (pow 0 pi) 0))
  (expect true)
  (lean-proof "simp [Real.pi_pos]"))

sp-acj4-848-ground

Given

nothing

Claim

\(\displaystyle \sinh\left(\log 4\right) = \frac{15}{8}\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[848] + rules.json[512]: sinh log 4 -> 1.875

Lean proof: included

(case sp-acj4-848-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[848] + rules.json[512]: sinh log 4  ->  1.875")
  (ask (= (sinh (log 4)) 15/8))
  (expect true)
  (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sinh, Complex.exp_neg, Complex.exp_log]; norm_num"))

sp-acj4-868-ground

Given

nothing

Claim

\(\displaystyle 0 \, \operatorname{arcosh}\left(7\right) = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[868] + rules.json[561]: * 0 acosh 7 -> 0

Lean proof: included

(case sp-acj4-868-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[868] + rules.json[561]: * 0 acosh 7  ->  0")
  (ask (= (* 0 (acosh 7)) 0))
  (expect true)
  (lean-proof "simp"))

sp-acj4-911-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\arcsin\left(-1\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[911] + rules.json[604]: / 0 asin (-1) -> 0

Lean proof: included

(case sp-acj4-911-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[911] + rules.json[604]: / 0 asin (-1)  ->  0")
  (ask (= (/ 0 (asin -1)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (-1:ℂ) = ((-1:ℝ):ℂ) by push_cast; rfl, AE.asin_ofReal (by norm_num) (by norm_num), Real.arcsin_neg_one]; simp [Real.pi_ne_zero]"))

sp-acj4-927-ground

Given

nothing

Claim

\(\displaystyle \frac{0}{\operatorname{arsinh}\left(4\right)} = 0\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

SimpliPy acj-4 (MIT) rules_real.json[927] + rules.json[620]: / 0 asinh 4 -> 0

Lean proof: included

(case sp-acj4-927-ground (category simplipy-ground)
  (note "SimpliPy acj-4 (MIT) rules_real.json[927] + rules.json[620]: / 0 asinh 4  ->  0")
  (ask (= (/ 0 (asinh 4)) 0))
  (expect true)
  (lean-proof "refine ⟨⟨by simp, ?_⟩, by simp⟩; rw [show (4:ℂ) = ((4:ℝ):ℂ) by norm_num, AE.asinh_ofReal]; exact_mod_cast (Real.arsinh_pos_iff.mpr (by norm_num)).ne'"))

simplipy-ground

Case set ba9dc4def822

Case set 3ba0dfac4bca

Case set ee702ae2fe06

Case set `ba9dc4def822`

Case set `3ba0dfac4bca`

Case set `ee702ae2fe06`