awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
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)
rw₂ rw₃ : x / √(1 + HPow.hPow (β := ℕ) x 2) = x / √(1 + HPow.hPow (β := ℕ) x 2)
⊢ tanh (arsinh x) = x / √(1 + HPow.hPow (β := ℕ) x 2)

Tactic:
rw [tanh_eq_sinh_div_cosh, sinh_arsinh, cosh_arsinh]

Premises used: Real.tanh_eq_sinh_div_cosh, Real.sinh_arsinh, Real.cosh_arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ Surjective sinh

Tactic:
LeftInverse.surjective sinh_arsinh

Premises used: Real.sinh_arsinh, Function.LeftInverse.surjective
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ Bijective sinh

Tactic:
⟨sinh_injective, sinh_surjective⟩

Premises used: Real.sinh_surjective, And.intro, Function.Bijective, Real.sinh_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ arsinh (sinh x) = x

Tactic:
rightInverse_of_injective_of_leftInverse sinh_injective sinh_arsinh x

Premises used: Function.rightInverse_of_injective_of_leftInverse, Real.sinh_arsinh, Real.sinh_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ Bijective arsinh

Tactic:
sinhEquiv.symm.bijective

Premises used: Equiv.bijective, Real.arsinh, Real.log, dite, Real.sinhEquiv, Equiv.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ Injective arsinh

Tactic:
sinhEquiv.symm.injective

Premises used: Real.arsinh, Real.log, dite, Real.sinhEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ Surjective arsinh

Tactic:
sinhEquiv.symm.surjective

Premises used: Real.arsinh, Real.log, dite, Real.sinhEquiv, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ StrictMono arsinh

Tactic:
sinhOrderIso.symm.strictMono

Premises used: OrderIso.strictMono, Real.sinhOrderIso, Real.arsinh, OrderIso.symm, Real.log, dite
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x y : ℝ
⊢ arsinh x = arsinh y ↔ x = y

Tactic:
arsinh_injective.eq_iff

Premises used: Real.arsinh_injective, Function.Injective.eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x y : ℝ
⊢ arsinh x ≤ arsinh y ↔ x ≤ y

Tactic:
sinhOrderIso.symm.le_iff_le

Premises used: Real.sinhOrderIso, OrderIso.le_iff_le, Real.arsinh, OrderIso.symm, Real.log, dite
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x y : ℝ
⊢ arsinh x < arsinh y ↔ x < y

Tactic:
sinhOrderIso.symm.lt_iff_lt

Premises used: OrderIso.lt_iff_lt, Real.sinhOrderIso, Real.arsinh, OrderIso.symm, Real.log, dite
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ arsinh x = 0 ↔ x = 0

Tactic:
arsinh_injective.eq_iff' arsinh_zero

Premises used: Real.arsinh_zero, Real.arsinh_injective, Function.Injective.eq_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
rw : sinh 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
rw₁ : 0 ≤ sinh (arsinh x) ↔ 0 ≤ x
rw₂ rw₃ : 0 ≤ x ↔ 0 ≤ x
⊢ 0 ≤ arsinh x ↔ 0 ≤ x

Tactic:
rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]

Premises used: Real.sinh_zero, Real.sinh_arsinh, Real.sinh_le_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
rw : sinh (arsinh x) ≤ sinh 0 ↔ x ≤ 0
rw₁ : sinh (arsinh x) ≤ 0 ↔ x ≤ 0
rw₂ rw₃ : x ≤ 0 ↔ x ≤ 0
⊢ arsinh x ≤ 0 ↔ x ≤ 0

Tactic:
rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]

Premises used: Real.sinh_zero, Real.sinh_arsinh, Real.sinh_le_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ 0 < arsinh x ↔ 0 < x

Tactic:
lt_iff_lt_of_le_iff_le arsinh_nonpos_iff

Premises used: Real.arsinh_nonpos_iff, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ arsinh x < 0 ↔ x < 0

Tactic:
lt_iff_lt_of_le_iff_le arsinh_nonneg_iff

Premises used: Real.arsinh_nonneg_iff, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ HasStrictDerivAt (↑sinhHomeomorph.toOpenPartialHomeomorph.symm : ℝ → ℝ)
    (cosh ((↑sinhHomeomorph.toOpenPartialHomeomorph.symm : ℝ → ℝ) x))⁻¹ x

Tactic:
sinhHomeomorph.toOpenPartialHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne'
      (hasStrictDerivAt_sinh _)

Premises used: Real.hasStrictDerivAt_sinh, Real.sinhHomeomorph, Real.cosh_pos, LT.lt.ne', Set.mem_univ, OpenPartialHomeomorph.hasStrictDerivAt_symm, Homeomorph.toOpenPartialHomeomorph
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
h : √(1 + HPow.hPow (β := ℕ) x 2) = cosh ((↑sinhHomeomorph.toOpenPartialHomeomorph.symm : ℝ → ℝ) x)
⊢ HasStrictDerivAt arsinh (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ x

Tactic:
convert!
    sinhHomeomorph.toOpenPartialHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne'
      (hasStrictDerivAt_sinh _) using 2

Premises used: Real.hasStrictDerivAt_sinh, Real.sinhHomeomorph, Real.cosh_pos, LT.lt.ne', Set.mem_univ, OpenPartialHomeomorph.hasStrictDerivAt_symm, Homeomorph.toOpenPartialHomeomorph
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ √(1 + HPow.hPow (β := ℕ) x 2) = cosh ((↑sinhHomeomorph.toOpenPartialHomeomorph.symm : ℝ → ℝ) x)

Tactic:
(cosh_arsinh _).symm

Premises used: OpenPartialHomeomorph.toFun', Real.arsinh, Real.log, dite, Real.cosh_arsinh, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ √(1 + HPow.hPow (β := ℕ) x 2) = cosh ((↑sinhHomeomorph.toOpenPartialHomeomorph.symm : ℝ → ℝ) x)

Tactic:
exact (cosh_arsinh _).symm

Premises used: Real.cosh_arsinh, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ HasDerivAt arsinh (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ x

Tactic:
(hasStrictDerivAt_arsinh x).hasDerivAt

Premises used: Real.hasStrictDerivAt_arsinh, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ Differentiable ℝ arsinh

Tactic:
fun x =>
  (hasDerivAt_arsinh x).differentiableAt

Premises used: Differentiable, Real.hasDerivAt_arsinh, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℝ n arsinh

Tactic:
sinhHomeomorph.contDiff_symm_deriv (fun x => (cosh_pos x).ne') hasDerivAt_sinh contDiff_sinh

Premises used: Real.sinhHomeomorph, Real.arsinh, Real.log, dite, Real.cosh_pos, LT.lt.ne', Real.contDiff_sinh, Homeomorph.contDiff_symm_deriv, Real.hasDerivAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ Continuous arsinh

Tactic:
sinhHomeomorph.symm.continuous

Premises used: Homeomorph.continuous, Real.sinhHomeomorph, Real.arsinh, Real.log, dite, Homeomorph.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ AnalyticAt ℝ arsinh x

Tactic:
contDiff_arsinh.contDiffAt.analyticAt

Premises used: Real.contDiff_arsinh, ContDiffAt.analyticAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
s : Set ℝ
⊢ AnalyticWithinAt ℝ arsinh s x

Tactic:
contDiff_arsinh.contDiffWithinAt.analyticWithinAt

Premises used: Real.contDiff_arsinh, ContDiff.contDiffWithinAt, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
s : Set ℝ
⊢ AnalyticOnNhd ℝ arsinh s

Tactic:
fun _ _ ↦ analyticAt_arsinh

Premises used: AnalyticOnNhd, Real.analyticAt_arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
s : Set ℝ
⊢ AnalyticOn ℝ arsinh s

Tactic:
contDiff_arsinh.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, Real.contDiff_arsinh, ContDiffOn.analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
a : ℝ
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ Real.arsinh (f x)) l (𝓝 (Real.arsinh a))

Tactic:
(continuous_arsinh.tendsto _).comp h

Premises used: Real.arsinh, Real.log, dite, Continuous.tendsto, Filter.Tendsto.comp, Real.continuous_arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
a : X
h : ContinuousAt f a
⊢ ContinuousAt (Y := ℝ) (fun (x : X) ↦ Real.arsinh (f x)) a

Tactic:
h.arsinh

Premises used: ContinuousAt, Filter.Tendsto.arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
s : Set X
a : X
h : ContinuousWithinAt f s a
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : X) ↦ Real.arsinh (f x)) s a

Tactic:
h.arsinh

Premises used: ContinuousWithinAt, Filter.Tendsto.arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
s : Set X
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ) (fun (x : X) ↦ Real.arsinh (f x)) s

Tactic:
fun x hx => (h x hx).arsinh

Premises used: ContinuousWithinAt.arsinh, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
h : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (x : X) ↦ Real.arsinh (f x)

Tactic:
continuous_arsinh.comp h

Premises used: Continuous.comp, Real.arsinh, Real.log, dite, Real.continuous_arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
f' : StrongDual ℝ E
hf : HasStrictFDerivAt f f' a
⊢ HasStrictFDerivAt (fun (x : E) ↦ Real.arsinh (f x)) ((√(1 + HPow.hPow (β := ℕ) (f a) 2))⁻¹ • f') a

Tactic:
(hasStrictDerivAt_arsinh _).comp_hasStrictFDerivAt a hf

Premises used: Real.arsinh, Real.log, dite, Real.hasStrictDerivAt_arsinh, HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
f' : StrongDual ℝ E
hf : HasFDerivAt f f' a
⊢ HasFDerivAt (fun (x : E) ↦ Real.arsinh (f x)) ((√(1 + HPow.hPow (β := ℕ) (f a) 2))⁻¹ • f') a

Tactic:
(hasDerivAt_arsinh _).comp_hasFDerivAt a hf

Premises used: Real.hasDerivAt_arsinh, Real.arsinh, Real.log, dite, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a : E
f' : StrongDual ℝ E
hf : HasFDerivWithinAt f f' s a
⊢ HasFDerivWithinAt (fun (x : E) ↦ Real.arsinh (f x)) ((√(1 + HPow.hPow (β := ℕ) (f a) 2))⁻¹ • f') s a

Tactic:
(hasDerivAt_arsinh _).comp_hasFDerivWithinAt a hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Real.hasDerivAt_arsinh, Real.arsinh, Real.log, dite
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
h : DifferentiableAt ℝ f a
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ Real.arsinh (f x)) a

Tactic:
(differentiable_arsinh _).comp a h

Premises used: Real.arsinh, Real.log, dite, DifferentiableAt.comp, Real.differentiable_arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a : E
h : DifferentiableWithinAt ℝ f s a
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ Real.arsinh (f x)) s a

Tactic:
(differentiable_arsinh _).comp_differentiableWithinAt a h

Premises used: Real.arsinh, Real.log, dite, DifferentiableAt.comp_differentiableWithinAt, Real.differentiable_arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
h : DifferentiableOn ℝ f s
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : E) ↦ Real.arsinh (f x)) s

Tactic:
fun x hx => (h x hx).arsinh

Premises used: DifferentiableWithinAt.arsinh, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
h : Differentiable ℝ f
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ Real.arsinh (f x)

Tactic:
differentiable_arsinh.comp h

Premises used: Real.arsinh, Real.log, dite, Real.differentiable_arsinh, Differentiable.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
n : ℕ∞
h : ContDiffAt ℝ (↑n : WithTop ℕ∞) f a
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : E) ↦ Real.arsinh (f x)) a

Tactic:
contDiff_arsinh.contDiffAt.comp a h

Premises used: Real.contDiff_arsinh, Real.arsinh, Real.log, dite, ContDiffAt.comp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a : E
n : ℕ∞
h : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) f s a
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : E) ↦ Real.arsinh (f x)) s a

Tactic:
contDiff_arsinh.contDiffAt.comp_contDiffWithinAt a h

Premises used: Real.contDiff_arsinh, Real.arsinh, Real.log, dite, ContDiffAt.comp_contDiffWithinAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
n : ℕ∞
h : ContDiff ℝ (↑n : ℕ∞ω) f
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : E) ↦ Real.arsinh (f x)

Tactic:
contDiff_arsinh.comp h

Premises used: Real.contDiff_arsinh, Real.arsinh, Real.log, dite, ContDiff.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
n : ℕ∞
h : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
⊢ ContDiffOn ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : E) ↦ Real.arsinh (f x)) s

Tactic:
fun x hx => (h x hx).arsinh

Premises used: ContDiffOn, ContDiffWithinAt.arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
f : ℝ → ℝ
a f' : ℝ
hf : HasStrictDerivAt f f' a
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ Real.arsinh (f x)) ((√(1 + HPow.hPow (β := ℕ) (f a) 2))⁻¹ • f') a

Tactic:
(hasStrictDerivAt_arsinh _).comp a hf

Premises used: Real.arsinh, Real.log, dite, Real.hasStrictDerivAt_arsinh, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
f : ℝ → ℝ
a f' : ℝ
hf : HasDerivAt f f' a
⊢ HasDerivAt (fun (x : ℝ) ↦ Real.arsinh (f x)) ((√(1 + HPow.hPow (β := ℕ) (f a) 2))⁻¹ • f') a

Tactic:
(hasDerivAt_arsinh _).comp a hf

Premises used: Real.hasDerivAt_arsinh, HasDerivAt.comp, Real.arsinh, Real.log, dite
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
f : ℝ → ℝ
s : Set ℝ
a f' : ℝ
hf : HasDerivWithinAt f f' s a
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ Real.arsinh (f x)) ((√(1 + HPow.hPow (β := ℕ) (f a) 2))⁻¹ • f') s a

Tactic:
(hasDerivAt_arsinh _).comp_hasDerivWithinAt a hf

Premises used: Real.hasDerivAt_arsinh, Real.arsinh, Real.log, dite, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
⊢ 0 ≤ 1 + x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
⊢ 0 ≤ 1 - x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
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))
rw₂ rw₃ : log ((1 + x) / (1 - x)) / 2 = log ((1 + x) / (1 - x)) / 2
⊢ artanh x = 1 / 2 * log ((1 + x) / (1 - x))

Tactic:
rw [artanh, log_sqrt <| div_nonneg (by grind) (by grind), one_div_mul_eq_div]

Premises used: Real.log_sqrt, Real.artanh, one_div_mul_eq_div, div_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ 0 < 1 + x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ 0 < 1 - x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
⊢ artanh 0 = 0

Tactic:
simp [artanh]

Premises used: Real.artanh
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ 0 < √((1 + x) / (1 - x))

Tactic:
have : 0 < √((1 + x) / (1 - x)) := sqrt_pos_of_pos <| div_pos (by grind) (by grind)
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
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))
hx₁ : 0 ≤ 1 + x
⊢ sinh (artanh x) = x / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]

Premises used: one_pow, Real.sqrt_mul, OfNat.ofNat, sq_sub_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : 0 < √((1 + x) / (1 - x))
⊢ sinh (artanh x) = x / (√(1 + x) * √(1 - x))

Tactic:
grind [artanh, sinh_eq, exp_neg, exp_log, sqrt_div]

Premises used: Real.sinh_eq, Real.exp_log, Real.artanh, Real.sqrt_div, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : 0 < √((1 + x) / (1 - x))
⊢ 0 ≤ 1 + x

Tactic:
grind [artanh, sinh_eq, exp_neg, exp_log, sqrt_div]

Premises used: Real.sinh_eq, Real.exp_log, Real.artanh, Real.sqrt_div, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
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))
hx₁ : 0 ≤ 1 + x
⊢ cosh (artanh x) = 1 / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]

Premises used: one_pow, Real.sqrt_mul, OfNat.ofNat, sq_sub_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : 0 < √((1 + x) / (1 - x))
⊢ cosh (artanh x) = HPow.hPow (α := ℝ) (β := ℕ) 1 2 / (√(1 + x) * √(1 - x))

Tactic:
grind [artanh, cosh_eq, exp_neg, exp_log, sqrt_div]

Premises used: Real.exp_log, Real.artanh, Real.sqrt_div, Real.cosh_eq, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : 0 < √((1 + x) / (1 - x))
⊢ 0 ≤ 1 + x

Tactic:
grind [artanh, cosh_eq, exp_neg, exp_log, sqrt_div]

Premises used: Real.exp_log, Real.artanh, Real.sqrt_div, Real.cosh_eq, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ HPow.hPow (α := ℝ) (β := ℕ) 1 2 - HPow.hPow (β := ℕ) x 2 = (1 + x) * (1 - x)

Tactic:
have := sq_sub_sq 1 x
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
this : HPow.hPow (α := ℝ) (β := ℕ) 1 2 - HPow.hPow (β := ℕ) x 2 = (1 + x) * (1 - x)
⊢ tanh (artanh x) = x

Tactic:
grind [tanh_eq_sinh_div_cosh, sinh_artanh, cosh_artanh, sqrt_ne_zero', mul_pos]

Premises used: Real.tanh_eq_sinh_div_cosh, mul_pos, Real.sinh_artanh, Real.sqrt_ne_zero', Real.cosh_artanh
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
⊢ 0 < 1 + tanh x

Tactic:
grind [neg_one_lt_tanh]

Premises used: Real.neg_one_lt_tanh
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
⊢ 0 < 1 - tanh x

Tactic:
grind [tanh_lt_one]

Premises used: Real.tanh_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
⊢ 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])
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
rw :
  (1 + (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) / (1 - (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) =
    HPow.hPow (β := ℕ) (rexp x) 2
⊢ artanh (tanh x) = x

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]

Premises used: Real.exp_eq_exp, le_of_lt, Real.sq_sqrt, Real.exp_log, Real.sqrt_pos_of_pos, Real.exp_nonneg, Real.artanh, Real.tanh_eq, sq_eq_sq₀, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
h : 0 < (1 + tanh x) / (1 - tanh x)
⊢ (1 + (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) / (1 - (rexp x - (rexp x)⁻¹) / (rexp x + (rexp x)⁻¹)) =
    HPow.hPow (β := ℕ) (rexp x) 2

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y
h : x < y
⊢ 0 < 1 - x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y
h : x < y
⊢ 0 < 1 - y

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y
h : x < y
field_simp : (1 + x) * (1 - y) < (1 - x) * (1 + y)
⊢ LT.lt (α := ℝ) ((fun (x : ℝ) ↦ (1 + x) / (1 - x)) x) ((fun (x : ℝ) ↦ (1 + x) / (1 - x)) y)

Tactic:
field_simp [show 0 < 1 - x by grind, show 0 < 1 - y by grind]
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y
h : x < y
⊢ (1 + x) * (1 - y) < (1 - x) * (1 + y)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
apply : StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ √((1 + x) / (1 - x))) (Ioo (-1) 1)
⊢ StrictMonoOn artanh (Ioo (-1) 1)

Tactic:
apply strictMonoOn_log.comp ?_ fun x hx ↦ sqrt_pos_of_pos <| div_pos (by grind) (by grind)

Premises used: StrictMonoOn.comp, Real.sqrt_pos_of_pos, Real.strictMonoOn_log, div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ 0 ≤ 1 + x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ 0 ≤ 1 - x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ 0 ≤ (1 + x) / (1 - x)

Tactic:
exact div_nonneg (by grind) (by grind)

Premises used: div_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ √((1 + x) / (1 - x))) (Ioo (-1) 1)

Tactic:
apply strictMonoOn_sqrt.comp strictMonoOn_one_add_div_one_sub
    fun x hx ↦ show 0 ≤ (1 + x) / (1 - x) by exact div_nonneg (by grind) (by grind)

Premises used: Real.strictMonoOn_sqrt, StrictMonoOn.comp, Real.strictMonoOn_one_add_div_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x y : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
hy : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y
⊢ artanh x ≤ artanh y ↔ x ≤ y

Tactic:
strictMonoOn_artanh.le_iff_le hx hy

Premises used: Real.strictMonoOn_artanh, StrictMonoOn.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x y : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
hy : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y
⊢ artanh x < artanh y ↔ x < y

Tactic:
strictMonoOn_artanh.lt_iff_lt hx hy

Premises used: Real.strictMonoOn_artanh, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x y : ℝ
hx : -1 < x
hy : y < 1
hxy : x ≤ y
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x y : ℝ
hx : -1 < x
hy : y < 1
hxy : x ≤ y
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x y : ℝ
hx : -1 < x
hy : y < 1
hxy : x < y
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x y : ℝ
hx : -1 < x
hy : y < 1
hxy : x < y
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) y

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
⊢ artanh x = 0 ↔ x ≤ -1 ∨ x = 0 ∨ 1 ≤ x

Tactic:
grind [artanh, log_eq_zero, div_nonpos_iff]

Premises used: Real.log_eq_zero, div_nonpos_iff, Real.artanh
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
rw : 0 < x
⊢ 0 < artanh x

Tactic:
rw [← artanh_zero, artanh_lt_artanh_iff (by grind) (by grind)]

Premises used: Real.artanh_zero, Real.artanh_lt_artanh_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Artanh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ 0 < x

Tactic:
hx.1

Premises used: And.left