awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ (x + √(HPow.hPow (β := ℕ) x 2 - 1)) * (x - √(HPow.hPow (β := ℕ) x 2 - 1)) = 1
have a : HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) x 2 - 1)) 2 = 1
Tactic: rw [← pow_two_sub_pow_two, sq_sqrt (sub_nonneg_of_le (one_le_pow₀ hx)), sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
a : HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) x 2 - 1)) 2 = 1
⊢ (x + √(HPow.hPow (β := ℕ) x 2 - 1)) * (x - √(HPow.hPow (β := ℕ) x 2 - 1)) = 1
have a₁ : HPow.hPow (β := ℕ) x 2 - (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
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
⊢ (x + √(HPow.hPow (β := ℕ) x 2 - 1)) * (x - √(HPow.hPow (β := ℕ) x 2 - 1)) = 1
have a₂ : Eq (α := ℝ) 1 1
Tactic: rw [← pow_two_sub_pow_two, sq_sqrt (sub_nonneg_of_le (one_le_pow₀ hx)), sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ cosh (arcosh x) = x
have rw : (x + √(HPow.hPow (β := ℕ) x 2 - 1) + (x - √(HPow.hPow (β := ℕ) x 2 - 1))) / 2 = x
Tactic: rw [arcosh, cosh_eq, exp_neg, exp_log (by positivity), add_sqrt_self_sq_sub_one_inv hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ arcosh x = 0 ↔ x = 1
have rw : x + √(HPow.hPow (β := ℕ) x 2 - 1) = 1 ↔ x = 1
Tactic: rw [← exp_injective.eq_iff, exp_arcosh hx, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ sinh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1)
have rw : (x + √(HPow.hPow (β := ℕ) x 2 - 1) - (x - √(HPow.hPow (β := ℕ) x 2 - 1))) / 2 = √(HPow.hPow (β := ℕ) x 2 - 1)
Tactic: rw [arcosh, sinh_eq, exp_neg, exp_log (by positivity), add_sqrt_self_sq_sub_one_inv hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ tanh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x
have rw : sinh (arcosh x) / cosh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_arcosh hx, cosh_arcosh hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
rw : sinh (arcosh x) / cosh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x
⊢ tanh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x
have rw₁ : √(HPow.hPow (β := ℕ) x 2 - 1) / cosh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_arcosh hx, cosh_arcosh hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
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
⊢ tanh (arcosh x) = √(HPow.hPow (β := ℕ) x 2 - 1) / x
have rw₂ : √(HPow.hPow (β := ℕ) x 2 - 1) / x = √(HPow.hPow (β := ℕ) x 2 - 1) / x
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_arcosh hx, cosh_arcosh hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ arcosh (cosh x) = x
have rw : log (cosh x + √(HPow.hPow (β := ℕ) (cosh x) 2 - 1)) = 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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 0 ≤ x
rw : log (cosh x + √(HPow.hPow (β := ℕ) (cosh x) 2 - 1)) = x
⊢ arcosh (cosh x) = x
have rw₁ : rexp (log (cosh x + √(HPow.hPow (β := ℕ) (cosh x) 2 - 1))) = rexp 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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
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
⊢ arcosh (cosh x) = x
have rw₂ : cosh x + √(HPow.hPow (β := ℕ) (cosh x) 2 - 1) = rexp 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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
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
⊢ arcosh (cosh x) = x
have rw₃ : √(HPow.hPow (β := ℕ) (cosh x) 2 - 1) = rexp x - cosh 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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
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
⊢ arcosh (cosh x) = x
have rw₄ : √(HPow.hPow (β := ℕ) (cosh x) 2 - 1) = sinh 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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
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
⊢ arcosh (cosh x) = x
have rw₅ : HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) (cosh x) 2 - 1)) 2 = HPow.hPow (β := ℕ) (sinh x) 2
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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
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
⊢ arcosh (cosh x) = x
have rw₆ : HPow.hPow (β := ℕ) (√(HPow.hPow (β := ℕ) (sinh x) 2)) 2 = HPow.hPow (β := ℕ) (sinh x) 2
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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
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
⊢ arcosh (cosh x) = x
have rw₇ : HPow.hPow (β := ℕ) (sinh x) 2 = HPow.hPow (β := ℕ) (sinh x) 2
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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ arcosh x
have hx₁ : 1 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
Tactic: apply log_nonneg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ x + 0 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
have bc : 0 ≤ √(HPow.hPow (β := ℕ) x 2 - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
have x₁ : 1 ≤ x + 0
Tactic: calc
    1 ≤ x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 ≤ x
x₁ : 1 ≤ x + 0
⊢ 1 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
have x₂ : x + 0 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
Tactic: calc
    1 ≤ x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 < x
⊢ 0 < arcosh x
have hx₁ : 1 < x + √(HPow.hPow (β := ℕ) x 2 - 1)
Tactic: apply log_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 < x
⊢ x + 0 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
have bc : 0 ≤ √(HPow.hPow (β := ℕ) x 2 - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 < x
⊢ 1 < x + √(HPow.hPow (β := ℕ) x 2 - 1)
have x₁ : 1 < x + 0
Tactic: calc
    1 < x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 1 < x
x₁ : 1 < x + 0
⊢ 1 < x + √(HPow.hPow (β := ℕ) x 2 - 1)
have x₂ : x + 0 ≤ x + √(HPow.hPow (β := ℕ) x 2 - 1)
Tactic: calc
    1 < x + 0 := by simpa
    _ ≤ x + √(x ^ 2 - 1) := by gcongr; positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
⊢ StrictMonoOn arcosh (Ioi 0)
have refine : StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ x + √(HPow.hPow (β := ℕ) x 2 - 1)) (Ioi 0)
Tactic: refine strictMonoOn_log.comp ?_ fun x (hx : 0 < x) ↦ show 0 < x + √(x ^ 2 - 1) by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
hxy : x ≤ y
⊢ √(HPow.hPow (β := ℕ) x 2 - 1) ≤ √(HPow.hPow (β := ℕ) y 2 - 1)
have a : 0 ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ HasStrictDerivAt arcosh (√(HPow.hPow (β := ℕ) x 2 - 1))⁻¹ x
have rw : HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x
Tactic: rw [← sinh_arcosh (le_of_lt hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ HasStrictDerivAt arcosh (sinh (arcosh x))⁻¹ x
have refine : sinh (arcosh x) ≠ 0
Tactic: refine coshOpenPartialHomeomorph.hasStrictDerivAt_symm hx ?_ (hasStrictDerivAt_cosh _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ sinh (arcosh x) ≠ 0
have rw : ¬arcosh x = 0
Tactic: rw [ne_eq, sinh_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
n : WithTop ℕ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ ContDiffAt ℝ n arcosh x
have refine : sinh ((↑coshOpenPartialHomeomorph.symm : ℝ → ℝ) x) ≠ 0
Tactic: refine coshOpenPartialHomeomorph.contDiffAt_symm_deriv ?_ hx (hasDerivAt_cosh _)
    contDiff_cosh.contDiffAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Arcosh (goal)
Goal:
n : WithTop ℕ∞
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ sinh ((↑coshOpenPartialHomeomorph.symm : ℝ → ℝ) x) ≠ 0
have rw : ¬(↑coshOpenPartialHomeomorph.symm : ℝ → ℝ) x = 0
Tactic: rw [ne_eq, sinh_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) ≤ (x + y) / 2
have rw : HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2 * x * y ≤ HPow.hPow (β := ℕ) (x + y) 2
Tactic: rw [sqrt_le_iff_le_sq, div_pow, le_div_iff₀' (by positivity), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2 * x * y ≤ HPow.hPow (β := ℕ) (x + y) 2
have norm_num : 4 * x * y ≤ HPow.hPow (β := ℕ) (x + y) 2
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
have inr : ∀ (this : ∀ {x y : ℝ≥0} (h : x ≠ y) (hl : y < x), (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2) (hl : ¬y < x),
  (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
Tactic: wlog hl : y < x generalizing x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
inr :
  ∀ (this : ∀ {x y : ℝ≥0} (h : x ≠ y) (hl : y < x), (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2) (hl : ¬y < x),
    (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
have wlog : ∀ {x y : ℝ≥0} (h : x ≠ y) (hl : y < x), (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
Tactic: wlog hl : y < x generalizing x y
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (hypothesis)
Goal:
x y : ℝ≥0
h : x ≠ y
this : ∀ {x y : ℝ≥0} (h : x ≠ y) (hl : y < x), (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
hl : ¬y < x
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
have this₁ : (sqrt : (a : ℝ≥0) → ℝ≥0) (y * x) < (y + x) / 2
Tactic: specialize this h.symm (h.gt_or_lt.resolve_left hl)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
hl : ¬y < x
this : (sqrt : (a : ℝ≥0) → ℝ≥0) (y * x) < (y + x) / 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
have inr : (sqrt : (a : ℝ≥0) → ℝ≥0) (y * x) < (x + y) / 2
Tactic: rwa [mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ x - y ≠ 0
have rwa : 0 < x - y
Tactic: rwa [← zero_lt_iff, tsub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (hypothesis)
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
have key : 0 < HPow.hPow (β := ℕ) (x - y) 2
Tactic: have key : 0 < (x - y) ^ 2 := sq_pos_iff.mpr (by rwa [← zero_lt_iff, tsub_pos_iff_lt])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (hypothesis)
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < HPow.hPow (β := ℕ) (x - y) 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
have key₁ : 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: rw [sq, tsub_mul, mul_tsub, mul_tsub, tsub_tsub_eq_add_tsub_of_le (by gcongr),
    tsub_add_eq_add_tsub (by gcongr), tsub_tsub, show x * y + y * x = 2 * x * y by ring,
    tsub_pos_iff_lt, ← sq, ← sq] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
have rw : 2 * x * y + 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + 2 * x * y
Tactic: rw [← sqrt_sq (_ / 2), sqrt_lt_sqrt, div_pow, lt_div_iff₀' (by positivity),
    show (2 : ℝ≥0) ^ 2 * (x * y) = 2 * x * y + 2 * x * y by ring, add_sq, add_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
⊢ x.agmSequences y (n + 1) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0) ((x.agmSequences y n).1 * (x.agmSequences y n).2),
      ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
have rw : (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
  ((sqrt : (a : ℝ≥0) → ℝ≥0) ((x.agmSequences y n).1 * (x.agmSequences y n).2),
    ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
Tactic: rw [agmSequences, agmSequences, iterate_succ', comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
rw :
  (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0) ((x.agmSequences y n).1 * (x.agmSequences y n).2),
      ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
⊢ x.agmSequences y (n + 1) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0) ((x.agmSequences y n).1 * (x.agmSequences y n).2),
      ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
have rw₁ : (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
  ((sqrt : (a : ℝ≥0) → ℝ≥0)
      (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
        ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
    (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
        ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
      2)
Tactic: rw [agmSequences, agmSequences, iterate_succ', comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
rw :
  (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0) ((x.agmSequences y n).1 * (x.agmSequences y n).2),
      ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
rw₁ :
  (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0)
        (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2)
⊢ x.agmSequences y (n + 1) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0) ((x.agmSequences y n).1 * (x.agmSequences y n).2),
      ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
have rw₂ : Eq (α := ℝ≥0 × ℝ≥0)
  (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2)) ∘
        (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1])
      (x, y) :
    ℝ≥0 × ℝ≥0)
  (((sqrt : (a : ℝ≥0) → ℝ≥0)
        (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2) :
    ℝ≥0 × ℝ≥0)
Tactic: rw [agmSequences, agmSequences, iterate_succ', comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
rw :
  (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0) ((x.agmSequences y n).1 * (x.agmSequences y n).2),
      ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
rw₁ :
  (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1 + 1] (x, y) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0)
        (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2)
rw₂ :
  Eq (α := ℝ≥0 × ℝ≥0)
    (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2)) ∘
          (fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1])
        (x, y) :
      ℝ≥0 × ℝ≥0)
    (((sqrt : (a : ℝ≥0) → ℝ≥0)
          (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
            ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
        (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
            ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
          2) :
      ℝ≥0 × ℝ≥0)
⊢ x.agmSequences y (n + 1) =
    ((sqrt : (a : ℝ≥0) → ℝ≥0) ((x.agmSequences y n).1 * (x.agmSequences y n).2),
      ((x.agmSequences y n).1 + (x.agmSequences y n).2) / 2)
have rw₃ : Eq (α := ℝ≥0 × ℝ≥0)
  (((sqrt : (a : ℝ≥0) → ℝ≥0)
        (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2) :
    ℝ≥0 × ℝ≥0)
  (((sqrt : (a : ℝ≥0) → ℝ≥0)
        (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 *
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2),
      (((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).1 +
          ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[n + 1] (x, y)).2) /
        2) :
    ℝ≥0 × ℝ≥0)
Tactic: rw [agmSequences, agmSequences, iterate_succ', comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ x.agmSequences y = y.agmSequences x
have h : ∀ (n : ℕ), x.agmSequences y n = y.agmSequences x n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
⊢ x.agmSequences y n = y.agmSequences x n
have h : x.agmSequences y 0 = y.agmSequences x 0
Tactic: cases n with
  | zero => simp [mul_comm, add_comm]
  | succ n => simp [agmSequences_succ, mul_comm, add_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
h : x.agmSequences y 0 = y.agmSequences x 0
⊢ x.agmSequences y n = y.agmSequences x n
have h₁ : ∀ (n : ℕ), x.agmSequences y (n + 1) = y.agmSequences x (n + 1)
Tactic: cases n with
  | zero => simp [mul_comm, add_comm]
  | succ n => simp [agmSequences_succ, mul_comm, add_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≤ y
⊢ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) ∧ (x + y) / 2 ≤ y
have left : x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≤ y
left : x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)
⊢ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) ∧ (x + y) / 2 ≤ y
have right : (x + y) / 2 ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≤ y
⊢ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)
have left : x * x ≤ x * y
Tactic: rw [le_sqrt_iff_sq_le, sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≤ y
⊢ (x + y) / 2 ≤ y
have right : x + y ≤ 2 * y
Tactic: apply div_le_of_le_mul'