simplipy-real
Real flavour of rules found in both rule files: the rule over the reals, with only the assumptions that make it defined.
Case set ba9dc4def822
sp-acj4-1-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[1] + rules.json[0]: asin abs _0 -> abs asin _0
Lean proof: included
(case sp-acj4-1-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[1] + rules.json[0]: asin abs _0 -> abs asin _0") (var x real) (ask (= (asin (abs 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_r1w2 | 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-102-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[102] + rules.json[81]: / abs _0 6 -> abs / _0 (-6)
Lean proof: included
(case sp-acj4-102-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[102] + rules.json[81]: / abs _0 6 -> abs / _0 (-6)") (var x real) (ask (= (/ (abs x) 6) (abs (/ x -6)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq, div_eq_mul_inv]"))
sp-acj4-108-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[108] + rules.json[87]: / abs _0 _0 -> / _0 abs _0
Lean proof: included
(case sp-acj4-108-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[108] + rules.json[87]: / abs _0 _0 -> / _0 abs _0") (var x real) (assume (nonzero x)) (assume (nonzero (abs x))) (ask (= (/ (abs x) x) (/ x (abs x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; have hr : (r:ℂ) ≠ 0 := h0.2; have ha : ((|r|:ℝ):ℂ) ≠ 0 := (by have := h1.2; rwa [AE.abs_ofReal] at this); simp only [AE.abs_ofReal, AE.inv_def]; rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_eq_div_iff hr ha]; exact_mod_cast (abs_mul_abs_self r)"))
sp-acj4-120-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[120] + rules.json[92]: / np.pi abs _0 -> abs / np.pi _0
Lean proof: included
(case sp-acj4-120-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[120] + rules.json[92]: / np.pi abs _0 -> abs / np.pi _0") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (/ pi (abs x)) (abs (/ pi x)))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, h1.2, by simp⟩, ?_⟩; simp [AE.abs_eq, abs_of_pos Real.pi_pos]"))
sp-acj4-127-real
equal at some admissible points, different at others
witness (true): \(x = -1\)
witness (false): \(x = 1\)
SimpliPy acj-4 (MIT) rules_real.json[127] + rules.json[96]: abs atanh exp _0 -> atanh exp _0
Lean proof: included
(case sp-acj4-127-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[127] + rules.json[96]: abs atanh exp _0 -> atanh exp _0") (var x real) (assume (!= (exp x) 1)) (assume (!= (exp x) -1)) (ask (= (abs (atanh (exp x))) (atanh (exp x)))) (expect contingent) (witness true (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r127w1 | exact AE.w2_exp_neg_one_ne_one | exact AE.w2_exp_neg_one_ne_neg_one | exact AE.w2_atanhD_exp_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]")) (witness false (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r127w2 | exact AE.w2_exp_one_ne_one | exact AE.w2_exp_one_ne_neg_one | exact AE.w2_atanhD_exp_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-128-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[128] + rules.json[97]: abs cos asin _0 -> cos asin _0
Lean proof: included
(case sp-acj4-128-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[128] + rules.json[97]: abs cos asin _0 -> cos asin _0") (var x real) (ask (= (abs (cos (asin x))) (cos (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_r128w2 | 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-131-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[131] + rules.json[99]: abs log cosh _0 -> log cosh _0
Lean proof: included
(case sp-acj4-131-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[131] + rules.json[99]: abs log cosh _0 -> log cosh _0") (var x real) (assume (nonzero (cosh x))) (ask (= (abs (log (cosh x))) (log (cosh x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨⟨trivial, h0.2⟩, by simp⟩, trivial, h0.2⟩, ?_⟩; rw [AE.cosh_ofReal, AE.log_ofReal (Real.cosh_pos r).le, AE.abs_ofReal, abs_of_nonneg (Real.log_nonneg (Real.one_le_cosh r))]"))
sp-acj4-132-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[132] + rules.json[100]: abs log sin _0 -> neg log sin _0
Lean proof: included
(case sp-acj4-132-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[132] + rules.json[100]: abs log sin _0 -> neg log sin _0") (var x real) (assume (nonzero (sin x))) (ask (= (abs (log (sin x))) (- (log (sin x))))) (expect contingent) (witness true (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r132w1 | exact AE.w2_sin_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) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r132w2 | exact AE.w2_sin_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]")))
sp-acj4-133-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[133] + rules.json[101]: abs log tanh _0 -> neg log tanh _0
Lean proof: included
(case sp-acj4-133-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[133] + rules.json[101]: abs log tanh _0 -> neg log tanh _0") (var x real) (assume (nonzero (tanh x))) (ask (= (abs (log (tanh x))) (- (log (tanh x))))) (expect contingent) (witness true (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r133w1 | exact AE.w2_tanh_one_ne | exact AE.w2_tanhD_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]")) (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r133w2 | exact AE.w2_tanh_neg_one_ne | exact AE.w2_tanhD_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-136-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[136] + rules.json[104]: abs pow _0 np.e -> pow _0 np.e
Lean proof: included
(case sp-acj4-136-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[136] + rules.json[104]: abs pow _0 np.e -> pow _0 np.e") (var x real) (assume (or (nonzero x) (> (re (exp 1)) 0))) (ask (= (abs (pow x (exp 1))) (pow x (exp 1)))) (expect contingent) (witness true (x 0) (lean-proof "constructorm* _ ∧ _ <;> first | 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, Complex.exp_im]")) (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r136w2 | 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-137-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[137] + rules.json[105]: abs pow _0 np.pi -> pow _0 np.pi
Lean proof: included
(case sp-acj4-137-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[137] + rules.json[105]: abs pow _0 np.pi -> pow _0 np.pi") (var x real) (assume (or (nonzero x) (> (re pi) 0))) (ask (= (abs (pow x pi)) (pow x pi))) (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 -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r137w2 | 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-14-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[14] + rules.json[10]: neg sin _0 -> sin neg _0
Lean proof: included
(case sp-acj4-14-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[14] + rules.json[10]: neg sin _0 -> sin neg _0") (var x real) (ask (= (- (sin x)) (sin (- x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sin_neg]"))
sp-acj4-145-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[145] + rules.json[113]: abs sin acos _0 -> cos asin _0
Lean proof: included
(case sp-acj4-145-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[145] + rules.json[113]: abs sin acos _0 -> cos asin _0") (var x real) (ask (= (abs (sin (acos x))) (cos (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_r145w2 | 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-162-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[162] + rules.json[119]: acosh rootn _0 5 -> acosh pow _0 0.2
Lean proof: included
(case sp-acj4-162-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[162] + rules.json[119]: acosh rootn _0 5 -> acosh pow _0 0.2") (var x real) (ask (= (acosh (surd x 5)) (acosh (pow x 1/5)))) (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 -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r162w2 | 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-179-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 3\)
SimpliPy acj-4 (MIT) rules_real.json[179] + rules.json[128]: atan sinh acos _0 -> asin tanh acos _0
Lean proof: included
(case sp-acj4-179-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[179] + rules.json[128]: atan sinh acos _0 -> asin tanh acos _0") (var x real) (assume (!= (sinh (acos x)) i)) (assume (!= (sinh (acos x)) (- i))) (assume (nonzero (cosh (acos x)))) (ask (= (atan (sinh (acos x))) (asin (tanh (acos x))))) (expect contingent) (witness true (x 0) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r179w1 | exact AE.w2_r179w1_hI | exact AE.w2_r179w1_hnI | exact AE.w2_r179w1_atanD | exact AE.w2_r179w1_cosh | exact AE.w2_r179w1_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]")) (witness false (x 3) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r179w2 | exact AE.w2_r179_hI | exact AE.w2_r179_hnI | exact AE.w2_r179_atanD | exact AE.w2_r179_cosh | exact AE.w2_r179_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-181-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 3\)
SimpliPy acj-4 (MIT) rules_real.json[181] + rules.json[129]: atan sinh asin _0 -> asin tanh asin _0
Lean proof: included
(case sp-acj4-181-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[181] + rules.json[129]: atan sinh asin _0 -> asin tanh asin _0") (var x real) (assume (!= (sinh (asin x)) i)) (assume (!= (sinh (asin x)) (- i))) (assume (nonzero (cosh (asin x)))) (ask (= (atan (sinh (asin x))) (asin (tanh (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 3) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r181w2 | exact AE.w2_r181_hI | exact AE.w2_r181_hnI | exact AE.w2_r181_atanD | exact AE.w2_r181_cosh | exact AE.w2_r181_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-185-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[185] + rules.json[132]: atan tan cos _0 -> cos _0
Lean proof: included
(case sp-acj4-185-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[185] + rules.json[132]: atan tan cos _0 -> cos _0") (var x real) (assume (nonzero (cos (cos x)))) (assume (!= (tan (cos x)) i)) (assume (!= (tan (cos x)) (- i))) (ask (= (atan (tan (cos x))) (cos x))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨⟨trivial, h1.1.2⟩, by rw [AE.cos_ofReal, AE.tan_ofReal]; exact AE.atan.D_ofReal _⟩, trivial⟩, ?_⟩; rw [AE.cos_ofReal, AE.tan_ofReal, AE.atan_ofReal, Real.arctan_tan (by linarith [Real.neg_one_le_cos r, Real.pi_gt_three]) (by linarith [Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-194-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[194] + rules.json[136]: atanh sin cos _0 -> asinh tan cos _0
Lean proof: included
(case sp-acj4-194-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[194] + rules.json[136]: atanh sin cos _0 -> asinh tan cos _0") (var x real) (assume (!= (sin (cos x)) 1)) (assume (!= (sin (cos x)) -1)) (assume (nonzero (cos (cos x)))) (ask (= (atanh (sin (cos x))) (asinh (tan (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.cos r := (by linarith [Real.neg_one_le_cos r, Real.pi_gt_three]); have hy2 : Real.cos r < Real.pi / 2 := (by linarith [Real.cos_le_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.cos_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.cos r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.cos r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp, by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp, by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp⟩, ?_⟩; rw [AE.cos_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-195-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[195] + rules.json[137]: atanh sin sin _0 -> asinh tan sin _0
Lean proof: included
(case sp-acj4-195-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[195] + rules.json[137]: atanh sin sin _0 -> asinh tan sin _0") (var x real) (assume (!= (sin (sin x)) 1)) (assume (!= (sin (sin x)) -1)) (assume (nonzero (cos (sin x)))) (ask (= (atanh (sin (sin x))) (asinh (tan (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.sin r := (by linarith [Real.neg_one_le_sin r, Real.pi_gt_three]); have hy2 : Real.sin r < Real.pi / 2 := (by linarith [Real.sin_le_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.sin_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.sin r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.sin r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp, by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp, by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp⟩, ?_⟩; rw [AE.sin_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-196-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[196] + rules.json[138]: atanh sin tanh _0 -> asinh tan tanh _0
Lean proof: included
(case sp-acj4-196-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[196] + rules.json[138]: atanh sin tanh _0 -> asinh tan tanh _0") (var x real) (assume (!= (sin (tanh x)) 1)) (assume (!= (sin (tanh x)) -1)) (assume (nonzero (cos (tanh x)))) (ask (= (atanh (sin (tanh x))) (asinh (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.tanh r := (by linarith [Real.neg_one_lt_tanh r, Real.pi_gt_three]); have hy2 : Real.tanh r < Real.pi / 2 := (by linarith [Real.tanh_lt_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.tanh_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.tanh r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.tanh r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp [AE.cosh_ofReal_ne_zero]⟩, ?_⟩; rw [AE.tanh_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-218-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[218] + rules.json[150]: inv / (-6) !0 -> / !0 (-6)
Lean proof: included
(case sp-acj4-218-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[218] + rules.json[150]: inv / (-6) !0 -> / !0 (-6)") (var x real) (assume (nonzero x)) (assume (nonzero (/ -6 x))) (ask (= (/ (/ -6 x)) (/ x -6))) (expect true) (lean-proof "refine ⟨⟨h0.2, h1.2⟩, ?_⟩; have hx : x ≠ 0 := h0.2; simp only [AE.inv_def]; field_simp; try ring"))
sp-acj4-22-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[22] + rules.json[17]: tanh abs _0 -> abs tanh _0
Lean proof: included
(case sp-acj4-22-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[22] + rules.json[17]: tanh abs _0 -> abs tanh _0") (var x real) (ask (= (tanh (abs x)) (abs (tanh x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [AE.abs_ofReal, AE.tanh_ofReal, AE.tanh_ofReal, AE.abs_ofReal]; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; rw [AE.tanh_abs]"))
sp-acj4-220-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[220] + rules.json[152]: inv / (-8) !0 -> / !0 (-8)
Lean proof: included
(case sp-acj4-220-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[220] + rules.json[152]: inv / (-8) !0 -> / !0 (-8)") (var x real) (assume (nonzero x)) (assume (nonzero (/ -8 x))) (ask (= (/ (/ -8 x)) (/ x -8))) (expect true) (lean-proof "refine ⟨⟨h0.2, h1.2⟩, ?_⟩; have hx : x ≠ 0 := h0.2; simp only [AE.inv_def]; field_simp; try ring"))
sp-acj4-233-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[233] + rules.json[162]: inv pow _0 np.pi -> pow _0 neg np.pi
Lean proof: included
(case sp-acj4-233-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[233] + rules.json[162]: inv pow _0 np.pi -> pow _0 neg np.pi") (var x real) (assume (or (nonzero x) (> (re pi) 0))) (assume (nonzero (pow x pi))) (assume (or (nonzero x) (> (re (- pi)) 0))) (ask (= (/ (pow x pi)) (pow x (- pi)))) (expect true) (lean-proof "have hx : x ≠ 0 := (by intro h; apply h1.2; rw [h]; simp); refine ⟨⟨⟨by simp [hx], h1.2⟩, by simp [hx]⟩, ?_⟩; simp only [AE.pow, if_neg hx, AE.inv_def, AE.exp_def]; rw [← Complex.exp_neg]; ring_nf"))
sp-acj4-248-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[248] + rules.json[164]: neg abs asin _0 -> asin neg abs _0
Lean proof: included
(case sp-acj4-248-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[248] + rules.json[164]: neg abs asin _0 -> asin neg abs _0") (var x real) (ask (= (- (abs (asin x))) (asin (- (abs 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_r248w2 | 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-249-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[249] + rules.json[165]: neg abs asinh _0 -> asinh neg abs _0
Lean proof: included
(case sp-acj4-249-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[249] + rules.json[165]: neg abs asinh _0 -> asinh neg abs _0") (var x real) (ask (= (- (abs (asinh x))) (asinh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.asinh_ofReal, AE.asinh_ofReal, AE.abs_ofReal, Real.arsinh_neg, AE.arsinh_abs]; push_cast; ring"))
sp-acj4-251-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[251] + rules.json[167]: neg abs atanh _0 -> atanh neg abs _0
Lean proof: included
(case sp-acj4-251-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[251] + rules.json[167]: neg abs atanh _0 -> atanh neg abs _0") (var x real) (assume (!= x 1)) (assume (!= x -1)) (assume (!= (- (abs x)) 1)) (assume (!= (- (abs x)) -1)) (ask (= (- (abs (atanh x))) (atanh (- (abs 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_r251w2 | 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-252-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[252] + rules.json[168]: neg abs sinh _0 -> sinh neg abs _0
Lean proof: included
(case sp-acj4-252-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[252] + rules.json[168]: neg abs sinh _0 -> sinh neg abs _0") (var x real) (ask (= (- (abs (sinh x))) (sinh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.sinh_ofReal, AE.sinh_ofReal, AE.abs_ofReal, Real.abs_sinh, Real.sinh_neg]; push_cast; ring"))
sp-acj4-253-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[253] + rules.json[169]: neg abs tanh _0 -> tanh neg abs _0
Lean proof: included
(case sp-acj4-253-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[253] + rules.json[169]: neg abs tanh _0 -> tanh neg abs _0") (var x real) (ask (= (- (abs (tanh x))) (tanh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.tanh_ofReal, AE.tanh_ofReal, AE.abs_ofReal, ← AE.tanh_abs, Real.tanh_neg]; push_cast; ring"))
sp-acj4-256-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[256] + rules.json[171]: neg exp neg !0 -> inv neg exp !0
Lean proof: included
(case sp-acj4-256-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[256] + rules.json[171]: neg exp neg !0 -> inv neg exp !0") (var x real) (assume (nonzero (- (exp x)))) (ask (= (- (exp (- x))) (/ (- (exp x))))) (expect true) (lean-proof "refine ⟨h0.2, ?_⟩; simp [Complex.exp_neg]"))
sp-acj4-275-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[275] + rules.json[184]: pow abs _0 (-3) -> abs pow _0 (-3)
Lean proof: included
(case sp-acj4-275-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[275] + rules.json[184]: pow abs _0 (-3) -> abs pow _0 (-3)") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (pow (abs x) -3) (abs (pow x -3)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : (r:ℂ) ≠ 0 := h1.2; have ha : AE.abs (r:ℂ) ≠ 0 := h0.2; refine ⟨⟨⟨by simp, by simp [ha]⟩, by simp [hr], by simp⟩, ?_⟩; rw [AE.pow_neg_ofNat ha, AE.pow_neg_ofNat hr, AE.abs_inv, AE.abs_eq, AE.abs_eq]; simp"))
sp-acj4-276-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[276] + rules.json[185]: pow abs _0 (-4) -> pow _0 (-4)
Lean proof: included
(case sp-acj4-276-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[276] + rules.json[185]: pow abs _0 (-4) -> pow _0 (-4)") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (pow (abs x) -4) (pow x -4))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : (r:ℂ) ≠ 0 := h1.2; have ha : AE.abs (r:ℂ) ≠ 0 := h0.2; refine ⟨⟨⟨by simp, by simp [ha]⟩, by simp [hr]⟩, ?_⟩; rw [AE.pow_neg_ofNat ha, AE.pow_neg_ofNat hr, AE.abs_ofReal]; congr 1; exact_mod_cast (Even.pow_abs ⟨2, by norm_num⟩ r)"))
sp-acj4-283-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[283] + rules.json[192]: pow abs _0 2 -> * _0 _0
Lean proof: included
(case sp-acj4-283-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[283] + rules.json[192]: pow abs _0 2 -> * _0 _0") (var x real) (ask (= (pow (abs x) 2) (* x x))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.abs_ofReal]; exact_mod_cast (by rw [sq_abs]; ring : |r|^2 = r*r)"))
sp-acj4-286-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[286] + rules.json[195]: pow abs _0 5 -> abs pow _0 5
Lean proof: included
(case sp-acj4-286-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[286] + rules.json[195]: pow abs _0 5 -> abs pow _0 5") (var x real) (ask (= (pow (abs x) 5) (abs (pow x 5)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.pow_ofNat_real, AE.abs_ofReal r, ← Complex.ofReal_pow r, AE.abs_ofReal (r^5), abs_pow]; push_cast; ring"))
sp-acj4-289-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[289] + rules.json[198]: pow abs _0 8 -> pow _0 8
Lean proof: included
(case sp-acj4-289-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[289] + rules.json[198]: pow abs _0 8 -> pow _0 8") (var x real) (ask (= (pow (abs x) 8) (pow x 8))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.pow_ofNat_real, AE.abs_ofReal]; exact_mod_cast (Even.pow_abs ⟨4, by norm_num⟩ r)"))
sp-acj4-31-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[31] + rules.json[24]: * 5 abs _0 -> abs * (-5) _0
Lean proof: included
(case sp-acj4-31-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[31] + rules.json[24]: * 5 abs _0 -> abs * (-5) _0") (var x real) (ask (= (* 5 (abs x)) (abs (* -5 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq]"))
sp-acj4-326-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[326] + rules.json[208]: pow exp _0 2 -> exp * 2 _0
Lean proof: included
(case sp-acj4-326-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[326] + rules.json[208]: pow exp _0 2 -> exp * 2 _0") (var x real) (ask (= (pow (exp x) 2) (exp (* 2 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.exp_def, AE.exp_def, ← Complex.exp_nat_mul]; norm_num"))
sp-acj4-33-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[33] + rules.json[26]: * 6 abs _0 -> abs * (-6) _0
Lean proof: included
(case sp-acj4-33-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[33] + rules.json[26]: * 6 abs _0 -> abs * (-6) _0") (var x real) (ask (= (* 6 (abs x)) (abs (* -6 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq]"))
sp-acj4-35-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[35] + rules.json[28]: * 7 log _0 -> log pow _0 7
Lean proof: included
(case sp-acj4-35-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[35] + rules.json[28]: * 7 log _0 -> log pow _0 7") (var x real) (assume (nonzero x)) (assume (nonzero (pow x 7))) (ask (= (* 7 (log x)) (log (pow x 7)))) (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_r35w2 | 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-354-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[354] + rules.json[224]: pow _0 log 5 -> pow 5 log _0
Lean proof: included
(case sp-acj4-354-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[354] + rules.json[224]: pow _0 log 5 -> pow 5 log _0") (var x real) (assume (or (nonzero x) (> (re (log 5)) 0))) (assume (nonzero x)) (ask (= (pow x (log 5)) (pow 5 (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by norm_num, by simp [hx]⟩, hx, by simp⟩, ?_⟩; simp [AE.pow, hx, mul_comm]"))
sp-acj4-356-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[356] + rules.json[226]: pow _0 log 7 -> pow 7 log _0
Lean proof: included
(case sp-acj4-356-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[356] + rules.json[226]: pow _0 log 7 -> pow 7 log _0") (var x real) (assume (or (nonzero x) (> (re (log 7)) 0))) (assume (nonzero x)) (ask (= (pow x (log 7)) (pow 7 (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by norm_num, by simp [hx]⟩, hx, by simp⟩, ?_⟩; simp [AE.pow, hx, mul_comm]"))
sp-acj4-359-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[359] + rules.json[227]: pow _0 log np.pi -> pow np.pi log _0
Lean proof: included
(case sp-acj4-359-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[359] + rules.json[227]: pow _0 log np.pi -> pow np.pi log _0") (var x real) (assume (or (nonzero x) (> (re (log pi)) 0))) (assume (nonzero x)) (ask (= (pow x (log pi)) (pow pi (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by simp [Real.pi_ne_zero], by simp [hx]⟩, hx, by simp [Real.pi_ne_zero]⟩, ?_⟩; simp [AE.pow, hx, Real.pi_ne_zero, mul_comm]"))
sp-acj4-364-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[364] + rules.json[232]: rootn abs _0 3 -> abs rootn _0 3
Lean proof: included
(case sp-acj4-364-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[364] + rules.json[232]: rootn abs _0 3 -> abs rootn _0 3") (var x real) (ask (= (surd (abs x) 3) (abs (surd x 3)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [show (3:ℂ) = ((3:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨AE.abs_isReal _, AE.IsInt.ofInt 3, by norm_num, Or.inr (AE.odd_ofInt ⟨1, by norm_num⟩), Or.inr (by norm_num)⟩⟩, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt 3, by norm_num, Or.inr (AE.odd_ofInt ⟨1, by norm_num⟩), Or.inr (by norm_num)⟩, by simp⟩, ?_⟩; rw [AE.abs_ofReal, AE.surd_abs_odd r (by norm_num)]"))
sp-acj4-367-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[367] + rules.json[235]: rootn abs _0 9 -> abs rootn _0 9
Lean proof: included
(case sp-acj4-367-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[367] + rules.json[235]: rootn abs _0 9 -> abs rootn _0 9") (var x real) (ask (= (surd (abs x) 9) (abs (surd x 9)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [show (9:ℂ) = ((9:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨AE.abs_isReal _, AE.IsInt.ofInt 9, by norm_num, Or.inr (AE.odd_ofInt ⟨4, by norm_num⟩), Or.inr (by norm_num)⟩⟩, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt 9, by norm_num, Or.inr (AE.odd_ofInt ⟨4, by norm_num⟩), Or.inr (by norm_num)⟩, by simp⟩, ?_⟩; rw [AE.abs_ofReal, AE.surd_abs_odd r (by norm_num)]"))
sp-acj4-368-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[368] + rules.json[236]: rootn acos _0 (-5) -> pow acos _0 -0.2
Lean proof: included
(case sp-acj4-368-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[368] + rules.json[236]: rootn acos _0 (-5) -> pow acos _0 -0.2") (var x real) (assume (real (acos x))) (assume (nonzero (acos x))) (ask (= (surd (acos x) -5) (pow (acos x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.mem_Icc_of_acos_real (by simpa using h0.2); rw [AE.acos_ofReal hI.1 hI.2]; have ha : 0 ≤ Real.arccos r := Real.arccos_nonneg r; have hne : Real.arccos r ≠ 0 := (by have := h1.2; rw [AE.acos_ofReal hI.1 hI.2] at this; intro h; exact this (by rw [h]; simp)); rw [show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inl (by exact_mod_cast hne)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hne)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inl hne)]"))
sp-acj4-369-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[369] + rules.json[237]: rootn acos _0 5 -> pow acos _0 0.2
Lean proof: included
(case sp-acj4-369-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[369] + rules.json[237]: rootn acos _0 5 -> pow acos _0 0.2") (var x real) (assume (real (acos x))) (ask (= (surd (acos x) 5) (pow (acos x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.mem_Icc_of_acos_real (by simpa using h0.2); rw [AE.acos_ofReal hI.1 hI.2]; have ha : 0 ≤ Real.arccos r := Real.arccos_nonneg r; rw [show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inr (by norm_num)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inr (by norm_num)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inr (by norm_num))]"))
sp-acj4-370-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[370] + rules.json[238]: rootn acosh _0 (-5) -> pow acosh _0 -0.2
Lean proof: included
(case sp-acj4-370-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[370] + rules.json[238]: rootn acosh _0 (-5) -> pow acosh _0 -0.2") (var x real) (assume (real (acosh x))) (assume (nonzero (acosh x))) (ask (= (surd (acosh x) -5) (pow (acosh x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.one_le_of_acosh_real (by simpa using h0.2); rw [AE.acosh_ofReal hI]; have ha : 0 ≤ Real.arcosh r := AE.arcosh_nonneg hI; have hne : Real.arcosh r ≠ 0 := (by have := h1.2; rw [AE.acosh_ofReal hI] at this; intro h; exact this (by rw [h]; simp)); rw [show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inl (by exact_mod_cast hne)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hne)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inl hne)]"))
sp-acj4-371-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[371] + rules.json[239]: rootn acosh _0 5 -> pow acosh _0 0.2
Lean proof: included
(case sp-acj4-371-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[371] + rules.json[239]: rootn acosh _0 5 -> pow acosh _0 0.2") (var x real) (assume (real (acosh x))) (ask (= (surd (acosh x) 5) (pow (acosh x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.one_le_of_acosh_real (by simpa using h0.2); rw [AE.acosh_ofReal hI]; have ha : 0 ≤ Real.arcosh r := AE.arcosh_nonneg hI; rw [show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inr (by norm_num)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inr (by norm_num)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inr (by norm_num))]"))
sp-acj4-372-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[372] + rules.json[240]: rootn cosh _0 (-5) -> pow cosh _0 -0.2
Lean proof: included
(case sp-acj4-372-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[372] + rules.json[240]: rootn cosh _0 (-5) -> pow cosh _0 -0.2") (var x real) (assume (nonzero (cosh x))) (ask (= (surd (cosh x) -5) (pow (cosh x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hc := Real.cosh_pos r; rw [AE.cosh_ofReal, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨trivial, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simp; positivity), Or.inl (by exact_mod_cast hc.ne')⟩⟩, trivial, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hc.ne')⟩, ?_⟩; rw [AE.surd_ofReal_nonneg hc.le (by norm_num), show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, AE.pow_ofReal hc.le (Or.inl hc.ne')]"))
sp-acj4-373-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[373] + rules.json[241]: rootn cosh _0 5 -> pow cosh _0 0.2
Lean proof: included
(case sp-acj4-373-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[373] + rules.json[241]: rootn cosh _0 5 -> pow cosh _0 0.2") (var x real) (ask (= (surd (cosh x) 5) (pow (cosh x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hc := Real.cosh_pos r; rw [AE.cosh_ofReal, show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨trivial, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simp; positivity), Or.inl (by exact_mod_cast hc.ne')⟩⟩, trivial, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hc.ne')⟩, ?_⟩; rw [AE.surd_ofReal_nonneg hc.le (by norm_num), AE.pow_ofReal hc.le (Or.inl hc.ne')]"))
sp-acj4-38-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[38] + rules.json[31]: * 9 log _0 -> log pow _0 9
Lean proof: included
(case sp-acj4-38-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[38] + rules.json[31]: * 9 log _0 -> log pow _0 9") (var x real) (assume (nonzero x)) (assume (nonzero (pow x 9))) (ask (= (* 9 (log x)) (log (pow 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_r38w2 | 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-394-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[394] + rules.json[242]: sin abs atanh _0 -> abs sin atanh _0
Lean proof: included
(case sp-acj4-394-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[394] + rules.json[242]: sin abs atanh _0 -> abs sin atanh _0") (var x real) (assume (!= x 1)) (assume (!= x -1)) (ask (= (sin (abs (atanh x))) (abs (sin (atanh 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_r394w2 | 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-395-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[395] + rules.json[243]: sin abs cos _0 -> abs sin cos _0
Lean proof: included
(case sp-acj4-395-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[395] + rules.json[243]: sin abs cos _0 -> abs sin cos _0") (var x real) (ask (= (sin (abs (cos x))) (abs (sin (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.cos_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [Real.neg_one_le_cos r, Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-396-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[396] + rules.json[244]: sin abs sin _0 -> abs sin sin _0
Lean proof: included
(case sp-acj4-396-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[396] + rules.json[244]: sin abs sin _0 -> abs sin sin _0") (var x real) (ask (= (sin (abs (sin x))) (abs (sin (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.sin_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [Real.neg_one_le_sin r, Real.sin_le_one r, Real.pi_gt_three])]"))
sp-acj4-397-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[397] + rules.json[245]: sin abs tanh _0 -> abs sin tanh _0
Lean proof: included
(case sp-acj4-397-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[397] + rules.json[245]: sin abs tanh _0 -> abs sin tanh _0") (var x real) (ask (= (sin (abs (tanh x))) (abs (sin (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.tanh_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [(Real.neg_one_lt_tanh r).le, (Real.tanh_lt_one r).le, Real.pi_gt_three])]"))
sp-acj4-402-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[402] + rules.json[246]: sin atanh abs _0 -> abs sin atanh _0
Lean proof: included
(case sp-acj4-402-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[402] + rules.json[246]: sin atanh abs _0 -> abs sin atanh _0") (var x real) (assume (!= (abs x) 1)) (assume (!= x 1)) (assume (!= x -1)) (ask (= (sin (atanh (abs x))) (abs (sin (atanh 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_r402w2 | 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-404-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[404] + rules.json[247]: sin tanh abs _0 -> abs sin tanh _0
Lean proof: included
(case sp-acj4-404-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[404] + rules.json[247]: sin tanh abs _0 -> abs sin tanh _0") (var x real) (ask (= (sin (tanh (abs x))) (abs (sin (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.tanh_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.tanh_abs, AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [(Real.neg_one_lt_tanh r).le, (Real.tanh_lt_one r).le, Real.pi_gt_three])]"))
sp-acj4-412-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[412] + rules.json[253]: tan abs asin _0 -> abs tan asin _0
Lean proof: included
(case sp-acj4-412-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[412] + rules.json[253]: tan abs asin _0 -> abs tan asin _0") (var x real) (assume (nonzero (cos (abs (asin x))))) (assume (nonzero (cos (asin x)))) (ask (= (tan (abs (asin x))) (abs (tan (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_r412w2 | exact AE.w2_r412_cos | exact AE.w2_r412_tanD | 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_asin_two]")))
sp-acj4-413-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[413] + rules.json[254]: tan abs cos _0 -> abs tan cos _0
Lean proof: included
(case sp-acj4-413-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[413] + rules.json[254]: tan abs cos _0 -> abs tan cos _0") (var x real) (assume (nonzero (cos (abs (cos x))))) (assume (nonzero (cos (cos x)))) (ask (= (tan (abs (cos x))) (abs (tan (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.cos_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_le_cos r, Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-414-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[414] + rules.json[255]: tan abs sin _0 -> abs tan sin _0
Lean proof: included
(case sp-acj4-414-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[414] + rules.json[255]: tan abs sin _0 -> abs tan sin _0") (var x real) (assume (nonzero (cos (abs (sin x))))) (assume (nonzero (cos (sin x)))) (ask (= (tan (abs (sin x))) (abs (tan (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.sin_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_le_sin r, Real.sin_le_one r, Real.pi_gt_three])]"))
sp-acj4-415-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[415] + rules.json[256]: tan abs tanh _0 -> abs tan tanh _0
Lean proof: included
(case sp-acj4-415-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[415] + rules.json[256]: tan abs tanh _0 -> abs tan tanh _0") (var x real) (assume (nonzero (cos (abs (tanh x))))) (assume (nonzero (cos (tanh x)))) (ask (= (tan (abs (tanh x))) (abs (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.tanh_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_lt_tanh r, Real.tanh_lt_one r, Real.pi_gt_three])]"))
sp-acj4-417-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[417] + rules.json[257]: tan asin abs _0 -> abs tan asin _0
Lean proof: included
(case sp-acj4-417-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[417] + rules.json[257]: tan asin abs _0 -> abs tan asin _0") (var x real) (assume (nonzero (cos (asin (abs x))))) (assume (nonzero (cos (asin x)))) (ask (= (tan (asin (abs x))) (abs (tan (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_r417w2 | 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_asin_two]")))
sp-acj4-421-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[421] + rules.json[260]: tan tanh abs _0 -> abs tan tanh _0
Lean proof: included
(case sp-acj4-421-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[421] + rules.json[260]: tan tanh abs _0 -> abs tan tanh _0") (var x real) (assume (nonzero (cos (tanh (abs x))))) (assume (nonzero (cos (tanh x)))) (ask (= (tan (tanh (abs x))) (abs (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.abs_ofReal, AE.tanh_ofReal, AE.tan_ofReal]; rw [AE.tanh_abs, AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_lt_tanh r, Real.tanh_lt_one r, Real.pi_gt_three])]"))
sp-acj4-5-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[5] + rules.json[3]: atanh abs _0 -> abs atanh _0
Lean proof: included
(case sp-acj4-5-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[5] + rules.json[3]: atanh abs _0 -> abs atanh _0") (var x real) (assume (!= (abs x) 1)) (assume (!= x 1)) (assume (!= x -1)) (ask (= (atanh (abs x)) (abs (atanh 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_r5w2 | 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-73-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[73] + rules.json[52]: / (-1) abs !0 -> inv neg abs !0
Lean proof: included
(case sp-acj4-73-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[73] + rules.json[52]: / (-1) abs !0 -> inv neg abs !0") (var x real) (assume (nonzero (abs x))) (assume (nonzero (- (abs x)))) (ask (= (/ -1 (abs x)) (/ (- (abs x))))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-80-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[80] + rules.json[59]: / (-1) cos _0 -> inv neg cos _0
Lean proof: included
(case sp-acj4-80-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[80] + rules.json[59]: / (-1) cos _0 -> inv neg cos _0") (var x real) (assume (nonzero (cos x))) (assume (nonzero (- (cos x)))) (ask (= (/ -1 (cos x)) (/ (- (cos x))))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-83-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[83] + rules.json[62]: / (-1) log !0 -> inv neg log !0
Lean proof: included
(case sp-acj4-83-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[83] + rules.json[62]: / (-1) log !0 -> inv neg log !0") (var x real) (assume (nonzero x)) (assume (nonzero (log x))) (assume (nonzero (- (log x)))) (ask (= (/ -1 (log x)) (/ (- (log x))))) (expect true) (lean-proof "refine ⟨⟨⟨h0.2, h1.2⟩, h0.2, h2.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-86-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[86] + rules.json[65]: / (-1) tan !0 -> inv neg tan !0
Lean proof: included
(case sp-acj4-86-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[86] + rules.json[65]: / (-1) tan !0 -> inv neg tan !0") (var x real) (assume (nonzero (cos x))) (assume (nonzero (tan x))) (assume (nonzero (- (tan x)))) (ask (= (/ -1 (tan x)) (/ (- (tan x))))) (expect true) (lean-proof "refine ⟨⟨⟨h1.1.1, h1.2⟩, h1.1.1, h2.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-90-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[90] + rules.json[69]: / 3 abs _0 -> abs / (-3) _0
Lean proof: included
(case sp-acj4-90-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[90] + rules.json[69]: / 3 abs _0 -> abs / (-3) _0") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (/ 3 (abs x)) (abs (/ -3 x)))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, h1.2, by simp⟩, ?_⟩; simp [AE.abs_eq, div_eq_mul_inv]"))
sp-acj4-99-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[99] + rules.json[78]: / abs _0 3 -> abs / _0 (-3)
Lean proof: included
(case sp-acj4-99-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[99] + rules.json[78]: / abs _0 3 -> abs / _0 (-3)") (var x real) (ask (= (/ (abs x) 3) (abs (/ x -3)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq, div_eq_mul_inv]"))
Case set 3ba0dfac4bca
sp-acj4-1-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[1] + rules.json[0]: asin abs _0 -> abs asin _0
Lean proof: included
(case sp-acj4-1-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[1] + rules.json[0]: asin abs _0 -> abs asin _0") (var x real) (ask (= (asin (abs 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_r1w2 | 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-102-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[102] + rules.json[81]: / abs _0 6 -> abs / _0 (-6)
Lean proof: included
(case sp-acj4-102-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[102] + rules.json[81]: / abs _0 6 -> abs / _0 (-6)") (var x real) (ask (= (/ (abs x) 6) (abs (/ x -6)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq, div_eq_mul_inv]"))
sp-acj4-108-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[108] + rules.json[87]: / abs _0 _0 -> / _0 abs _0
Lean proof: included
(case sp-acj4-108-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[108] + rules.json[87]: / abs _0 _0 -> / _0 abs _0") (var x real) (assume (nonzero x)) (assume (nonzero (abs x))) (ask (= (/ (abs x) x) (/ x (abs x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; have hr : (r:ℂ) ≠ 0 := h0.2; have ha : ((|r|:ℝ):ℂ) ≠ 0 := (by have := h1.2; rwa [AE.abs_ofReal] at this); simp only [AE.abs_ofReal, AE.inv_def]; rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_eq_div_iff hr ha]; exact_mod_cast (abs_mul_abs_self r)"))
sp-acj4-120-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[120] + rules.json[92]: / np.pi abs _0 -> abs / np.pi _0
Lean proof: included
(case sp-acj4-120-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[120] + rules.json[92]: / np.pi abs _0 -> abs / np.pi _0") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (/ pi (abs x)) (abs (/ pi x)))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, h1.2, by simp⟩, ?_⟩; simp [AE.abs_eq, abs_of_pos Real.pi_pos]"))
sp-acj4-127-real
equal at some admissible points, different at others
witness (true): \(x = -1\)
witness (false): \(x = 1\)
SimpliPy acj-4 (MIT) rules_real.json[127] + rules.json[96]: abs atanh exp _0 -> atanh exp _0
Lean proof: included
(case sp-acj4-127-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[127] + rules.json[96]: abs atanh exp _0 -> atanh exp _0") (var x real) (assume (!= (exp x) 1)) (assume (!= (exp x) -1)) (ask (= (abs (atanh (exp x))) (atanh (exp x)))) (expect contingent) (witness true (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r127w1 | exact AE.w2_exp_neg_one_ne_one | exact AE.w2_exp_neg_one_ne_neg_one | exact AE.w2_atanhD_exp_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]")) (witness false (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r127w2 | exact AE.w2_exp_one_ne_one | exact AE.w2_exp_one_ne_neg_one | exact AE.w2_atanhD_exp_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-128-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[128] + rules.json[97]: abs cos asin _0 -> cos asin _0
Lean proof: included
(case sp-acj4-128-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[128] + rules.json[97]: abs cos asin _0 -> cos asin _0") (var x real) (ask (= (abs (cos (asin x))) (cos (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_r128w2 | 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-131-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[131] + rules.json[99]: abs log cosh _0 -> log cosh _0
Lean proof: included
(case sp-acj4-131-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[131] + rules.json[99]: abs log cosh _0 -> log cosh _0") (var x real) (assume (nonzero (cosh x))) (ask (= (abs (log (cosh x))) (log (cosh x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨⟨trivial, h0.2⟩, by simp⟩, trivial, h0.2⟩, ?_⟩; rw [AE.cosh_ofReal, AE.log_ofReal (Real.cosh_pos r).le, AE.abs_ofReal, abs_of_nonneg (Real.log_nonneg (Real.one_le_cosh r))]"))
sp-acj4-132-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[132] + rules.json[100]: abs log sin _0 -> neg log sin _0
Lean proof: included
(case sp-acj4-132-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[132] + rules.json[100]: abs log sin _0 -> neg log sin _0") (var x real) (assume (nonzero (sin x))) (ask (= (abs (log (sin x))) (- (log (sin x))))) (expect contingent) (witness true (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r132w1 | exact AE.w2_sin_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) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r132w2 | exact AE.w2_sin_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]")))
sp-acj4-133-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[133] + rules.json[101]: abs log tanh _0 -> neg log tanh _0
Lean proof: included
(case sp-acj4-133-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[133] + rules.json[101]: abs log tanh _0 -> neg log tanh _0") (var x real) (assume (nonzero (tanh x))) (ask (= (abs (log (tanh x))) (- (log (tanh x))))) (expect contingent) (witness true (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r133w1 | exact AE.w2_tanh_one_ne | exact AE.w2_tanhD_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]")) (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r133w2 | exact AE.w2_tanh_neg_one_ne | exact AE.w2_tanhD_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-136-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[136] + rules.json[104]: abs pow _0 np.e -> pow _0 np.e
Lean proof: included
(case sp-acj4-136-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[136] + rules.json[104]: abs pow _0 np.e -> pow _0 np.e") (var x real) (assume (or (nonzero x) (> (re (exp 1)) 0))) (ask (= (abs (pow x (exp 1))) (pow x (exp 1)))) (expect contingent) (witness true (x 0) (lean-proof "constructorm* _ ∧ _ <;> first | 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, Complex.exp_im]")) (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r136w2 | 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-137-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[137] + rules.json[105]: abs pow _0 np.pi -> pow _0 np.pi
Lean proof: included
(case sp-acj4-137-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[137] + rules.json[105]: abs pow _0 np.pi -> pow _0 np.pi") (var x real) (assume (or (nonzero x) (> (re pi) 0))) (ask (= (abs (pow x pi)) (pow x pi))) (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 -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r137w2 | 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-14-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[14] + rules.json[10]: neg sin _0 -> sin neg _0
Lean proof: included
(case sp-acj4-14-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[14] + rules.json[10]: neg sin _0 -> sin neg _0") (var x real) (ask (= (- (sin x)) (sin (- x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sin_neg]"))
sp-acj4-145-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[145] + rules.json[113]: abs sin acos _0 -> cos asin _0
Lean proof: included
(case sp-acj4-145-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[145] + rules.json[113]: abs sin acos _0 -> cos asin _0") (var x real) (ask (= (abs (sin (acos x))) (cos (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_r145w2 | 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-162-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[162] + rules.json[119]: acosh rootn _0 5 -> acosh pow _0 0.2
Lean proof: included
(case sp-acj4-162-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[162] + rules.json[119]: acosh rootn _0 5 -> acosh pow _0 0.2") (var x real) (ask (= (acosh (surd x 5)) (acosh (pow x 1/5)))) (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 -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r162w2 | 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-179-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 3\)
SimpliPy acj-4 (MIT) rules_real.json[179] + rules.json[128]: atan sinh acos _0 -> asin tanh acos _0
Lean proof: included
(case sp-acj4-179-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[179] + rules.json[128]: atan sinh acos _0 -> asin tanh acos _0") (var x real) (assume (!= (sinh (acos x)) i)) (assume (!= (sinh (acos x)) (- i))) (assume (nonzero (cosh (acos x)))) (ask (= (atan (sinh (acos x))) (asin (tanh (acos x))))) (expect contingent) (witness true (x 0) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r179w1 | exact AE.w2_r179w1_hI | exact AE.w2_r179w1_hnI | exact AE.w2_r179w1_atanD | exact AE.w2_r179w1_cosh | exact AE.w2_r179w1_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]")) (witness false (x 3) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r179w2 | exact AE.w2_r179_hI | exact AE.w2_r179_hnI | exact AE.w2_r179_atanD | exact AE.w2_r179_cosh | exact AE.w2_r179_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-181-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 3\)
SimpliPy acj-4 (MIT) rules_real.json[181] + rules.json[129]: atan sinh asin _0 -> asin tanh asin _0
Lean proof: included
(case sp-acj4-181-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[181] + rules.json[129]: atan sinh asin _0 -> asin tanh asin _0") (var x real) (assume (!= (sinh (asin x)) i)) (assume (!= (sinh (asin x)) (- i))) (assume (nonzero (cosh (asin x)))) (ask (= (atan (sinh (asin x))) (asin (tanh (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 3) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r181w2 | exact AE.w2_r181_hI | exact AE.w2_r181_hnI | exact AE.w2_r181_atanD | exact AE.w2_r181_cosh | exact AE.w2_r181_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-185-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[185] + rules.json[132]: atan tan cos _0 -> cos _0
Lean proof: included
(case sp-acj4-185-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[185] + rules.json[132]: atan tan cos _0 -> cos _0") (var x real) (assume (nonzero (cos (cos x)))) (assume (!= (tan (cos x)) i)) (assume (!= (tan (cos x)) (- i))) (ask (= (atan (tan (cos x))) (cos x))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨⟨trivial, h1.1.2⟩, by rw [AE.cos_ofReal, AE.tan_ofReal]; exact AE.atan.D_ofReal _⟩, trivial⟩, ?_⟩; rw [AE.cos_ofReal, AE.tan_ofReal, AE.atan_ofReal, Real.arctan_tan (by linarith [Real.neg_one_le_cos r, Real.pi_gt_three]) (by linarith [Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-194-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[194] + rules.json[136]: atanh sin cos _0 -> asinh tan cos _0
Lean proof: included
(case sp-acj4-194-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[194] + rules.json[136]: atanh sin cos _0 -> asinh tan cos _0") (var x real) (assume (!= (sin (cos x)) 1)) (assume (!= (sin (cos x)) -1)) (assume (nonzero (cos (cos x)))) (ask (= (atanh (sin (cos x))) (asinh (tan (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.cos r := (by linarith [Real.neg_one_le_cos r, Real.pi_gt_three]); have hy2 : Real.cos r < Real.pi / 2 := (by linarith [Real.cos_le_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.cos_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.cos r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.cos r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp, by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp, by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp⟩, ?_⟩; rw [AE.cos_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-195-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[195] + rules.json[137]: atanh sin sin _0 -> asinh tan sin _0
Lean proof: included
(case sp-acj4-195-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[195] + rules.json[137]: atanh sin sin _0 -> asinh tan sin _0") (var x real) (assume (!= (sin (sin x)) 1)) (assume (!= (sin (sin x)) -1)) (assume (nonzero (cos (sin x)))) (ask (= (atanh (sin (sin x))) (asinh (tan (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.sin r := (by linarith [Real.neg_one_le_sin r, Real.pi_gt_three]); have hy2 : Real.sin r < Real.pi / 2 := (by linarith [Real.sin_le_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.sin_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.sin r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.sin r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp, by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp, by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp⟩, ?_⟩; rw [AE.sin_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-196-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[196] + rules.json[138]: atanh sin tanh _0 -> asinh tan tanh _0
Lean proof: included
(case sp-acj4-196-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[196] + rules.json[138]: atanh sin tanh _0 -> asinh tan tanh _0") (var x real) (assume (!= (sin (tanh x)) 1)) (assume (!= (sin (tanh x)) -1)) (assume (nonzero (cos (tanh x)))) (ask (= (atanh (sin (tanh x))) (asinh (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.tanh r := (by linarith [Real.neg_one_lt_tanh r, Real.pi_gt_three]); have hy2 : Real.tanh r < Real.pi / 2 := (by linarith [Real.tanh_lt_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.tanh_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.tanh r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.tanh r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp [AE.cosh_ofReal_ne_zero]⟩, ?_⟩; rw [AE.tanh_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-218-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[218] + rules.json[150]: inv / (-6) !0 -> / !0 (-6)
Lean proof: included
(case sp-acj4-218-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[218] + rules.json[150]: inv / (-6) !0 -> / !0 (-6)") (var x real) (assume (nonzero x)) (assume (nonzero (/ -6 x))) (ask (= (/ (/ -6 x)) (/ x -6))) (expect true) (lean-proof "refine ⟨⟨h0.2, h1.2⟩, ?_⟩; have hx : x ≠ 0 := h0.2; simp only [AE.inv_def]; field_simp; try ring"))
sp-acj4-22-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[22] + rules.json[17]: tanh abs _0 -> abs tanh _0
Lean proof: included
(case sp-acj4-22-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[22] + rules.json[17]: tanh abs _0 -> abs tanh _0") (var x real) (ask (= (tanh (abs x)) (abs (tanh x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [AE.abs_ofReal, AE.tanh_ofReal, AE.tanh_ofReal, AE.abs_ofReal]; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; rw [AE.tanh_abs]"))
sp-acj4-220-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[220] + rules.json[152]: inv / (-8) !0 -> / !0 (-8)
Lean proof: included
(case sp-acj4-220-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[220] + rules.json[152]: inv / (-8) !0 -> / !0 (-8)") (var x real) (assume (nonzero x)) (assume (nonzero (/ -8 x))) (ask (= (/ (/ -8 x)) (/ x -8))) (expect true) (lean-proof "refine ⟨⟨h0.2, h1.2⟩, ?_⟩; have hx : x ≠ 0 := h0.2; simp only [AE.inv_def]; field_simp; try ring"))
sp-acj4-233-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[233] + rules.json[162]: inv pow _0 np.pi -> pow _0 neg np.pi
Lean proof: included
(case sp-acj4-233-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[233] + rules.json[162]: inv pow _0 np.pi -> pow _0 neg np.pi") (var x real) (assume (or (nonzero x) (> (re pi) 0))) (assume (nonzero (pow x pi))) (assume (or (nonzero x) (> (re (- pi)) 0))) (ask (= (/ (pow x pi)) (pow x (- pi)))) (expect true) (lean-proof "have hx : x ≠ 0 := (by intro h; apply h1.2; rw [h]; simp); refine ⟨⟨⟨by simp [hx], h1.2⟩, by simp [hx]⟩, ?_⟩; simp only [AE.pow, if_neg hx, AE.inv_def, AE.exp_def]; rw [← Complex.exp_neg]; ring_nf"))
sp-acj4-248-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[248] + rules.json[164]: neg abs asin _0 -> asin neg abs _0
Lean proof: included
(case sp-acj4-248-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[248] + rules.json[164]: neg abs asin _0 -> asin neg abs _0") (var x real) (ask (= (- (abs (asin x))) (asin (- (abs 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_r248w2 | 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-249-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[249] + rules.json[165]: neg abs asinh _0 -> asinh neg abs _0
Lean proof: included
(case sp-acj4-249-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[249] + rules.json[165]: neg abs asinh _0 -> asinh neg abs _0") (var x real) (ask (= (- (abs (asinh x))) (asinh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.asinh_ofReal, AE.asinh_ofReal, AE.abs_ofReal, Real.arsinh_neg, AE.arsinh_abs]; push_cast; ring"))
sp-acj4-251-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[251] + rules.json[167]: neg abs atanh _0 -> atanh neg abs _0
Lean proof: included
(case sp-acj4-251-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[251] + rules.json[167]: neg abs atanh _0 -> atanh neg abs _0") (var x real) (assume (!= x 1)) (assume (!= x -1)) (assume (!= (- (abs x)) 1)) (assume (!= (- (abs x)) -1)) (ask (= (- (abs (atanh x))) (atanh (- (abs 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_r251w2 | 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-252-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[252] + rules.json[168]: neg abs sinh _0 -> sinh neg abs _0
Lean proof: included
(case sp-acj4-252-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[252] + rules.json[168]: neg abs sinh _0 -> sinh neg abs _0") (var x real) (ask (= (- (abs (sinh x))) (sinh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.sinh_ofReal, AE.sinh_ofReal, AE.abs_ofReal, Real.abs_sinh, Real.sinh_neg]; push_cast; ring"))
sp-acj4-253-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[253] + rules.json[169]: neg abs tanh _0 -> tanh neg abs _0
Lean proof: included
(case sp-acj4-253-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[253] + rules.json[169]: neg abs tanh _0 -> tanh neg abs _0") (var x real) (ask (= (- (abs (tanh x))) (tanh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.tanh_ofReal, AE.tanh_ofReal, AE.abs_ofReal, ← AE.tanh_abs, Real.tanh_neg]; push_cast; ring"))
sp-acj4-256-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[256] + rules.json[171]: neg exp neg !0 -> inv neg exp !0
Lean proof: included
(case sp-acj4-256-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[256] + rules.json[171]: neg exp neg !0 -> inv neg exp !0") (var x real) (assume (nonzero (- (exp x)))) (ask (= (- (exp (- x))) (/ (- (exp x))))) (expect true) (lean-proof "refine ⟨h0.2, ?_⟩; simp [Complex.exp_neg]"))
sp-acj4-275-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[275] + rules.json[184]: pow abs _0 (-3) -> abs pow _0 (-3)
Lean proof: included
(case sp-acj4-275-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[275] + rules.json[184]: pow abs _0 (-3) -> abs pow _0 (-3)") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (pow (abs x) -3) (abs (pow x -3)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : (r:ℂ) ≠ 0 := h1.2; have ha : AE.abs (r:ℂ) ≠ 0 := h0.2; refine ⟨⟨⟨by simp, by simp [ha]⟩, by simp [hr], by simp⟩, ?_⟩; rw [AE.pow_neg_ofNat ha, AE.pow_neg_ofNat hr, AE.abs_inv, AE.abs_eq, AE.abs_eq]; simp"))
sp-acj4-276-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[276] + rules.json[185]: pow abs _0 (-4) -> pow _0 (-4)
Lean proof: included
(case sp-acj4-276-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[276] + rules.json[185]: pow abs _0 (-4) -> pow _0 (-4)") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (pow (abs x) -4) (pow x -4))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : (r:ℂ) ≠ 0 := h1.2; have ha : AE.abs (r:ℂ) ≠ 0 := h0.2; refine ⟨⟨⟨by simp, by simp [ha]⟩, by simp [hr]⟩, ?_⟩; rw [AE.pow_neg_ofNat ha, AE.pow_neg_ofNat hr, AE.abs_ofReal]; congr 1; exact_mod_cast (Even.pow_abs ⟨2, by norm_num⟩ r)"))
sp-acj4-283-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[283] + rules.json[192]: pow abs _0 2 -> * _0 _0
Lean proof: included
(case sp-acj4-283-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[283] + rules.json[192]: pow abs _0 2 -> * _0 _0") (var x real) (ask (= (pow (abs x) 2) (* x x))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.abs_ofReal]; exact_mod_cast (by rw [sq_abs]; ring : |r|^2 = r*r)"))
sp-acj4-286-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[286] + rules.json[195]: pow abs _0 5 -> abs pow _0 5
Lean proof: included
(case sp-acj4-286-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[286] + rules.json[195]: pow abs _0 5 -> abs pow _0 5") (var x real) (ask (= (pow (abs x) 5) (abs (pow x 5)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.pow_ofNat_real, AE.abs_ofReal r, ← Complex.ofReal_pow r, AE.abs_ofReal (r^5), abs_pow]; push_cast; ring"))
sp-acj4-289-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[289] + rules.json[198]: pow abs _0 8 -> pow _0 8
Lean proof: included
(case sp-acj4-289-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[289] + rules.json[198]: pow abs _0 8 -> pow _0 8") (var x real) (ask (= (pow (abs x) 8) (pow x 8))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.pow_ofNat_real, AE.abs_ofReal]; exact_mod_cast (Even.pow_abs ⟨4, by norm_num⟩ r)"))
sp-acj4-31-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[31] + rules.json[24]: * 5 abs _0 -> abs * (-5) _0
Lean proof: included
(case sp-acj4-31-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[31] + rules.json[24]: * 5 abs _0 -> abs * (-5) _0") (var x real) (ask (= (* 5 (abs x)) (abs (* -5 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq]"))
sp-acj4-326-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[326] + rules.json[208]: pow exp _0 2 -> exp * 2 _0
Lean proof: included
(case sp-acj4-326-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[326] + rules.json[208]: pow exp _0 2 -> exp * 2 _0") (var x real) (ask (= (pow (exp x) 2) (exp (* 2 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.exp_def, AE.exp_def, ← Complex.exp_nat_mul]; norm_num"))
sp-acj4-33-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[33] + rules.json[26]: * 6 abs _0 -> abs * (-6) _0
Lean proof: included
(case sp-acj4-33-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[33] + rules.json[26]: * 6 abs _0 -> abs * (-6) _0") (var x real) (ask (= (* 6 (abs x)) (abs (* -6 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq]"))
sp-acj4-35-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[35] + rules.json[28]: * 7 log _0 -> log pow _0 7
Lean proof: included
(case sp-acj4-35-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[35] + rules.json[28]: * 7 log _0 -> log pow _0 7") (var x real) (assume (nonzero x)) (assume (nonzero (pow x 7))) (ask (= (* 7 (log x)) (log (pow x 7)))) (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_r35w2 | 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-354-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[354] + rules.json[224]: pow _0 log 5 -> pow 5 log _0
Lean proof: included
(case sp-acj4-354-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[354] + rules.json[224]: pow _0 log 5 -> pow 5 log _0") (var x real) (assume (or (nonzero x) (> (re (log 5)) 0))) (assume (nonzero x)) (ask (= (pow x (log 5)) (pow 5 (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by norm_num, by simp [hx]⟩, hx, by simp⟩, ?_⟩; simp [AE.pow, hx, mul_comm]"))
sp-acj4-356-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[356] + rules.json[226]: pow _0 log 7 -> pow 7 log _0
Lean proof: included
(case sp-acj4-356-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[356] + rules.json[226]: pow _0 log 7 -> pow 7 log _0") (var x real) (assume (or (nonzero x) (> (re (log 7)) 0))) (assume (nonzero x)) (ask (= (pow x (log 7)) (pow 7 (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by norm_num, by simp [hx]⟩, hx, by simp⟩, ?_⟩; simp [AE.pow, hx, mul_comm]"))
sp-acj4-359-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[359] + rules.json[227]: pow _0 log np.pi -> pow np.pi log _0
Lean proof: included
(case sp-acj4-359-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[359] + rules.json[227]: pow _0 log np.pi -> pow np.pi log _0") (var x real) (assume (or (nonzero x) (> (re (log pi)) 0))) (assume (nonzero x)) (ask (= (pow x (log pi)) (pow pi (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by simp [Real.pi_ne_zero], by simp [hx]⟩, hx, by simp [Real.pi_ne_zero]⟩, ?_⟩; simp [AE.pow, hx, Real.pi_ne_zero, mul_comm]"))
sp-acj4-364-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[364] + rules.json[232]: rootn abs _0 3 -> abs rootn _0 3
Lean proof: included
(case sp-acj4-364-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[364] + rules.json[232]: rootn abs _0 3 -> abs rootn _0 3") (var x real) (ask (= (surd (abs x) 3) (abs (surd x 3)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [show (3:ℂ) = ((3:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨AE.abs_isReal _, AE.IsInt.ofInt 3, by norm_num, Or.inr (AE.odd_ofInt ⟨1, by norm_num⟩), Or.inr (by norm_num)⟩⟩, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt 3, by norm_num, Or.inr (AE.odd_ofInt ⟨1, by norm_num⟩), Or.inr (by norm_num)⟩, by simp⟩, ?_⟩; rw [AE.abs_ofReal, AE.surd_abs_odd r (by norm_num)]"))
sp-acj4-367-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[367] + rules.json[235]: rootn abs _0 9 -> abs rootn _0 9
Lean proof: included
(case sp-acj4-367-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[367] + rules.json[235]: rootn abs _0 9 -> abs rootn _0 9") (var x real) (ask (= (surd (abs x) 9) (abs (surd x 9)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [show (9:ℂ) = ((9:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨AE.abs_isReal _, AE.IsInt.ofInt 9, by norm_num, Or.inr (AE.odd_ofInt ⟨4, by norm_num⟩), Or.inr (by norm_num)⟩⟩, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt 9, by norm_num, Or.inr (AE.odd_ofInt ⟨4, by norm_num⟩), Or.inr (by norm_num)⟩, by simp⟩, ?_⟩; rw [AE.abs_ofReal, AE.surd_abs_odd r (by norm_num)]"))
sp-acj4-368-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[368] + rules.json[236]: rootn acos _0 (-5) -> pow acos _0 -0.2
Lean proof: included
(case sp-acj4-368-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[368] + rules.json[236]: rootn acos _0 (-5) -> pow acos _0 -0.2") (var x real) (assume (real (acos x))) (assume (nonzero (acos x))) (ask (= (surd (acos x) -5) (pow (acos x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.mem_Icc_of_acos_real (by simpa using h0.2); rw [AE.acos_ofReal hI.1 hI.2]; have ha : 0 ≤ Real.arccos r := Real.arccos_nonneg r; have hne : Real.arccos r ≠ 0 := (by have := h1.2; rw [AE.acos_ofReal hI.1 hI.2] at this; intro h; exact this (by rw [h]; simp)); rw [show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inl (by exact_mod_cast hne)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hne)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inl hne)]"))
sp-acj4-369-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[369] + rules.json[237]: rootn acos _0 5 -> pow acos _0 0.2
Lean proof: included
(case sp-acj4-369-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[369] + rules.json[237]: rootn acos _0 5 -> pow acos _0 0.2") (var x real) (assume (real (acos x))) (ask (= (surd (acos x) 5) (pow (acos x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.mem_Icc_of_acos_real (by simpa using h0.2); rw [AE.acos_ofReal hI.1 hI.2]; have ha : 0 ≤ Real.arccos r := Real.arccos_nonneg r; rw [show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inr (by norm_num)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inr (by norm_num)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inr (by norm_num))]"))
sp-acj4-370-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[370] + rules.json[238]: rootn acosh _0 (-5) -> pow acosh _0 -0.2
Lean proof: included
(case sp-acj4-370-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[370] + rules.json[238]: rootn acosh _0 (-5) -> pow acosh _0 -0.2") (var x real) (assume (real (acosh x))) (assume (nonzero (acosh x))) (ask (= (surd (acosh x) -5) (pow (acosh x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.one_le_of_acosh_real (by simpa using h0.2); rw [AE.acosh_ofReal hI]; have ha : 0 ≤ Real.arcosh r := AE.arcosh_nonneg hI; have hne : Real.arcosh r ≠ 0 := (by have := h1.2; rw [AE.acosh_ofReal hI] at this; intro h; exact this (by rw [h]; simp)); rw [show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inl (by exact_mod_cast hne)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hne)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inl hne)]"))
sp-acj4-371-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[371] + rules.json[239]: rootn acosh _0 5 -> pow acosh _0 0.2
Lean proof: included
(case sp-acj4-371-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[371] + rules.json[239]: rootn acosh _0 5 -> pow acosh _0 0.2") (var x real) (assume (real (acosh x))) (ask (= (surd (acosh x) 5) (pow (acosh x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.one_le_of_acosh_real (by simpa using h0.2); rw [AE.acosh_ofReal hI]; have ha : 0 ≤ Real.arcosh r := AE.arcosh_nonneg hI; rw [show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inr (by norm_num)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inr (by norm_num)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inr (by norm_num))]"))
sp-acj4-372-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[372] + rules.json[240]: rootn cosh _0 (-5) -> pow cosh _0 -0.2
Lean proof: included
(case sp-acj4-372-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[372] + rules.json[240]: rootn cosh _0 (-5) -> pow cosh _0 -0.2") (var x real) (assume (nonzero (cosh x))) (ask (= (surd (cosh x) -5) (pow (cosh x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hc := Real.cosh_pos r; rw [AE.cosh_ofReal, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨trivial, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simp; positivity), Or.inl (by exact_mod_cast hc.ne')⟩⟩, trivial, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hc.ne')⟩, ?_⟩; rw [AE.surd_ofReal_nonneg hc.le (by norm_num), show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, AE.pow_ofReal hc.le (Or.inl hc.ne')]"))
sp-acj4-373-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[373] + rules.json[241]: rootn cosh _0 5 -> pow cosh _0 0.2
Lean proof: included
(case sp-acj4-373-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[373] + rules.json[241]: rootn cosh _0 5 -> pow cosh _0 0.2") (var x real) (ask (= (surd (cosh x) 5) (pow (cosh x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hc := Real.cosh_pos r; rw [AE.cosh_ofReal, show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨trivial, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simp; positivity), Or.inl (by exact_mod_cast hc.ne')⟩⟩, trivial, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hc.ne')⟩, ?_⟩; rw [AE.surd_ofReal_nonneg hc.le (by norm_num), AE.pow_ofReal hc.le (Or.inl hc.ne')]"))
sp-acj4-38-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[38] + rules.json[31]: * 9 log _0 -> log pow _0 9
Lean proof: included
(case sp-acj4-38-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[38] + rules.json[31]: * 9 log _0 -> log pow _0 9") (var x real) (assume (nonzero x)) (assume (nonzero (pow x 9))) (ask (= (* 9 (log x)) (log (pow 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_r38w2 | 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-394-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[394] + rules.json[242]: sin abs atanh _0 -> abs sin atanh _0
Lean proof: included
(case sp-acj4-394-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[394] + rules.json[242]: sin abs atanh _0 -> abs sin atanh _0") (var x real) (assume (!= x 1)) (assume (!= x -1)) (ask (= (sin (abs (atanh x))) (abs (sin (atanh 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_r394w2 | 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-395-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[395] + rules.json[243]: sin abs cos _0 -> abs sin cos _0
Lean proof: included
(case sp-acj4-395-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[395] + rules.json[243]: sin abs cos _0 -> abs sin cos _0") (var x real) (ask (= (sin (abs (cos x))) (abs (sin (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.cos_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [Real.neg_one_le_cos r, Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-396-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[396] + rules.json[244]: sin abs sin _0 -> abs sin sin _0
Lean proof: included
(case sp-acj4-396-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[396] + rules.json[244]: sin abs sin _0 -> abs sin sin _0") (var x real) (ask (= (sin (abs (sin x))) (abs (sin (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.sin_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [Real.neg_one_le_sin r, Real.sin_le_one r, Real.pi_gt_three])]"))
sp-acj4-397-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[397] + rules.json[245]: sin abs tanh _0 -> abs sin tanh _0
Lean proof: included
(case sp-acj4-397-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[397] + rules.json[245]: sin abs tanh _0 -> abs sin tanh _0") (var x real) (ask (= (sin (abs (tanh x))) (abs (sin (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.tanh_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [(Real.neg_one_lt_tanh r).le, (Real.tanh_lt_one r).le, Real.pi_gt_three])]"))
sp-acj4-402-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[402] + rules.json[246]: sin atanh abs _0 -> abs sin atanh _0
Lean proof: included
(case sp-acj4-402-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[402] + rules.json[246]: sin atanh abs _0 -> abs sin atanh _0") (var x real) (assume (!= (abs x) 1)) (assume (!= x 1)) (assume (!= x -1)) (ask (= (sin (atanh (abs x))) (abs (sin (atanh 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_r402w2 | 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-404-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[404] + rules.json[247]: sin tanh abs _0 -> abs sin tanh _0
Lean proof: included
(case sp-acj4-404-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[404] + rules.json[247]: sin tanh abs _0 -> abs sin tanh _0") (var x real) (ask (= (sin (tanh (abs x))) (abs (sin (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.tanh_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.tanh_abs, AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [(Real.neg_one_lt_tanh r).le, (Real.tanh_lt_one r).le, Real.pi_gt_three])]"))
sp-acj4-412-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[412] + rules.json[253]: tan abs asin _0 -> abs tan asin _0
Lean proof: included
(case sp-acj4-412-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[412] + rules.json[253]: tan abs asin _0 -> abs tan asin _0") (var x real) (assume (nonzero (cos (abs (asin x))))) (assume (nonzero (cos (asin x)))) (ask (= (tan (abs (asin x))) (abs (tan (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_r412w2 | exact AE.w2_r412_cos | exact AE.w2_r412_tanD | 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_asin_two]")))
sp-acj4-413-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[413] + rules.json[254]: tan abs cos _0 -> abs tan cos _0
Lean proof: included
(case sp-acj4-413-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[413] + rules.json[254]: tan abs cos _0 -> abs tan cos _0") (var x real) (assume (nonzero (cos (abs (cos x))))) (assume (nonzero (cos (cos x)))) (ask (= (tan (abs (cos x))) (abs (tan (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.cos_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_le_cos r, Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-414-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[414] + rules.json[255]: tan abs sin _0 -> abs tan sin _0
Lean proof: included
(case sp-acj4-414-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[414] + rules.json[255]: tan abs sin _0 -> abs tan sin _0") (var x real) (assume (nonzero (cos (abs (sin x))))) (assume (nonzero (cos (sin x)))) (ask (= (tan (abs (sin x))) (abs (tan (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.sin_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_le_sin r, Real.sin_le_one r, Real.pi_gt_three])]"))
sp-acj4-415-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[415] + rules.json[256]: tan abs tanh _0 -> abs tan tanh _0
Lean proof: included
(case sp-acj4-415-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[415] + rules.json[256]: tan abs tanh _0 -> abs tan tanh _0") (var x real) (assume (nonzero (cos (abs (tanh x))))) (assume (nonzero (cos (tanh x)))) (ask (= (tan (abs (tanh x))) (abs (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.tanh_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_lt_tanh r, Real.tanh_lt_one r, Real.pi_gt_three])]"))
sp-acj4-417-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[417] + rules.json[257]: tan asin abs _0 -> abs tan asin _0
Lean proof: included
(case sp-acj4-417-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[417] + rules.json[257]: tan asin abs _0 -> abs tan asin _0") (var x real) (assume (nonzero (cos (asin (abs x))))) (assume (nonzero (cos (asin x)))) (ask (= (tan (asin (abs x))) (abs (tan (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_r417w2 | 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_asin_two]")))
sp-acj4-421-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[421] + rules.json[260]: tan tanh abs _0 -> abs tan tanh _0
Lean proof: included
(case sp-acj4-421-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[421] + rules.json[260]: tan tanh abs _0 -> abs tan tanh _0") (var x real) (assume (nonzero (cos (tanh (abs x))))) (assume (nonzero (cos (tanh x)))) (ask (= (tan (tanh (abs x))) (abs (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.abs_ofReal, AE.tanh_ofReal, AE.tan_ofReal]; rw [AE.tanh_abs, AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_lt_tanh r, Real.tanh_lt_one r, Real.pi_gt_three])]"))
sp-acj4-5-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[5] + rules.json[3]: atanh abs _0 -> abs atanh _0
Lean proof: included
(case sp-acj4-5-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[5] + rules.json[3]: atanh abs _0 -> abs atanh _0") (var x real) (assume (!= (abs x) 1)) (assume (!= x 1)) (assume (!= x -1)) (ask (= (atanh (abs x)) (abs (atanh 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_r5w2 | 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-73-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[73] + rules.json[52]: / (-1) abs !0 -> inv neg abs !0
Lean proof: included
(case sp-acj4-73-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[73] + rules.json[52]: / (-1) abs !0 -> inv neg abs !0") (var x real) (assume (nonzero (abs x))) (assume (nonzero (- (abs x)))) (ask (= (/ -1 (abs x)) (/ (- (abs x))))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-80-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[80] + rules.json[59]: / (-1) cos _0 -> inv neg cos _0
Lean proof: included
(case sp-acj4-80-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[80] + rules.json[59]: / (-1) cos _0 -> inv neg cos _0") (var x real) (assume (nonzero (cos x))) (assume (nonzero (- (cos x)))) (ask (= (/ -1 (cos x)) (/ (- (cos x))))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-83-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[83] + rules.json[62]: / (-1) log !0 -> inv neg log !0
Lean proof: included
(case sp-acj4-83-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[83] + rules.json[62]: / (-1) log !0 -> inv neg log !0") (var x real) (assume (nonzero x)) (assume (nonzero (log x))) (assume (nonzero (- (log x)))) (ask (= (/ -1 (log x)) (/ (- (log x))))) (expect true) (lean-proof "refine ⟨⟨⟨h0.2, h1.2⟩, h0.2, h2.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-86-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[86] + rules.json[65]: / (-1) tan !0 -> inv neg tan !0
Lean proof: included
(case sp-acj4-86-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[86] + rules.json[65]: / (-1) tan !0 -> inv neg tan !0") (var x real) (assume (nonzero (cos x))) (assume (nonzero (tan x))) (assume (nonzero (- (tan x)))) (ask (= (/ -1 (tan x)) (/ (- (tan x))))) (expect true) (lean-proof "refine ⟨⟨⟨h1.1.1, h1.2⟩, h1.1.1, h2.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-90-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[90] + rules.json[69]: / 3 abs _0 -> abs / (-3) _0
Lean proof: included
(case sp-acj4-90-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[90] + rules.json[69]: / 3 abs _0 -> abs / (-3) _0") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (/ 3 (abs x)) (abs (/ -3 x)))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, h1.2, by simp⟩, ?_⟩; simp [AE.abs_eq, div_eq_mul_inv]"))
sp-acj4-99-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[99] + rules.json[78]: / abs _0 3 -> abs / _0 (-3)
Lean proof: included
(case sp-acj4-99-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[99] + rules.json[78]: / abs _0 3 -> abs / _0 (-3)") (var x real) (ask (= (/ (abs x) 3) (abs (/ x -3)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq, div_eq_mul_inv]"))
Case set ee702ae2fe06
sp-acj4-1-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[1] + rules.json[0]: asin abs _0 -> abs asin _0
Lean proof: included
(case sp-acj4-1-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[1] + rules.json[0]: asin abs _0 -> abs asin _0") (var x real) (ask (= (asin (abs 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_r1w2 | 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-102-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[102] + rules.json[81]: / abs _0 6 -> abs / _0 (-6)
Lean proof: included
(case sp-acj4-102-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[102] + rules.json[81]: / abs _0 6 -> abs / _0 (-6)") (var x real) (ask (= (/ (abs x) 6) (abs (/ x -6)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq, div_eq_mul_inv]"))
sp-acj4-108-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[108] + rules.json[87]: / abs _0 _0 -> / _0 abs _0
Lean proof: included
(case sp-acj4-108-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[108] + rules.json[87]: / abs _0 _0 -> / _0 abs _0") (var x real) (assume (nonzero x)) (assume (nonzero (abs x))) (ask (= (/ (abs x) x) (/ x (abs x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; have hr : (r:ℂ) ≠ 0 := h0.2; have ha : ((|r|:ℝ):ℂ) ≠ 0 := (by have := h1.2; rwa [AE.abs_ofReal] at this); simp only [AE.abs_ofReal, AE.inv_def]; rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_eq_div_iff hr ha]; exact_mod_cast (abs_mul_abs_self r)"))
sp-acj4-120-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[120] + rules.json[92]: / np.pi abs _0 -> abs / np.pi _0
Lean proof: included
(case sp-acj4-120-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[120] + rules.json[92]: / np.pi abs _0 -> abs / np.pi _0") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (/ pi (abs x)) (abs (/ pi x)))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, h1.2, by simp⟩, ?_⟩; simp [AE.abs_eq, abs_of_pos Real.pi_pos]"))
sp-acj4-127-real
equal at some admissible points, different at others
witness (true): \(x = -1\)
witness (false): \(x = 1\)
SimpliPy acj-4 (MIT) rules_real.json[127] + rules.json[96]: abs atanh exp _0 -> atanh exp _0
Lean proof: included
(case sp-acj4-127-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[127] + rules.json[96]: abs atanh exp _0 -> atanh exp _0") (var x real) (assume (!= (exp x) 1)) (assume (!= (exp x) -1)) (ask (= (abs (atanh (exp x))) (atanh (exp x)))) (expect contingent) (witness true (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r127w1 | exact AE.w2_exp_neg_one_ne_one | exact AE.w2_exp_neg_one_ne_neg_one | exact AE.w2_atanhD_exp_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]")) (witness false (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r127w2 | exact AE.w2_exp_one_ne_one | exact AE.w2_exp_one_ne_neg_one | exact AE.w2_atanhD_exp_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-128-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[128] + rules.json[97]: abs cos asin _0 -> cos asin _0
Lean proof: included
(case sp-acj4-128-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[128] + rules.json[97]: abs cos asin _0 -> cos asin _0") (var x real) (ask (= (abs (cos (asin x))) (cos (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_r128w2 | 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-131-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[131] + rules.json[99]: abs log cosh _0 -> log cosh _0
Lean proof: included
(case sp-acj4-131-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[131] + rules.json[99]: abs log cosh _0 -> log cosh _0") (var x real) (assume (nonzero (cosh x))) (ask (= (abs (log (cosh x))) (log (cosh x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨⟨trivial, h0.2⟩, by simp⟩, trivial, h0.2⟩, ?_⟩; rw [AE.cosh_ofReal, AE.log_ofReal (Real.cosh_pos r).le, AE.abs_ofReal, abs_of_nonneg (Real.log_nonneg (Real.one_le_cosh r))]"))
sp-acj4-132-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[132] + rules.json[100]: abs log sin _0 -> neg log sin _0
Lean proof: included
(case sp-acj4-132-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[132] + rules.json[100]: abs log sin _0 -> neg log sin _0") (var x real) (assume (nonzero (sin x))) (ask (= (abs (log (sin x))) (- (log (sin x))))) (expect contingent) (witness true (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r132w1 | exact AE.w2_sin_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) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r132w2 | exact AE.w2_sin_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]")))
sp-acj4-133-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[133] + rules.json[101]: abs log tanh _0 -> neg log tanh _0
Lean proof: included
(case sp-acj4-133-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[133] + rules.json[101]: abs log tanh _0 -> neg log tanh _0") (var x real) (assume (nonzero (tanh x))) (ask (= (abs (log (tanh x))) (- (log (tanh x))))) (expect contingent) (witness true (x 1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r133w1 | exact AE.w2_tanh_one_ne | exact AE.w2_tanhD_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]")) (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r133w2 | exact AE.w2_tanh_neg_one_ne | exact AE.w2_tanhD_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-136-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[136] + rules.json[104]: abs pow _0 np.e -> pow _0 np.e
Lean proof: included
(case sp-acj4-136-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[136] + rules.json[104]: abs pow _0 np.e -> pow _0 np.e") (var x real) (assume (or (nonzero x) (> (re (exp 1)) 0))) (ask (= (abs (pow x (exp 1))) (pow x (exp 1)))) (expect contingent) (witness true (x 0) (lean-proof "constructorm* _ ∧ _ <;> first | 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, Complex.exp_im]")) (witness false (x -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r136w2 | 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-137-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[137] + rules.json[105]: abs pow _0 np.pi -> pow _0 np.pi
Lean proof: included
(case sp-acj4-137-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[137] + rules.json[105]: abs pow _0 np.pi -> pow _0 np.pi") (var x real) (assume (or (nonzero x) (> (re pi) 0))) (ask (= (abs (pow x pi)) (pow x pi))) (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 -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r137w2 | 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-14-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[14] + rules.json[10]: neg sin _0 -> sin neg _0
Lean proof: included
(case sp-acj4-14-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[14] + rules.json[10]: neg sin _0 -> sin neg _0") (var x real) (ask (= (- (sin x)) (sin (- x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [Complex.sin_neg]"))
sp-acj4-145-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[145] + rules.json[113]: abs sin acos _0 -> cos asin _0
Lean proof: included
(case sp-acj4-145-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[145] + rules.json[113]: abs sin acos _0 -> cos asin _0") (var x real) (ask (= (abs (sin (acos x))) (cos (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_r145w2 | 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-162-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[162] + rules.json[119]: acosh rootn _0 5 -> acosh pow _0 0.2
Lean proof: included
(case sp-acj4-162-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[162] + rules.json[119]: acosh rootn _0 5 -> acosh pow _0 0.2") (var x real) (ask (= (acosh (surd x 5)) (acosh (pow x 1/5)))) (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 -1) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r162w2 | 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-179-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 3\)
SimpliPy acj-4 (MIT) rules_real.json[179] + rules.json[128]: atan sinh acos _0 -> asin tanh acos _0
Lean proof: included
(case sp-acj4-179-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[179] + rules.json[128]: atan sinh acos _0 -> asin tanh acos _0") (var x real) (assume (!= (sinh (acos x)) i)) (assume (!= (sinh (acos x)) (- i))) (assume (nonzero (cosh (acos x)))) (ask (= (atan (sinh (acos x))) (asin (tanh (acos x))))) (expect contingent) (witness true (x 0) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r179w1 | exact AE.w2_r179w1_hI | exact AE.w2_r179w1_hnI | exact AE.w2_r179w1_atanD | exact AE.w2_r179w1_cosh | exact AE.w2_r179w1_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]")) (witness false (x 3) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r179w2 | exact AE.w2_r179_hI | exact AE.w2_r179_hnI | exact AE.w2_r179_atanD | exact AE.w2_r179_cosh | exact AE.w2_r179_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-181-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 3\)
SimpliPy acj-4 (MIT) rules_real.json[181] + rules.json[129]: atan sinh asin _0 -> asin tanh asin _0
Lean proof: included
(case sp-acj4-181-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[181] + rules.json[129]: atan sinh asin _0 -> asin tanh asin _0") (var x real) (assume (!= (sinh (asin x)) i)) (assume (!= (sinh (asin x)) (- i))) (assume (nonzero (cosh (asin x)))) (ask (= (atan (sinh (asin x))) (asin (tanh (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 3) (lean-proof "constructorm* _ ∧ _ <;> first | exact AE.w2_r181w2 | exact AE.w2_r181_hI | exact AE.w2_r181_hnI | exact AE.w2_r181_atanD | exact AE.w2_r181_cosh | exact AE.w2_r181_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-185-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[185] + rules.json[132]: atan tan cos _0 -> cos _0
Lean proof: included
(case sp-acj4-185-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[185] + rules.json[132]: atan tan cos _0 -> cos _0") (var x real) (assume (nonzero (cos (cos x)))) (assume (!= (tan (cos x)) i)) (assume (!= (tan (cos x)) (- i))) (ask (= (atan (tan (cos x))) (cos x))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨⟨trivial, h1.1.2⟩, by rw [AE.cos_ofReal, AE.tan_ofReal]; exact AE.atan.D_ofReal _⟩, trivial⟩, ?_⟩; rw [AE.cos_ofReal, AE.tan_ofReal, AE.atan_ofReal, Real.arctan_tan (by linarith [Real.neg_one_le_cos r, Real.pi_gt_three]) (by linarith [Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-194-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[194] + rules.json[136]: atanh sin cos _0 -> asinh tan cos _0
Lean proof: included
(case sp-acj4-194-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[194] + rules.json[136]: atanh sin cos _0 -> asinh tan cos _0") (var x real) (assume (!= (sin (cos x)) 1)) (assume (!= (sin (cos x)) -1)) (assume (nonzero (cos (cos x)))) (ask (= (atanh (sin (cos x))) (asinh (tan (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.cos r := (by linarith [Real.neg_one_le_cos r, Real.pi_gt_three]); have hy2 : Real.cos r < Real.pi / 2 := (by linarith [Real.cos_le_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.cos_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.cos r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.cos r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp, by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp, by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp⟩, ?_⟩; rw [AE.cos_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-195-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[195] + rules.json[137]: atanh sin sin _0 -> asinh tan sin _0
Lean proof: included
(case sp-acj4-195-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[195] + rules.json[137]: atanh sin sin _0 -> asinh tan sin _0") (var x real) (assume (!= (sin (sin x)) 1)) (assume (!= (sin (sin x)) -1)) (assume (nonzero (cos (sin x)))) (ask (= (atanh (sin (sin x))) (asinh (tan (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.sin r := (by linarith [Real.neg_one_le_sin r, Real.pi_gt_three]); have hy2 : Real.sin r < Real.pi / 2 := (by linarith [Real.sin_le_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.sin_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.sin r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.sin r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp, by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp, by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp⟩, ?_⟩; rw [AE.sin_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-196-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[196] + rules.json[138]: atanh sin tanh _0 -> asinh tan tanh _0
Lean proof: included
(case sp-acj4-196-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[196] + rules.json[138]: atanh sin tanh _0 -> asinh tan tanh _0") (var x real) (assume (!= (sin (tanh x)) 1)) (assume (!= (sin (tanh x)) -1)) (assume (nonzero (cos (tanh x)))) (ask (= (atanh (sin (tanh x))) (asinh (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hy1 : -(Real.pi / 2) < Real.tanh r := (by linarith [Real.neg_one_lt_tanh r, Real.pi_gt_three]); have hy2 : Real.tanh r < Real.pi / 2 := (by linarith [Real.tanh_lt_one r, Real.pi_gt_three]); have ha := h0.2; have hb := h1.2; rw [AE.tanh_ofReal, AE.sin_ofReal] at ha hb; have ha' : Real.sin (Real.tanh r) ≠ 1 := (by exact_mod_cast ha); have hb' : Real.sin (Real.tanh r) ≠ -1 := (by exact_mod_cast hb); refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.atanh.D_iff]; exact ⟨h0.2, h1.2⟩⟩, ⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h2.2⟩, by simp [AE.cosh_ofReal_ne_zero]⟩, ?_⟩; rw [AE.tanh_ofReal, AE.sin_ofReal, AE.tan_ofReal, AE.atanh_ofReal (lt_of_le_of_ne (Real.neg_one_le_sin _) hb'.symm) (lt_of_le_of_ne (Real.sin_le_one _) ha'), AE.asinh_ofReal, AE.artanh_sin_eq_arsinh_tan hy1 hy2]"))
sp-acj4-218-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[218] + rules.json[150]: inv / (-6) !0 -> / !0 (-6)
Lean proof: included
(case sp-acj4-218-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[218] + rules.json[150]: inv / (-6) !0 -> / !0 (-6)") (var x real) (assume (nonzero x)) (assume (nonzero (/ -6 x))) (ask (= (/ (/ -6 x)) (/ x -6))) (expect true) (lean-proof "refine ⟨⟨h0.2, h1.2⟩, ?_⟩; have hx : x ≠ 0 := h0.2; simp only [AE.inv_def]; field_simp; try ring"))
sp-acj4-22-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[22] + rules.json[17]: tanh abs _0 -> abs tanh _0
Lean proof: included
(case sp-acj4-22-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[22] + rules.json[17]: tanh abs _0 -> abs tanh _0") (var x real) (ask (= (tanh (abs x)) (abs (tanh x)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [AE.abs_ofReal, AE.tanh_ofReal, AE.tanh_ofReal, AE.abs_ofReal]; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; rw [AE.tanh_abs]"))
sp-acj4-220-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[220] + rules.json[152]: inv / (-8) !0 -> / !0 (-8)
Lean proof: included
(case sp-acj4-220-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[220] + rules.json[152]: inv / (-8) !0 -> / !0 (-8)") (var x real) (assume (nonzero x)) (assume (nonzero (/ -8 x))) (ask (= (/ (/ -8 x)) (/ x -8))) (expect true) (lean-proof "refine ⟨⟨h0.2, h1.2⟩, ?_⟩; have hx : x ≠ 0 := h0.2; simp only [AE.inv_def]; field_simp; try ring"))
sp-acj4-233-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[233] + rules.json[162]: inv pow _0 np.pi -> pow _0 neg np.pi
Lean proof: included
(case sp-acj4-233-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[233] + rules.json[162]: inv pow _0 np.pi -> pow _0 neg np.pi") (var x real) (assume (or (nonzero x) (> (re pi) 0))) (assume (nonzero (pow x pi))) (assume (or (nonzero x) (> (re (- pi)) 0))) (ask (= (/ (pow x pi)) (pow x (- pi)))) (expect true) (lean-proof "have hx : x ≠ 0 := (by intro h; apply h1.2; rw [h]; simp); refine ⟨⟨⟨by simp [hx], h1.2⟩, by simp [hx]⟩, ?_⟩; simp only [AE.pow, if_neg hx, AE.inv_def, AE.exp_def]; rw [← Complex.exp_neg]; ring_nf"))
sp-acj4-248-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[248] + rules.json[164]: neg abs asin _0 -> asin neg abs _0
Lean proof: included
(case sp-acj4-248-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[248] + rules.json[164]: neg abs asin _0 -> asin neg abs _0") (var x real) (ask (= (- (abs (asin x))) (asin (- (abs 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_r248w2 | 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-249-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[249] + rules.json[165]: neg abs asinh _0 -> asinh neg abs _0
Lean proof: included
(case sp-acj4-249-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[249] + rules.json[165]: neg abs asinh _0 -> asinh neg abs _0") (var x real) (ask (= (- (abs (asinh x))) (asinh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.asinh_ofReal, AE.asinh_ofReal, AE.abs_ofReal, Real.arsinh_neg, AE.arsinh_abs]; push_cast; ring"))
sp-acj4-251-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[251] + rules.json[167]: neg abs atanh _0 -> atanh neg abs _0
Lean proof: included
(case sp-acj4-251-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[251] + rules.json[167]: neg abs atanh _0 -> atanh neg abs _0") (var x real) (assume (!= x 1)) (assume (!= x -1)) (assume (!= (- (abs x)) 1)) (assume (!= (- (abs x)) -1)) (ask (= (- (abs (atanh x))) (atanh (- (abs 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_r251w2 | 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-252-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[252] + rules.json[168]: neg abs sinh _0 -> sinh neg abs _0
Lean proof: included
(case sp-acj4-252-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[252] + rules.json[168]: neg abs sinh _0 -> sinh neg abs _0") (var x real) (ask (= (- (abs (sinh x))) (sinh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.sinh_ofReal, AE.sinh_ofReal, AE.abs_ofReal, Real.abs_sinh, Real.sinh_neg]; push_cast; ring"))
sp-acj4-253-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[253] + rules.json[169]: neg abs tanh _0 -> tanh neg abs _0
Lean proof: included
(case sp-acj4-253-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[253] + rules.json[169]: neg abs tanh _0 -> tanh neg abs _0") (var x real) (ask (= (- (abs (tanh x))) (tanh (- (abs x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], ?_⟩; rw [AE.abs_ofReal r, ← Complex.ofReal_neg |r|, AE.tanh_ofReal, AE.tanh_ofReal, AE.abs_ofReal, ← AE.tanh_abs, Real.tanh_neg]; push_cast; ring"))
sp-acj4-256-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[256] + rules.json[171]: neg exp neg !0 -> inv neg exp !0
Lean proof: included
(case sp-acj4-256-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[256] + rules.json[171]: neg exp neg !0 -> inv neg exp !0") (var x real) (assume (nonzero (- (exp x)))) (ask (= (- (exp (- x))) (/ (- (exp x))))) (expect true) (lean-proof "refine ⟨h0.2, ?_⟩; simp [Complex.exp_neg]"))
sp-acj4-275-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[275] + rules.json[184]: pow abs _0 (-3) -> abs pow _0 (-3)
Lean proof: included
(case sp-acj4-275-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[275] + rules.json[184]: pow abs _0 (-3) -> abs pow _0 (-3)") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (pow (abs x) -3) (abs (pow x -3)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : (r:ℂ) ≠ 0 := h1.2; have ha : AE.abs (r:ℂ) ≠ 0 := h0.2; refine ⟨⟨⟨by simp, by simp [ha]⟩, by simp [hr], by simp⟩, ?_⟩; rw [AE.pow_neg_ofNat ha, AE.pow_neg_ofNat hr, AE.abs_inv, AE.abs_eq, AE.abs_eq]; simp"))
sp-acj4-276-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[276] + rules.json[185]: pow abs _0 (-4) -> pow _0 (-4)
Lean proof: included
(case sp-acj4-276-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[276] + rules.json[185]: pow abs _0 (-4) -> pow _0 (-4)") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (pow (abs x) -4) (pow x -4))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hr : (r:ℂ) ≠ 0 := h1.2; have ha : AE.abs (r:ℂ) ≠ 0 := h0.2; refine ⟨⟨⟨by simp, by simp [ha]⟩, by simp [hr]⟩, ?_⟩; rw [AE.pow_neg_ofNat ha, AE.pow_neg_ofNat hr, AE.abs_ofReal]; congr 1; exact_mod_cast (Even.pow_abs ⟨2, by norm_num⟩ r)"))
sp-acj4-283-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[283] + rules.json[192]: pow abs _0 2 -> * _0 _0
Lean proof: included
(case sp-acj4-283-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[283] + rules.json[192]: pow abs _0 2 -> * _0 _0") (var x real) (ask (= (pow (abs x) 2) (* x x))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.abs_ofReal]; exact_mod_cast (by rw [sq_abs]; ring : |r|^2 = r*r)"))
sp-acj4-286-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[286] + rules.json[195]: pow abs _0 5 -> abs pow _0 5
Lean proof: included
(case sp-acj4-286-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[286] + rules.json[195]: pow abs _0 5 -> abs pow _0 5") (var x real) (ask (= (pow (abs x) 5) (abs (pow x 5)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.pow_ofNat_real, AE.abs_ofReal r, ← Complex.ofReal_pow r, AE.abs_ofReal (r^5), abs_pow]; push_cast; ring"))
sp-acj4-289-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[289] + rules.json[198]: pow abs _0 8 -> pow _0 8
Lean proof: included
(case sp-acj4-289-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[289] + rules.json[198]: pow abs _0 8 -> pow _0 8") (var x real) (ask (= (pow (abs x) 8) (pow x 8))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.pow_ofNat_real, AE.abs_ofReal]; exact_mod_cast (Even.pow_abs ⟨4, by norm_num⟩ r)"))
sp-acj4-31-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[31] + rules.json[24]: * 5 abs _0 -> abs * (-5) _0
Lean proof: included
(case sp-acj4-31-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[31] + rules.json[24]: * 5 abs _0 -> abs * (-5) _0") (var x real) (ask (= (* 5 (abs x)) (abs (* -5 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq]"))
sp-acj4-326-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[326] + rules.json[208]: pow exp _0 2 -> exp * 2 _0
Lean proof: included
(case sp-acj4-326-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[326] + rules.json[208]: pow exp _0 2 -> exp * 2 _0") (var x real) (ask (= (pow (exp x) 2) (exp (* 2 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; rw [AE.pow_ofNat_real, AE.exp_def, AE.exp_def, ← Complex.exp_nat_mul]; norm_num"))
sp-acj4-33-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[33] + rules.json[26]: * 6 abs _0 -> abs * (-6) _0
Lean proof: included
(case sp-acj4-33-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[33] + rules.json[26]: * 6 abs _0 -> abs * (-6) _0") (var x real) (ask (= (* 6 (abs x)) (abs (* -6 x)))) (expect true) (lean-proof "refine ⟨by simp, ?_⟩; simp [AE.abs_eq]"))
sp-acj4-35-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[35] + rules.json[28]: * 7 log _0 -> log pow _0 7
Lean proof: included
(case sp-acj4-35-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[35] + rules.json[28]: * 7 log _0 -> log pow _0 7") (var x real) (assume (nonzero x)) (assume (nonzero (pow x 7))) (ask (= (* 7 (log x)) (log (pow x 7)))) (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_r35w2 | 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-354-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[354] + rules.json[224]: pow _0 log 5 -> pow 5 log _0
Lean proof: included
(case sp-acj4-354-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[354] + rules.json[224]: pow _0 log 5 -> pow 5 log _0") (var x real) (assume (or (nonzero x) (> (re (log 5)) 0))) (assume (nonzero x)) (ask (= (pow x (log 5)) (pow 5 (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by norm_num, by simp [hx]⟩, hx, by simp⟩, ?_⟩; simp [AE.pow, hx, mul_comm]"))
sp-acj4-356-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[356] + rules.json[226]: pow _0 log 7 -> pow 7 log _0
Lean proof: included
(case sp-acj4-356-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[356] + rules.json[226]: pow _0 log 7 -> pow 7 log _0") (var x real) (assume (or (nonzero x) (> (re (log 7)) 0))) (assume (nonzero x)) (ask (= (pow x (log 7)) (pow 7 (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by norm_num, by simp [hx]⟩, hx, by simp⟩, ?_⟩; simp [AE.pow, hx, mul_comm]"))
sp-acj4-359-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[359] + rules.json[227]: pow _0 log np.pi -> pow np.pi log _0
Lean proof: included
(case sp-acj4-359-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[359] + rules.json[227]: pow _0 log np.pi -> pow np.pi log _0") (var x real) (assume (or (nonzero x) (> (re (log pi)) 0))) (assume (nonzero x)) (ask (= (pow x (log pi)) (pow pi (log x)))) (expect true) (lean-proof "have hx : x ≠ 0 := h1.2; refine ⟨⟨⟨by simp [Real.pi_ne_zero], by simp [hx]⟩, hx, by simp [Real.pi_ne_zero]⟩, ?_⟩; simp [AE.pow, hx, Real.pi_ne_zero, mul_comm]"))
sp-acj4-364-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[364] + rules.json[232]: rootn abs _0 3 -> abs rootn _0 3
Lean proof: included
(case sp-acj4-364-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[364] + rules.json[232]: rootn abs _0 3 -> abs rootn _0 3") (var x real) (ask (= (surd (abs x) 3) (abs (surd x 3)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [show (3:ℂ) = ((3:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨AE.abs_isReal _, AE.IsInt.ofInt 3, by norm_num, Or.inr (AE.odd_ofInt ⟨1, by norm_num⟩), Or.inr (by norm_num)⟩⟩, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt 3, by norm_num, Or.inr (AE.odd_ofInt ⟨1, by norm_num⟩), Or.inr (by norm_num)⟩, by simp⟩, ?_⟩; rw [AE.abs_ofReal, AE.surd_abs_odd r (by norm_num)]"))
sp-acj4-367-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[367] + rules.json[235]: rootn abs _0 9 -> abs rootn _0 9
Lean proof: included
(case sp-acj4-367-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[367] + rules.json[235]: rootn abs _0 9 -> abs rootn _0 9") (var x real) (ask (= (surd (abs x) 9) (abs (surd x 9)))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; rw [show (9:ℂ) = ((9:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨AE.abs_isReal _, AE.IsInt.ofInt 9, by norm_num, Or.inr (AE.odd_ofInt ⟨4, by norm_num⟩), Or.inr (by norm_num)⟩⟩, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt 9, by norm_num, Or.inr (AE.odd_ofInt ⟨4, by norm_num⟩), Or.inr (by norm_num)⟩, by simp⟩, ?_⟩; rw [AE.abs_ofReal, AE.surd_abs_odd r (by norm_num)]"))
sp-acj4-368-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[368] + rules.json[236]: rootn acos _0 (-5) -> pow acos _0 -0.2
Lean proof: included
(case sp-acj4-368-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[368] + rules.json[236]: rootn acos _0 (-5) -> pow acos _0 -0.2") (var x real) (assume (real (acos x))) (assume (nonzero (acos x))) (ask (= (surd (acos x) -5) (pow (acos x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.mem_Icc_of_acos_real (by simpa using h0.2); rw [AE.acos_ofReal hI.1 hI.2]; have ha : 0 ≤ Real.arccos r := Real.arccos_nonneg r; have hne : Real.arccos r ≠ 0 := (by have := h1.2; rw [AE.acos_ofReal hI.1 hI.2] at this; intro h; exact this (by rw [h]; simp)); rw [show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inl (by exact_mod_cast hne)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hne)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inl hne)]"))
sp-acj4-369-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[369] + rules.json[237]: rootn acos _0 5 -> pow acos _0 0.2
Lean proof: included
(case sp-acj4-369-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[369] + rules.json[237]: rootn acos _0 5 -> pow acos _0 0.2") (var x real) (assume (real (acos x))) (ask (= (surd (acos x) 5) (pow (acos x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.mem_Icc_of_acos_real (by simpa using h0.2); rw [AE.acos_ofReal hI.1 hI.2]; have ha : 0 ≤ Real.arccos r := Real.arccos_nonneg r; rw [show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inr (by norm_num)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inr (by norm_num)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inr (by norm_num))]"))
sp-acj4-370-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[370] + rules.json[238]: rootn acosh _0 (-5) -> pow acosh _0 -0.2
Lean proof: included
(case sp-acj4-370-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[370] + rules.json[238]: rootn acosh _0 (-5) -> pow acosh _0 -0.2") (var x real) (assume (real (acosh x))) (assume (nonzero (acosh x))) (ask (= (surd (acosh x) -5) (pow (acosh x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.one_le_of_acosh_real (by simpa using h0.2); rw [AE.acosh_ofReal hI]; have ha : 0 ≤ Real.arcosh r := AE.arcosh_nonneg hI; have hne : Real.arcosh r ≠ 0 := (by have := h1.2; rw [AE.acosh_ofReal hI] at this; intro h; exact this (by rw [h]; simp)); rw [show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inl (by exact_mod_cast hne)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hne)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inl hne)]"))
sp-acj4-371-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[371] + rules.json[239]: rootn acosh _0 5 -> pow acosh _0 0.2
Lean proof: included
(case sp-acj4-371-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[371] + rules.json[239]: rootn acosh _0 5 -> pow acosh _0 0.2") (var x real) (assume (real (acosh x))) (ask (= (surd (acosh x) 5) (pow (acosh x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hI := AE.one_le_of_acosh_real (by simpa using h0.2); rw [AE.acosh_ofReal hI]; have ha : 0 ≤ Real.arcosh r := AE.arcosh_nonneg hI; rw [show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨by simp, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simpa using ha), Or.inr (by norm_num)⟩⟩, by simp, by rw [AE.pow.D_iff]; exact Or.inr (by norm_num)⟩, ?_⟩; rw [AE.surd_ofReal_nonneg ha (by norm_num), AE.pow_ofReal ha (Or.inr (by norm_num))]"))
sp-acj4-372-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[372] + rules.json[240]: rootn cosh _0 (-5) -> pow cosh _0 -0.2
Lean proof: included
(case sp-acj4-372-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[372] + rules.json[240]: rootn cosh _0 (-5) -> pow cosh _0 -0.2") (var x real) (assume (nonzero (cosh x))) (ask (= (surd (cosh x) -5) (pow (cosh x) -1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hc := Real.cosh_pos r; rw [AE.cosh_ofReal, show (-5:ℂ) = ((-5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨trivial, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simp; positivity), Or.inl (by exact_mod_cast hc.ne')⟩⟩, trivial, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hc.ne')⟩, ?_⟩; rw [AE.surd_ofReal_nonneg hc.le (by norm_num), show ((-1:ℂ)/5) = (((((-5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, AE.pow_ofReal hc.le (Or.inl hc.ne')]"))
sp-acj4-373-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[373] + rules.json[241]: rootn cosh _0 5 -> pow cosh _0 0.2
Lean proof: included
(case sp-acj4-373-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[373] + rules.json[241]: rootn cosh _0 5 -> pow cosh _0 0.2") (var x real) (ask (= (surd (cosh x) 5) (pow (cosh x) 1/5))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; have hc := Real.cosh_pos r; rw [AE.cosh_ofReal, show ((1:ℂ)/5) = (((((5:ℤ):ℝ))⁻¹ : ℝ) : ℂ) by push_cast; ring, show (5:ℂ) = ((5:ℤ):ℂ) by norm_num]; refine ⟨⟨⟨trivial, by rw [AE.surd.D_iff]; exact ⟨by simp, AE.IsInt.ofInt _, by norm_num, Or.inl (by simp; positivity), Or.inl (by exact_mod_cast hc.ne')⟩⟩, trivial, by rw [AE.pow.D_iff]; exact Or.inl (by exact_mod_cast hc.ne')⟩, ?_⟩; rw [AE.surd_ofReal_nonneg hc.le (by norm_num), AE.pow_ofReal hc.le (Or.inl hc.ne')]"))
sp-acj4-38-real
equal at some admissible points, different at others
witness (true): \(x = 1\)
witness (false): \(x = -1\)
SimpliPy acj-4 (MIT) rules_real.json[38] + rules.json[31]: * 9 log _0 -> log pow _0 9
Lean proof: included
(case sp-acj4-38-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[38] + rules.json[31]: * 9 log _0 -> log pow _0 9") (var x real) (assume (nonzero x)) (assume (nonzero (pow x 9))) (ask (= (* 9 (log x)) (log (pow 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_r38w2 | 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-394-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[394] + rules.json[242]: sin abs atanh _0 -> abs sin atanh _0
Lean proof: included
(case sp-acj4-394-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[394] + rules.json[242]: sin abs atanh _0 -> abs sin atanh _0") (var x real) (assume (!= x 1)) (assume (!= x -1)) (ask (= (sin (abs (atanh x))) (abs (sin (atanh 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_r394w2 | 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-395-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[395] + rules.json[243]: sin abs cos _0 -> abs sin cos _0
Lean proof: included
(case sp-acj4-395-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[395] + rules.json[243]: sin abs cos _0 -> abs sin cos _0") (var x real) (ask (= (sin (abs (cos x))) (abs (sin (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.cos_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [Real.neg_one_le_cos r, Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-396-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[396] + rules.json[244]: sin abs sin _0 -> abs sin sin _0
Lean proof: included
(case sp-acj4-396-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[396] + rules.json[244]: sin abs sin _0 -> abs sin sin _0") (var x real) (ask (= (sin (abs (sin x))) (abs (sin (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.sin_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [Real.neg_one_le_sin r, Real.sin_le_one r, Real.pi_gt_three])]"))
sp-acj4-397-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[397] + rules.json[245]: sin abs tanh _0 -> abs sin tanh _0
Lean proof: included
(case sp-acj4-397-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[397] + rules.json[245]: sin abs tanh _0 -> abs sin tanh _0") (var x real) (ask (= (sin (abs (tanh x))) (abs (sin (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.tanh_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [(Real.neg_one_lt_tanh r).le, (Real.tanh_lt_one r).le, Real.pi_gt_three])]"))
sp-acj4-402-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[402] + rules.json[246]: sin atanh abs _0 -> abs sin atanh _0
Lean proof: included
(case sp-acj4-402-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[402] + rules.json[246]: sin atanh abs _0 -> abs sin atanh _0") (var x real) (assume (!= (abs x) 1)) (assume (!= x 1)) (assume (!= x -1)) (ask (= (sin (atanh (abs x))) (abs (sin (atanh 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_r402w2 | 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-404-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[404] + rules.json[247]: sin tanh abs _0 -> abs sin tanh _0
Lean proof: included
(case sp-acj4-404-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[404] + rules.json[247]: sin tanh abs _0 -> abs sin tanh _0") (var x real) (ask (= (sin (tanh (abs x))) (abs (sin (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], ?_⟩; simp only [AE.tanh_ofReal, AE.sin_ofReal, AE.abs_ofReal]; rw [AE.tanh_abs, AE.sin_abs_of_le_pi (by rw [abs_le]; constructor <;> linarith [(Real.neg_one_lt_tanh r).le, (Real.tanh_lt_one r).le, Real.pi_gt_three])]"))
sp-acj4-412-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[412] + rules.json[253]: tan abs asin _0 -> abs tan asin _0
Lean proof: included
(case sp-acj4-412-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[412] + rules.json[253]: tan abs asin _0 -> abs tan asin _0") (var x real) (assume (nonzero (cos (abs (asin x))))) (assume (nonzero (cos (asin x)))) (ask (= (tan (abs (asin x))) (abs (tan (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_r412w2 | exact AE.w2_r412_cos | exact AE.w2_r412_tanD | 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_asin_two]")))
sp-acj4-413-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[413] + rules.json[254]: tan abs cos _0 -> abs tan cos _0
Lean proof: included
(case sp-acj4-413-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[413] + rules.json[254]: tan abs cos _0 -> abs tan cos _0") (var x real) (assume (nonzero (cos (abs (cos x))))) (assume (nonzero (cos (cos x)))) (ask (= (tan (abs (cos x))) (abs (tan (cos x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.cos_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_le_cos r, Real.cos_le_one r, Real.pi_gt_three])]"))
sp-acj4-414-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[414] + rules.json[255]: tan abs sin _0 -> abs tan sin _0
Lean proof: included
(case sp-acj4-414-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[414] + rules.json[255]: tan abs sin _0 -> abs tan sin _0") (var x real) (assume (nonzero (cos (abs (sin x))))) (assume (nonzero (cos (sin x)))) (ask (= (tan (abs (sin x))) (abs (tan (sin x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.sin_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_le_sin r, Real.sin_le_one r, Real.pi_gt_three])]"))
sp-acj4-415-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[415] + rules.json[256]: tan abs tanh _0 -> abs tan tanh _0
Lean proof: included
(case sp-acj4-415-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[415] + rules.json[256]: tan abs tanh _0 -> abs tan tanh _0") (var x real) (assume (nonzero (cos (abs (tanh x))))) (assume (nonzero (cos (tanh x)))) (ask (= (tan (abs (tanh x))) (abs (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.tanh_ofReal, AE.abs_ofReal, AE.tan_ofReal]; rw [AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_lt_tanh r, Real.tanh_lt_one r, Real.pi_gt_three])]"))
sp-acj4-417-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[417] + rules.json[257]: tan asin abs _0 -> abs tan asin _0
Lean proof: included
(case sp-acj4-417-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[417] + rules.json[257]: tan asin abs _0 -> abs tan asin _0") (var x real) (assume (nonzero (cos (asin (abs x))))) (assume (nonzero (cos (asin x)))) (ask (= (tan (asin (abs x))) (abs (tan (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_r417w2 | 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_asin_two]")))
sp-acj4-421-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[421] + rules.json[260]: tan tanh abs _0 -> abs tan tanh _0
Lean proof: included
(case sp-acj4-421-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[421] + rules.json[260]: tan tanh abs _0 -> abs tan tanh _0") (var x real) (assume (nonzero (cos (tanh (abs x))))) (assume (nonzero (cos (tanh x)))) (ask (= (tan (tanh (abs x))) (abs (tan (tanh x))))) (expect true) (lean-proof "obtain ⟨r, rfl⟩ := AE.IsReal.exists hd0; refine ⟨⟨⟨by simp [AE.abs_ofReal, AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h0.2⟩, ⟨⟨by simp [AE.cosh_ofReal_ne_zero], by rw [AE.tan.D_iff, ← AE.cos_eq]; exact h1.2⟩, by simp⟩⟩, ?_⟩; simp only [AE.abs_ofReal, AE.tanh_ofReal, AE.tan_ofReal]; rw [AE.tanh_abs, AE.tan_abs_of_lt (by rw [abs_lt]; constructor <;> linarith [Real.neg_one_lt_tanh r, Real.tanh_lt_one r, Real.pi_gt_three])]"))
sp-acj4-5-real
equal at some admissible points, different at others
witness (true): \(x = 0\)
witness (false): \(x = 2\)
SimpliPy acj-4 (MIT) rules_real.json[5] + rules.json[3]: atanh abs _0 -> abs atanh _0
Lean proof: included
(case sp-acj4-5-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[5] + rules.json[3]: atanh abs _0 -> abs atanh _0") (var x real) (assume (!= (abs x) 1)) (assume (!= x 1)) (assume (!= x -1)) (ask (= (atanh (abs x)) (abs (atanh 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_r5w2 | 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-73-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[73] + rules.json[52]: / (-1) abs !0 -> inv neg abs !0
Lean proof: included
(case sp-acj4-73-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[73] + rules.json[52]: / (-1) abs !0 -> inv neg abs !0") (var x real) (assume (nonzero (abs x))) (assume (nonzero (- (abs x)))) (ask (= (/ -1 (abs x)) (/ (- (abs x))))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-80-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[80] + rules.json[59]: / (-1) cos _0 -> inv neg cos _0
Lean proof: included
(case sp-acj4-80-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[80] + rules.json[59]: / (-1) cos _0 -> inv neg cos _0") (var x real) (assume (nonzero (cos x))) (assume (nonzero (- (cos x)))) (ask (= (/ -1 (cos x)) (/ (- (cos x))))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, by simp, h1.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-83-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[83] + rules.json[62]: / (-1) log !0 -> inv neg log !0
Lean proof: included
(case sp-acj4-83-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[83] + rules.json[62]: / (-1) log !0 -> inv neg log !0") (var x real) (assume (nonzero x)) (assume (nonzero (log x))) (assume (nonzero (- (log x)))) (ask (= (/ -1 (log x)) (/ (- (log x))))) (expect true) (lean-proof "refine ⟨⟨⟨h0.2, h1.2⟩, h0.2, h2.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-86-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[86] + rules.json[65]: / (-1) tan !0 -> inv neg tan !0
Lean proof: included
(case sp-acj4-86-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[86] + rules.json[65]: / (-1) tan !0 -> inv neg tan !0") (var x real) (assume (nonzero (cos x))) (assume (nonzero (tan x))) (assume (nonzero (- (tan x)))) (ask (= (/ -1 (tan x)) (/ (- (tan x))))) (expect true) (lean-proof "refine ⟨⟨⟨h1.1.1, h1.2⟩, h1.1.1, h2.2⟩, ?_⟩; simp only [AE.inv_def]; rw [inv_neg]; ring"))
sp-acj4-90-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[90] + rules.json[69]: / 3 abs _0 -> abs / (-3) _0
Lean proof: included
(case sp-acj4-90-real (category simplipy-real) (note "SimpliPy acj-4 (MIT) rules_real.json[90] + rules.json[69]: / 3 abs _0 -> abs / (-3) _0") (var x real) (assume (nonzero (abs x))) (assume (nonzero x)) (ask (= (/ 3 (abs x)) (abs (/ -3 x)))) (expect true) (lean-proof "refine ⟨⟨⟨by simp, h0.2⟩, h1.2, by simp⟩, ?_⟩; simp [AE.abs_eq, div_eq_mul_inv]"))
sp-acj4-99-real
the two sides are equal at every admissible point
SimpliPy acj-4 (MIT) rules_real.json[99] + rules.json[78]: / abs _0 3 -> abs / _0 (-3)
Lean proof: included