awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
h :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₁ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h₂ : (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
h :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₁ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
h₂ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h₃ : (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * k * (x * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
h :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₁ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
h₂ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₃ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * k * (x * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h₄ : (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2 * (x * y))) (k * ((x + y) / 2)) n).2 =
  k * (x.agmSequences y (n + 1)).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
h :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₁ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
h₂ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₃ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * k * (x * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₄ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2 * (x * y))) (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h₅ : ((HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2) : ℝ≥0)
          ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences
      (k * ((x + y) / 2)) n).2 =
  k * (x.agmSequences y (n + 1)).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
h :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₁ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
h₂ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₃ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * k * (x * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₄ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2 * (x * y))) (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₅ :
  ((HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2) : ℝ≥0)
            ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences
        (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h₆ : ((HMul.hMul (β := ℝ≥0) k ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences (k * ((x + y) / 2)) n).2 =
  k * (x.agmSequences y (n + 1)).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
h :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₁ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
h₂ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₃ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * k * (x * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₄ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2 * (x * y))) (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₅ :
  ((HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2) : ℝ≥0)
            ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences
        (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₆ :
  ((HMul.hMul (β := ℝ≥0) k ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h₇ : k * (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
h :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₁ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
h₂ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₃ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * k * (x * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₄ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2 * (x * y))) (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₅ :
  ((HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2) : ℝ≥0)
            ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences
        (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₆ :
  ((HMul.hMul (β := ℝ≥0) k ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₇ : k * (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h₈ : k * (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) n).2 =
  k * (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) n).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y k : ℝ≥0
n : ℕ
⊢ ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
have h : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) 0).2 = k * (x.agmSequences y 0).2
Tactic: induction n generalizing x y with
  | zero => simp [← mul_div_assoc, mul_add]
  | succ n ih =>
    rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
Cleared hypotheses: x, y, n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y k : ℝ≥0
n : ℕ
h : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) 0).2 = k * (x.agmSequences y 0).2
⊢ ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
have h₁ : ∀ (n : ℕ) (ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2) {x y : ℝ≥0},
  ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
Tactic: induction n generalizing x y with
  | zero => simp [← mul_div_assoc, mul_add]
  | succ n ih =>
    rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
Cleared hypotheses: x, y, n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ rexp (arsinh x) = x + √(1 + HPow.hPow (β := ℕ) x 2)
have hx : 0 < x + √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: apply exp_log
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ 0 < x + √(1 + HPow.hPow (β := ℕ) x 2)
have hx : -x < √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [← neg_lt_iff_pos_add']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ -x < √(1 + HPow.hPow (β := ℕ) x 2)
have hx : HPow.hPow (β := ℕ) (-x) 2 < 1 + HPow.hPow (β := ℕ) x 2
Tactic: apply lt_sqrt_of_sq_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ arsinh (-x) = -arsinh x
have rw : -x + √(1 + HPow.hPow (β := ℕ) (-x) 2) = (x + √(1 + HPow.hPow (β := ℕ) x 2))⁻¹
Tactic: rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ -x + √(1 + HPow.hPow (β := ℕ) (-x) 2) = (x + √(1 + HPow.hPow (β := ℕ) x 2))⁻¹
have h : (-x + √(1 + HPow.hPow (β := ℕ) (-x) 2)) * (x + √(1 + HPow.hPow (β := ℕ) x 2)) = 1
Tactic: apply eq_inv_of_mul_eq_one_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ (-x + √(1 + HPow.hPow (β := ℕ) (-x) 2)) * (x + √(1 + HPow.hPow (β := ℕ) x 2)) = 1
have h : 0 ≤ 1 + HPow.hPow (β := ℕ) x 2
Tactic: rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ sinh (arsinh x) = x
have rw : (x + √(1 + HPow.hPow (β := ℕ) x 2) - (-x + √(1 + HPow.hPow (β := ℕ) x 2))) / 2 = x
Tactic: rw [sinh_eq, ← arsinh_neg, exp_arsinh, exp_arsinh, neg_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ cosh (arsinh x) = √(1 + HPow.hPow (β := ℕ) x 2)
have rw : √(HPow.hPow (β := ℕ) (cosh (arsinh x)) 2) = √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
rw : √(HPow.hPow (β := ℕ) (cosh (arsinh x)) 2) = √(1 + HPow.hPow (β := ℕ) x 2)
⊢ cosh (arsinh x) = √(1 + HPow.hPow (β := ℕ) x 2)
have rw₁ : √(1 + HPow.hPow (β := ℕ) (sinh (arsinh x)) 2) = √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
rw : √(HPow.hPow (β := ℕ) (cosh (arsinh x)) 2) = √(1 + HPow.hPow (β := ℕ) x 2)
rw₁ : √(1 + HPow.hPow (β := ℕ) (sinh (arsinh x)) 2) = √(1 + HPow.hPow (β := ℕ) x 2)
⊢ cosh (arsinh x) = √(1 + HPow.hPow (β := ℕ) x 2)
have rw₂ : √(1 + HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ tanh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
have rw : sinh (arsinh x) / cosh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_arsinh, cosh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
rw : sinh (arsinh x) / cosh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
⊢ tanh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
have rw₁ : x / cosh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_arsinh, cosh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
rw : sinh (arsinh x) / cosh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
rw₁ : x / cosh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
⊢ tanh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
have rw₂ : x / √(1 + HPow.hPow (β := ℕ) x 2) = x / √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_arsinh, cosh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ 0 ≤ arsinh x ↔ 0 ≤ x
have rw : sinh 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
Tactic: rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
rw : sinh 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
⊢ 0 ≤ arsinh x ↔ 0 ≤ x
have rw₁ : 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
Tactic: rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
rw : sinh 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
rw₁ : 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
⊢ 0 ≤ arsinh x ↔ 0 ≤ x
have rw₂ : 0 ≤ x ↔ 0 ≤ x
Tactic: rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ arsinh x ≤ 0 ↔ x ≤ 0
have rw : sinh (arsinh x) ≤ sinh 0 ↔ x ≤ 0
Tactic: rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
rw : sinh (arsinh x) ≤ sinh 0 ↔ x ≤ 0
⊢ arsinh x ≤ 0 ↔ x ≤ 0
have rw₁ : sinh (arsinh x) ≤ 0 ↔ x ≤ 0
Tactic: rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
rw : sinh (arsinh x) ≤ sinh 0 ↔ x ≤ 0
rw₁ : sinh (arsinh x) ≤ 0 ↔ x ≤ 0
⊢ arsinh x ≤ 0 ↔ x ≤ 0
have rw₂ : x ≤ 0 ↔ x ≤ 0
Tactic: rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arsinh (goal)
Goal:
x : ℝ
⊢ HasStrictDerivAt arsinh (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ x
have h : √(1 + HPow.hPow (β := ℕ) x 2) = cosh ((↑sinhHomeomorph.toOpenPartialHomeomorph.symm : ℝ → ℝ) x)
Tactic: convert!
    sinhHomeomorph.toOpenPartialHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne'
      (hasStrictDerivAt_sinh _) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
⊢ artanh x = 1 / 2 * log ((1 + x) / (1 - x))
have rw : log √((1 + x) / (1 - x)) = 1 / 2 * log ((1 + x) / (1 - x))
Tactic: rw [artanh, log_sqrt <| div_nonneg (by grind) (by grind), one_div_mul_eq_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
rw : log √((1 + x) / (1 - x)) = 1 / 2 * log ((1 + x) / (1 - x))
⊢ artanh x = 1 / 2 * log ((1 + x) / (1 - x))
have rw₁ : log ((1 + x) / (1 - x)) / 2 = 1 / 2 * log ((1 + x) / (1 - x))
Tactic: rw [artanh, log_sqrt <| div_nonneg (by grind) (by grind), one_div_mul_eq_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
rw : log √((1 + x) / (1 - x)) = 1 / 2 * log ((1 + x) / (1 - x))
rw₁ : log ((1 + x) / (1 - x)) / 2 = 1 / 2 * log ((1 + x) / (1 - x))
⊢ artanh x = 1 / 2 * log ((1 + x) / (1 - x))
have rw₂ : log ((1 + x) / (1 - x)) / 2 = log ((1 + x) / (1 - x)) / 2
Tactic: rw [artanh, log_sqrt <| div_nonneg (by grind) (by grind), one_div_mul_eq_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ sinh (artanh x) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have this : 0 < √((1 + x) / (1 - x))
Tactic: have : 0 < √((1 + x) / (1 - x)) := sqrt_pos_of_pos <| div_pos (by grind) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : 0 < √((1 + x) / (1 - x))
⊢ sinh (artanh x) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have rw : sinh (artanh x) = x / (√(1 + x) * √(1 - x))
Tactic: rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : 0 < √((1 + x) / (1 - x))
rw : sinh (artanh x) = x / (√(1 + x) * √(1 - x))
⊢ sinh (artanh x) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have hx₁ : 0 ≤ 1 + x
Tactic: rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ cosh (artanh x) = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have this : 0 < √((1 + x) / (1 - x))
Tactic: have : 0 < √((1 + x) / (1 - x)) := sqrt_pos_of_pos <| div_pos (by grind) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : 0 < √((1 + x) / (1 - x))
⊢ cosh (artanh x) = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have rw : cosh (artanh x) = HPow.hPow (α := ℝ) (β := ℕ) 1 2 / (√(1 + x) * √(1 - x))
Tactic: rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : 0 < √((1 + x) / (1 - x))
rw : cosh (artanh x) = HPow.hPow (α := ℝ) (β := ℕ) 1 2 / (√(1 + x) * √(1 - x))
⊢ cosh (artanh x) = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have hx₁ : 0 ≤ 1 + x
Tactic: rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ tanh (artanh x) = x
have this : HPow.hPow (α := ℝ) (β := ℕ) 1 2 - HPow.hPow (β := ℕ) x 2 = (1 + x) * (1 - x)
Tactic: have := sq_sub_sq 1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (hypothesis)
Goal:
x : ℝ
⊢ artanh (tanh x) = x
have h : 0 < (1 + tanh x) / (1 - tanh x)
Tactic: have h : 0 < (1 + tanh x) / (1 - tanh x) :=
    div_pos (by grind [neg_one_lt_tanh]) (by grind [tanh_lt_one])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ artanh (tanh x) = x
have rw : (1 + (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) / (1 - (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) =
  HPow.hPow (β := ℕ) (rexp x) 2
Tactic: rw [artanh, ← exp_eq_exp, exp_log (sqrt_pos_of_pos h),
    ← sq_eq_sq₀ (le_of_lt <| sqrt_pos_of_pos h) (exp_nonneg x),
    sq_sqrt (le_of_lt h), tanh_eq, exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y
h : x < y
⊢ LT.lt (α := ℝ) ((fun (x : ℝ) ↦ (1 + x) / (1 - x)) x) ((fun (x : ℝ) ↦ (1 + x) / (1 - x)) y)
have field_simp : (1 + x) * (1 - y) < (1 - x) * (1 + y)
Tactic: field_simp [show 0 < 1 - x by grind, show 0 < 1 - y by grind]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
⊢ StrictMonoOn artanh (Ioo (-1) 1)
have apply : StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ √((1 + x) / (1 - x))) (Ioo (-1) 1)
Tactic: apply strictMonoOn_log.comp ?_ fun x hx ↦ sqrt_pos_of_pos <| div_pos (by grind) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ 0 < artanh x
have rw : 0 < x
Tactic: rw [← artanh_zero, artanh_lt_artanh_iff (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 0) x
⊢ artanh x < 0
have rw : x < 0
Tactic: rw [← artanh_zero, artanh_lt_artanh_iff (by grind) (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ artanh x
have by_cases : x < 1 → 0 ≤ artanh x
Tactic: by_cases x < 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : 0 ≤ x
by_cases : x < 1 → 0 ≤ artanh x
⊢ 0 ≤ artanh x
have by_cases₁ : ¬x < 1 → 0 ≤ artanh x
Tactic: by_cases x < 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : x ≤ 0
⊢ artanh x ≤ 0
have by_cases : -1 < x → artanh x ≤ 0
Tactic: by_cases -1 < x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Artanh (goal)
Goal:
x : ℝ
hx : x ≤ 0
by_cases : -1 < x → artanh x ≤ 0
⊢ artanh x ≤ 0
have by_cases₁ : ¬-1 < x → artanh x ≤ 0
Tactic: by_cases -1 < x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
n ν : ℕ
x : (↑I : Type)
⊢ LE.le (α := ℝ) (0 : ℝ) ((bernstein n ν : (a : (↑I : Type)) → ℝ) x : ℝ)
have simp : 0 ≤ (↑(n.choose ν) : ℝ) * (↑x : ℝ) ^ ν * (1 - (↑x : ℝ)) ^ (n - ν)
Tactic: simp only [bernstein_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
Goal:
n ν : ℕ
x : (↑I : Type)
⊢ 0 ≤ (↑(n.choose ν) : ℝ) * (↑x : ℝ) ^ ν * (1 - (↑x : ℝ)) ^ (n - ν)
have h₁ : 0 ≤ (↑x : ℝ)
Tactic: have h₁ : (0 : ℝ) ≤ x := by unit_interval
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
Goal:
n ν : ℕ
x : (↑I : Type)
h₁ : 0 ≤ (↑x : ℝ)
⊢ 0 ≤ (↑(n.choose ν) : ℝ) * (↑x : ℝ) ^ ν * (1 - (↑x : ℝ)) ^ (n - ν)
have h₂ : 0 ≤ 1 - (↑x : ℝ)
Tactic: have h₂ : (0 : ℝ) ≤ 1 - x := by unit_interval
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
Goal:
n : ℕ
x : (↑I : Type)
⊢ Eq (α := ℝ) (∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x) 1
have this : Eq (α := Polynomial ℝ) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) 1
Tactic: have := bernsteinPolynomial.sum ℝ n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (hypothesis)
Goal:
n : ℕ
x : (↑I : Type)
this : Eq (α := Polynomial ℝ) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) 1
⊢ Eq (α := ℝ) (∑ k : Fin (n + 1), (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x) 1
have this₁ : Eq (α := ℝ)
  ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ) (∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial ℝ n ν) : ℝ)
  ((Polynomial.aeval (↑x : ℝ) : (a : Polynomial ℝ) → ℝ) 1 : ℝ)
Tactic: apply_fun fun p => Polynomial.aeval (x : ℝ) p at this
Cleared hypotheses: this