awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
rcases :
  ∀ (M : ℝ) (hM : Membership.mem (γ := Set ℝ) (upperBounds (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) (c • x))) M),
    BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)

Tactic:
rcases h _ hc with ⟨M, hM⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) (c • x))) M
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)

Tactic:
⟨M / ‖c‖, forall_mem_range.mpr fun i ↦ (le_div_iff₀' (norm_pos_iff.2 hc₀)).2 ?_⟩

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, le_div_iff₀', Set.forall_mem_range, HDiv.hDiv, BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) (c • x))) M
refine : ∀ (i : ι), HMul.hMul (β := ℝ) ‖c‖ ((p i : (a : E) → ℝ) x : ℝ) ≤ M
⊢ BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)

Tactic:
refine ⟨M / ‖c‖, forall_mem_range.mpr fun i ↦ (le_div_iff₀' (norm_pos_iff.2 hc₀)).2 ?_⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) (c • x))) M
i : ι
⊢ HMul.hMul (β := ℝ) ‖c‖ ((p i : (a : E) → ℝ) x : ℝ) ≤ M

Tactic:
hM ⟨i, map_smul_eq_mul ..⟩

Premises used: SeminormClass.map_smul_eq_mul, Exists.intro
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
s : Set E
hs : Absorbent 𝕜 s
h : ∀ x ∈ s, BddAbove (α := ℝ) (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) x)
x : E
c : 𝕜
hc₀ : c ≠ 0
hc : c • x ∈ s
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds (range fun (x_1 : ι) ↦ (p x_1 : (a : E) → ℝ) (c • x))) M
i : ι
⊢ HMul.hMul (β := ℝ) ‖c‖ ((p i : (a : E) → ℝ) x : ℝ) ≤ M

Tactic:
exact hM ⟨i, map_smul_eq_mul ..⟩

Premises used: SeminormClass.map_smul_eq_mul, Exists.intro
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
⊢ Eq (α := (a : E) → ℝ) (⇑(normSeminorm 𝕜 E) : (a : E) → ℝ) norm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
h : ∀ (x : E) (r : ℝ) (y : E), y ∈ Seminorm.ball (normSeminorm 𝕜 E) x r ↔ y ∈ Metric.ball x r
⊢ Seminorm.ball (normSeminorm 𝕜 E) = Metric.ball

Tactic:
ext x r y
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ Seminorm.ball (normSeminorm 𝕜 E) x r ↔ y ∈ Metric.ball x r

Tactic:
simp only [Seminorm.mem_ball, Metric.mem_ball, coe_normSeminorm, dist_eq_norm]

Premises used: dist_eq_norm, Metric.mem_ball, coe_normSeminorm, Seminorm.mem_ball
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
h : ∀ (x : E) (r : ℝ) (y : E), y ∈ Seminorm.closedBall (normSeminorm 𝕜 E) x r ↔ y ∈ Metric.closedBall x r
⊢ Seminorm.closedBall (normSeminorm 𝕜 E) = Metric.closedBall

Tactic:
ext x r y
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ Seminorm.closedBall (normSeminorm 𝕜 E) x r ↔ y ∈ Metric.closedBall x r

Tactic:
simp only [Seminorm.mem_closedBall, Metric.mem_closedBall, coe_normSeminorm, dist_eq_norm]

Premises used: dist_eq_norm, coe_normSeminorm, Metric.mem_closedBall, Seminorm.mem_closedBall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
rw : Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
⊢ Absorbent.{u_3, u_7} 𝕜 (α := E) (Metric.ball 0 r)

Tactic:
rw [← ball_normSeminorm 𝕜]

Premises used: ball_normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)

Tactic:
(normSeminorm _ _).absorbent_ball_zero hr

Premises used: normSeminorm, Seminorm.absorbent_ball_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)

Tactic:
exact (normSeminorm _ _).absorbent_ball_zero hr

Premises used: normSeminorm, Seminorm.absorbent_ball_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
rw : Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) x r)
⊢ Absorbent 𝕜 (Metric.ball x r)

Tactic:
rw [← ball_normSeminorm 𝕜]

Premises used: ball_normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) x r)

Tactic:
(normSeminorm _ _).absorbent_ball hx

Premises used: normSeminorm, Seminorm.absorbent_ball
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) x r)

Tactic:
exact (normSeminorm _ _).absorbent_ball hx

Premises used: normSeminorm, Seminorm.absorbent_ball
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
rw : Balanced 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)
⊢ Balanced.{u_3, u_7} 𝕜 (E := E) (Metric.ball 0 r)

Tactic:
rw [← ball_normSeminorm 𝕜]

Premises used: ball_normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)

Tactic:
(normSeminorm _ _).balanced_ball_zero r

Premises used: Seminorm.balanced_ball_zero, normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Seminorm.ball (normSeminorm 𝕜 E) 0 r)

Tactic:
exact (normSeminorm _ _).balanced_ball_zero r

Premises used: Seminorm.balanced_ball_zero, normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
rw : Balanced 𝕜 (Seminorm.closedBall (normSeminorm 𝕜 E) 0 r)
⊢ Balanced.{u_3, u_7} 𝕜 (E := E) (Metric.closedBall 0 r)

Tactic:
rw [← closedBall_normSeminorm 𝕜]

Premises used: closedBall_normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Seminorm.closedBall (normSeminorm 𝕜 E) 0 r)

Tactic:
(normSeminorm _ _).balanced_closedBall_zero r

Premises used: Seminorm.balanced_closedBall_zero, normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (Seminorm.closedBall (normSeminorm 𝕜 E) 0 r)

Tactic:
exact (normSeminorm _ _).balanced_closedBall_zero r

Premises used: Seminorm.balanced_closedBall_zero, normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ (n : ℤ), c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

Tactic:
(normSeminorm 𝕜 E).rescale_to_shell_zpow hc εpos hx

Premises used: Seminorm.rescale_to_shell_zpow, normSeminorm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ (d : 𝕜), d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

Tactic:
(normSeminorm 𝕜 E).rescale_to_shell hc εpos hx

Premises used: normSeminorm, Seminorm.rescale_to_shell
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
F : Type u_10
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : F
hx : x ≠ 0
⊢ ∃ (n : ℤ), c ^ n ≠ 0 ∧ ‖c ^ n • x‖ < ε ∧ ε / ‖c‖ ≤ ‖c ^ n • x‖ ∧ ‖c ^ n‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

Tactic:
rescale_to_shell_semi_normed_zpow hc εpos (norm_ne_zero_iff.mpr hx)

Premises used: Iff.mpr, rescale_to_shell_semi_normed_zpow, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
F : Type u_10
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : F
hx : x ≠ 0
⊢ ∃ (d : 𝕜), d ≠ 0 ∧ ‖d • x‖ < ε ∧ ε / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * ‖x‖

Tactic:
rescale_to_shell_semi_normed hc εpos (norm_ne_zero_iff.mpr hx)

Premises used: Iff.mpr, rescale_to_shell_semi_normed, norm_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
hx₁ : 0 < x + √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ rexp (arcosh x) = x + √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
apply exp_log

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 < x + √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ arcosh 1 = 0

Tactic:
simp [arcosh]

Premises used: Real.arcosh
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
a : (x + √(HPow.hPow (β := ℕ) x 2 - 1)) * (x - √(HPow.hPow (β := ℕ) x 2 - 1)) = 1
⊢ (x + √(HPow.hPow (β := ℕ) x 2 - 1))⁻¹ = x - √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
apply inv_eq_of_mul_eq_one_right

Premises used: inv_eq_of_mul_eq_one_right
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
a : HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) x 2 - 1)) 2 = 1
a₁ : HPow.hPow (β := ℕ) x 2 - (HPow.hPow (β := ℕ) x 2 - 1) = 1
a₂ a₃ : Eq (α := ℝ) 1 1
⊢ (x + √(HPow.hPow (β := ℕ) x 2 - 1)) * (x - √(HPow.hPow (β := ℕ) x 2 - 1)) = 1

Tactic:
rw [← pow_two_sub_pow_two, sq_sqrt (sub_nonneg_of_le (one_le_pow₀ hx)), sub_sub_cancel]

Premises used: sub_nonneg_of_le, one_le_pow₀, Real.sq_sqrt, pow_two_sub_pow_two, sub_sub_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
rw : (x + √(HPow.hPow (β := ℕ) x 2 - 1) + (x - √(HPow.hPow (β := ℕ) x 2 - 1))) / 2 = x
⊢ cosh (arcosh x) = x

Tactic:
rw [arcosh, cosh_eq, exp_neg, exp_log (by positivity), add_sqrt_self_sq_sub_one_inv hx]

Premises used: Real.add_sqrt_self_sq_sub_one_inv, Real.arcosh, Real.exp_log, Real.cosh_eq, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
⊢ (x + √(HPow.hPow (β := ℕ) x 2 - 1) + (x - √(HPow.hPow (β := ℕ) x 2 - 1))) / 2 = x

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
rw : x + √(HPow.hPow (β := ℕ) x 2 - 1) = 1 ↔ x = 1
⊢ arcosh x = 0 ↔ x = 1

Tactic:
rw [← exp_injective.eq_iff, exp_arcosh hx, exp_zero]

Premises used: Real.exp_arcosh, Function.Injective.eq_iff, Real.exp_injective, Real.exp_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
⊢ x + √(HPow.hPow (β := ℕ) x 2 - 1) = 1 ↔ x = 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
rw : (x + √(HPow.hPow (β := ℕ) x 2 - 1) - (x - √(HPow.hPow (β := ℕ) x 2 - 1))) / 2 = √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ sinh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
rw [arcosh, sinh_eq, exp_neg, exp_log (by positivity), add_sqrt_self_sq_sub_one_inv hx]

Premises used: Real.sinh_eq, Real.add_sqrt_self_sq_sub_one_inv, Real.arcosh, Real.exp_log, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
⊢ (x + √(HPow.hPow (β := ℕ) x 2 - 1) - (x - √(HPow.hPow (β := ℕ) x 2 - 1))) / 2 = √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
rw : sinh (arcosh x) / cosh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x
rw₁ : √(HPow.hPow (β := ℕ) x 2 - 1) / cosh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x
rw₂ rw₃ : √(HPow.hPow (β := ℕ) x 2 - 1) / x = √(HPow.hPow (β := ℕ) x 2 - 1) / x
⊢ tanh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x

Tactic:
rw [tanh_eq_sinh_div_cosh, sinh_arcosh hx, cosh_arcosh hx]

Premises used: Real.sinh_arcosh, Real.tanh_eq_sinh_div_cosh, Real.cosh_arcosh
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 0 < cosh x + √(HPow.hPow (β := ℕ) (cosh x) 2 - 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 0 ≤ x
rw : log (cosh x + √(HPow.hPow (β := ℕ) (cosh x) 2 - 1)) = x
rw₁ : rexp (log (cosh x + √(HPow.hPow (β := ℕ) (cosh x) 2 - 1))) = rexp x
rw₂ : cosh x + √(HPow.hPow (β := ℕ) (cosh x) 2 - 1) = rexp x
rw₃ : √(HPow.hPow (β := ℕ) (cosh x) 2 - 1) = rexp x - cosh x
rw₄ : √(HPow.hPow (β := ℕ) (cosh x) 2 - 1) = sinh x
rw₅ : HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) (cosh x) 2 - 1)) 2 = HPow.hPow (β := ℕ) (sinh x) 2
rw₆ : HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) (sinh x) 2)) 2 = HPow.hPow (β := ℕ) (sinh x) 2
rw₇ rw₈ : HPow.hPow (β := ℕ) (sinh x) 2 = HPow.hPow (β := ℕ) (sinh x) 2
⊢ arcosh (cosh x) = x

Tactic:
rw [arcosh, ← exp_eq_exp, exp_log (by positivity), ← eq_sub_iff_add_eq', exp_sub_cosh,
    ← sq_eq_sq₀ (sqrt_nonneg _) (sinh_nonneg_iff.mpr hx), ← sinh_sq, sq_sqrt (pow_two_nonneg _)]

Premises used: Iff.mpr, eq_sub_iff_add_eq', Real.sinh_nonneg_iff, Real.exp_eq_exp, pow_two_nonneg, Real.arcosh, Real.sq_sqrt, Real.sinh_sq, Real.exp_sub_cosh, Real.exp_log, Real.sqrt_nonneg, sq_eq_sq₀
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
hx₁ : 1 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ 0 ≤ arcosh x

Tactic:
apply log_nonneg

Premises used: Real.log_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ x + 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
bc : 0 ≤ √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ x + 0 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 ≤ x
x₁ : 1 ≤ x + 0
x₂ : x + 0 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ 1 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
calc
    1 ≤ x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 < x
hx₁ : 1 < x + √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ 0 < arcosh x

Tactic:
apply log_pos

Premises used: Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 < x
⊢ 1 < x + 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 < x
bc : 0 ≤ √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ x + 0 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 < x
⊢ 0 ≤ √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 1 < x
x₁ : 1 < x + 0
x₂ : x + 0 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ 1 < x + √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
calc
    1 < x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < x + √(HPow.hPow (β := ℕ) x 2 - 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
refine : StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ x + √(HPow.hPow (β := ℕ) x 2 - 1)) (Ioi 0)
⊢ StrictMonoOn arcosh (Ioi 0)

Tactic:
refine strictMonoOn_log.comp ?_ fun x (hx : 0 < x) ↦ show 0 < x + √(x ^ 2 - 1) by positivity

Premises used: StrictMonoOn.comp, Real.strictMonoOn_log
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
hxy : x ≤ y
a : 0 ≤ x
⊢ √(HPow.hPow (β := ℕ) x 2 - 1) ≤ √(HPow.hPow (β := ℕ) y 2 - 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ x + √(HPow.hPow (β := ℕ) x 2 - 1)) (Ioi 0)

Tactic:
exact strictMonoOn_id.add_monotone fun x (hx : 0 < x) y (hy : 0 < y) hxy ↦ by gcongr

Premises used: strictMonoOn_id, StrictMonoOn.add_monotone
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ arcosh x ≤ arcosh y ↔ x ≤ y

Tactic:
strictMonoOn_arcosh.le_iff_le hx hy

Premises used: Real.strictMonoOn_arcosh, StrictMonoOn.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ arcosh x < arcosh y ↔ x < y

Tactic:
strictMonoOn_arcosh.lt_iff_lt hx hy

Premises used: Real.strictMonoOn_arcosh, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 1) x
⊢ 0 < x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
this : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Ici 1) x), 0 < x + √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x + √(HPow.hPow (β := ℕ) x 2 - 1)) (Ici 1)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
this : ∀ {x : ℝ} (hx : Membership.mem (γ := Set ℝ) (Ici 1) x), 0 < x + √(HPow.hPow (β := ℕ) x 2 - 1)
⊢ MapsTo (β := ℝ) (fun (x : ℝ) ↦ x + √(HPow.hPow (β := ℕ) x 2 - 1)) (Ici 1) {0}ᶜ

Tactic:
grind [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x y : ℝ
⊢ ContinuousOn cosh (Ioi 0)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
rw : HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x
⊢ HasStrictDerivAt arcosh (√(HPow.hPow (β := ℕ) x 2 - 1))⁻¹ x

Tactic:
rw [← sinh_arcosh (le_of_lt hx)]

Premises used: Real.sinh_arcosh, le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x

Tactic:
coshOpenPartialHomeomorph.hasStrictDerivAt_symm hx ?_ (hasStrictDerivAt_cosh _)

Premises used: Real.arcosh, Real.hasStrictDerivAt_cosh, OpenPartialHomeomorph.toFun', Real.log, dite, Real.coshOpenPartialHomeomorph, OpenPartialHomeomorph.hasStrictDerivAt_symm
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
refine : sinh (arcosh x) ≠ 0
⊢ HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x

Tactic:
refine coshOpenPartialHomeomorph.hasStrictDerivAt_symm hx ?_ (hasStrictDerivAt_cosh _)

Premises used: Real.hasStrictDerivAt_cosh, Real.coshOpenPartialHomeomorph, OpenPartialHomeomorph.hasStrictDerivAt_symm
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
rw : ¬arcosh x = 0
⊢ sinh (arcosh x) ≠ 0

Tactic:
rw [ne_eq, sinh_eq_zero]

Premises used: Real.sinh_eq_zero, ne_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ ¬arcosh x = 0

Tactic:
ne_of_gt (arcosh_pos hx)

Premises used: ne_of_gt, Real.arcosh_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ ¬arcosh x = 0

Tactic:
exact ne_of_gt (arcosh_pos hx)

Premises used: ne_of_gt, Real.arcosh_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ HasDerivAt arcosh (√(HPow.hPow (β := ℕ) x 2 - 1))⁻¹ x

Tactic:
(hasStrictDerivAt_arcosh hx).hasDerivAt

Premises used: Real.hasStrictDerivAt_arcosh, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ DifferentiableAt ℝ arcosh x

Tactic:
(hasDerivAt_arcosh hx).differentiableAt

Premises used: Real.hasDerivAt_arcosh, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ DifferentiableOn ℝ arcosh (Ioi 1)

Tactic:
fun _ hx =>
  (differentiableAt_arcosh hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, DifferentiableOn, Real.differentiableAt_arcosh
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
n : WithTop ℕ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ ContDiffAt ℝ n arcosh x

Tactic:
coshOpenPartialHomeomorph.contDiffAt_symm_deriv ?_ hx (hasDerivAt_cosh _)
    contDiff_cosh.contDiffAt

Premises used: OpenPartialHomeomorph.contDiffAt_symm_deriv, Real.arcosh, OpenPartialHomeomorph.toFun', Real.log, dite, Real.coshOpenPartialHomeomorph, Real.hasDerivAt_cosh, Real.contDiff_cosh, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
n : WithTop ℕ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
refine : sinh ((↑coshOpenPartialHomeomorph.symm : ℝ → ℝ) x) ≠ 0
⊢ ContDiffAt ℝ n arcosh x

Tactic:
refine coshOpenPartialHomeomorph.contDiffAt_symm_deriv ?_ hx (hasDerivAt_cosh _)
    contDiff_cosh.contDiffAt

Premises used: OpenPartialHomeomorph.contDiffAt_symm_deriv, Real.coshOpenPartialHomeomorph, Real.hasDerivAt_cosh, Real.contDiff_cosh, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
n : WithTop ℕ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
rw : ¬(↑coshOpenPartialHomeomorph.symm : ℝ → ℝ) x = 0
⊢ sinh ((↑coshOpenPartialHomeomorph.symm : ℝ → ℝ) x) ≠ 0

Tactic:
rw [ne_eq, sinh_eq_zero]

Premises used: Real.sinh_eq_zero, ne_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
n : WithTop ℕ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ ¬(↑coshOpenPartialHomeomorph.symm : ℝ → ℝ) x = 0

Tactic:
(arcosh_pos hx).ne'

Premises used: Real.arcosh, OpenPartialHomeomorph.toFun', Real.log, dite, LT.lt.ne', Real.arcosh_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
n : WithTop ℕ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ ¬(↑coshOpenPartialHomeomorph.symm : ℝ → ℝ) x = 0

Tactic:
exact (arcosh_pos hx).ne'

Premises used: LT.lt.ne', Real.arcosh_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
n : WithTop ℕ∞
⊢ ContDiffOn ℝ n arcosh (Ioi 1)

Tactic:
fun _ hx =>
  (contDiffAt_arcosh hx).contDiffWithinAt

Premises used: Real.contDiffAt_arcosh, ContDiffOn, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ AnalyticAt ℝ arcosh x

Tactic:
(contDiffAt_arcosh hx).analyticAt

Premises used: Real.contDiffAt_arcosh, ContDiffAt.analyticAt