awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
s : Set ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 1) x
⊢ AnalyticWithinAt ℝ arcosh s x

Tactic:
(contDiffAt_arcosh hx).contDiffWithinAt.analyticWithinAt

Premises used: Real.contDiffAt_arcosh, ContDiffWithinAt.analyticWithinAt, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
s : Set ℝ
hs : s ⊆ Ioi 1
⊢ AnalyticOnNhd ℝ arcosh s

Tactic:
fun _ hx ↦ analyticAt_arcosh (hs hx)

Premises used: AnalyticOnNhd, Real.analyticAt_arcosh
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
s : Set ℝ
hs : s ⊆ Ioi 1
⊢ AnalyticOn ℝ arcosh s

Tactic:
contDiffOn_arcosh.analyticOn.mono hs

Premises used: ContDiffOn.analyticOn, Real.contDiffOn_arcosh, AnalyticOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ BijOn cosh (Ici 0) (Ici 1)

Tactic:
coshPartialEquiv.bijOn

Premises used: Real.coshPartialEquiv, Set.Ici, setOf, PartialEquiv.bijOn, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ InjOn cosh (Ici 0)

Tactic:
coshPartialEquiv.injOn

Premises used: Real.coshPartialEquiv, Set.Ici, PartialEquiv.injOn, setOf, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ SurjOn cosh (Ici 0) (Ici 1)

Tactic:
coshPartialEquiv.surjOn

Premises used: Real.coshPartialEquiv, Set.Ici, setOf, Real.cosh, PartialEquiv.surjOn
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ BijOn arcosh (Ici 1) (Ici 0)

Tactic:
coshPartialEquiv.symm.bijOn

Premises used: Real.coshPartialEquiv, Set.Ici, setOf, Real.arcosh, PartialEquiv.bijOn, PartialEquiv.symm, Real.log, dite
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ InjOn arcosh (Ici 1)

Tactic:
coshPartialEquiv.symm.injOn

Premises used: Real.coshPartialEquiv, Set.Ici, PartialEquiv.injOn, setOf, Real.arcosh, PartialEquiv.symm, Real.log, dite
-- Module: Mathlib.Analysis.SpecialFunctions.Arcosh
Goal:
⊢ SurjOn arcosh (Ici 1) (Ici 0)

Tactic:
coshPartialEquiv.symm.surjOn

Premises used: Real.coshPartialEquiv, Set.Ici, setOf, Real.arcosh, PartialEquiv.symm, Real.log, dite, PartialEquiv.surjOn
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ 0 < HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
rw : HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2 * x * y ≤ HPow.hPow (β := ℕ) (x + y) 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) ≤ (x + y) / 2

Tactic:
rw [sqrt_le_iff_le_sq, div_pow, le_div_iff₀' (by positivity), ← mul_assoc]

Premises used: le_div_iff₀', NNReal.sqrt_le_iff_le_sq, mul_assoc, div_pow
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
norm_num : 4 * x * y ≤ HPow.hPow (β := ℕ) (x + y) 2
⊢ HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2 * x * y ≤ HPow.hPow (β := ℕ) (x + y) 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ 4 * x * y ≤ HPow.hPow (β := ℕ) (x + y) 2

Tactic:
four_mul_le_sq_add ..

Premises used: four_mul_le_sq_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ 4 * x * y ≤ HPow.hPow (β := ℕ) (x + y) 2

Tactic:
exact four_mul_le_sq_add ..

Premises used: four_mul_le_sq_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
wlog : ∀ {x y : ℝ≥0} (h : x ≠ y) (hl : y < x), (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2

Tactic:
wlog hl : y < x generalizing x y
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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) (y * x) < (y + x) / 2

Tactic:
specialize this h.symm (h.gt_or_lt.resolve_left hl)

Premises used: Or.resolve_left, Ne.symm, Ne.gt_or_lt
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : ¬y < x
this : (sqrt : (a : ℝ≥0) → ℝ≥0) (y * x) < (y + x) / 2
inr : (sqrt : (a : ℝ≥0) → ℝ≥0) (y * x) < (x + y) / 2
inr₁ inr₂ inr₃ inr₄ : (sqrt : (a : ℝ≥0) → ℝ≥0) (y * x) < (y + x) / 2
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2

Tactic:
rwa [mul_comm, add_comm]

Premises used: add_comm, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
rwa : 0 < x - y
rwa₁ rwa₂ rwa₃ rwa₄ : y < x
⊢ x - y ≠ 0

Tactic:
rwa [← zero_lt_iff, tsub_pos_iff_lt]

Premises used: tsub_pos_iff_lt, zero_lt_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ 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])
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * x - x * y - (y * x - y * y)
⊢ y * y ≤ y * x

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * x - x * y + y * y - y * x
⊢ x * y ≤ x * x

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < x * x + y * y - (x * y + y * x)
⊢ x * y + y * x = 2 * x * y

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < HPow.hPow (β := ℕ) (x - y) 2
⊢ 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

Premises used: tsub_pos_iff_lt, sq, tsub_add_eq_add_tsub, tsub_tsub_eq_add_tsub_of_le, tsub_tsub, tsub_mul, mul_tsub
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ 0 < HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ HPow.hPow (α := ℝ≥0) (β := ℕ) 2 2 * (x * y) = 2 * x * y + 2 * x * y

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
rw : 2 * x * y + 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + 2 * x * y
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) < (x + y) / 2

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]

Premises used: NNReal.sqrt_sq, lt_div_iff₀', add_sq, HDiv.hDiv, add_right_comm, div_pow, OfNat.ofNat, NNReal.sqrt_lt_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ 2 * x * y + 2 * x * y < HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + 2 * x * y

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ x.agmSequences y 0 = ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2)

Tactic:
rfl

Premises used: NNReal.agmSequences, Nat.iterate, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
⊢ x.agmSequences y (n + 1) = agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) n

Tactic:
rfl

Premises used: Function.invFun, NNReal.agmSequences, Nat.iterate, dite, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [agmSequences, agmSequences, iterate_succ', comp_apply]

Premises used: NNReal.agmSequences, Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : ∀ (n : ℕ), x.agmSequences y n = y.agmSequences x n
⊢ x.agmSequences y = y.agmSequences x

Tactic:
funext n
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ x.agmSequences y 0 = y.agmSequences x 0

Tactic:
simp [mul_comm, add_comm]

Premises used: add_comm, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
⊢ x.agmSequences y (n + 1) = y.agmSequences x (n + 1)

Tactic:
simp [agmSequences_succ, mul_comm, add_comm]

Premises used: add_comm, mul_comm, NNReal.agmSequences_succ
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
h : x.agmSequences y 0 = y.agmSequences x 0
h₁ : ∀ (n : ℕ), x.agmSequences y (n + 1) = y.agmSequences x (n + 1)
⊢ x.agmSequences y n = y.agmSequences x n

Tactic:
cases n with
  | zero => simp [mul_comm, add_comm]
  | succ n => simp [agmSequences_succ, mul_comm, add_comm]

Premises used: add_comm, mul_comm, NNReal.agmSequences_succ
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≤ y
left : x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)
right : (x + y) / 2 ≤ y
⊢ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) ∧ (x + y) / 2 ≤ y

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≤ y
left : x * x ≤ x * y
⊢ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)

Tactic:
rw [le_sqrt_iff_sq_le, sq]

Premises used: NNReal.le_sqrt_iff_sq_le, sq
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≤ y
right : x + y ≤ 2 * y
⊢ (x + y) / 2 ≤ y

Tactic:
apply div_le_of_le_mul'

Premises used: NNReal.div_le_of_le_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≤ y
right : x + y ≤ y + y
⊢ x + y ≤ 2 * y

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≤ y
⊢ x + y ≤ y + y

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
inr :
  ∀ (this : ∀ {x y : ℝ≥0} (h : x ≤ y), dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2)
    (h : ¬x ≤ y), dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2
wlog : ∀ {x y : ℝ≥0} (h : x ≤ y), dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2
⊢ dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2

Tactic:
wlog h : x ≤ y generalizing x y
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
this : ∀ {x y : ℝ≥0} (h : x ≤ y), dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2
h : ¬x ≤ y
⊢ dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2

Tactic:
simpa [add_comm, mul_comm, dist_comm] using this (not_le.mp h).le

Premises used: not_le, LT.lt.le, dist_comm, add_comm, Iff.mp, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
rw : (↑(HSub.hSub (β := ℝ≥0) ((x + y) / 2) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)) : ℝ) ≤ dist x y / 2
⊢ dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2

Tactic:
rw [dist_comm, dist_eq, ← NNReal.coe_sub (sqrt_mul_le_half_add ..), abs_eq]

Premises used: dist_comm, NNReal.abs_eq, NNReal.dist_eq, NNReal.sqrt_mul_le_half_add, NNReal.coe_sub
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
a : x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)
⊢ (↑(HSub.hSub (β := ℝ≥0) ((x + y) / 2) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)) : ℝ) ≤ (↑((x + y) / 2 - x) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
a : x * x ≤ x * y
⊢ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)

Tactic:
rw [le_sqrt_iff_sq_le, sq]

Premises used: NNReal.le_sqrt_iff_sq_le, sq
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ x * x ≤ x * y

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
nth_rw : (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
⊢ (↑((x + y) / 2 - x) : ℝ) = dist x y / 2

Tactic:
nth_rw 2 [← add_halves x]

Premises used: add_halves
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
rw : (↑(x / 2 + y / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
rw₁ : (↑(y / 2 - x / 2) : ℝ) = dist x y / 2
rw₂ : (↑((y - x) / 2) : ℝ) = dist x y / 2
rw₃ : (↑(y - x) : ℝ) / (↑2 : ℝ) = dist x y / 2
rw₄ : (↑(y - x) : ℝ) / 2 = dist x y / 2
rw₅ : (↑(y - x) : ℝ) / 2 = dist y x / 2
rw₆ : (↑(y - x) : ℝ) / 2 = |(↑y : ℝ) - (↑x : ℝ)| / 2
rw₇ : (↑(y - x) : ℝ) / 2 = |(↑(y - x) : ℝ)| / 2
rw₈ rw₉ : (↑(y - x) : ℝ) / 2 = (↑(y - x) : ℝ) / 2
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2

Tactic:
rw [add_div, add_tsub_add_eq_tsub_left, ← tsub_div, NNReal.coe_div, NNReal.coe_two, dist_comm,
        dist_eq, ← NNReal.coe_sub h, abs_eq]

Premises used: NNReal.coe_div, dist_comm, NNReal.coe_two, add_tsub_add_eq_tsub_left, NNReal.abs_eq, NNReal.dist_eq, tsub_div, NNReal.coe_sub, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
_ : (↑(HSub.hSub (β := ℝ≥0) ((x + y) / 2) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)) : ℝ) ≤ (↑((x + y) / 2 - x) : ℝ)
_₁ : (↑((x + y) / 2 - x) : ℝ) = dist x y / 2
⊢ (↑(HSub.hSub (β := ℝ≥0) ((x + y) / 2) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)) : ℝ) ≤ dist x y / 2

Tactic:
calc
    _ ≤ ((x + y) / 2 - x).toReal := by
      gcongr
      rw [le_sqrt_iff_sq_le, sq]
      gcongr
    _ = _ := by
      nth_rw 2 [← add_halves x]
      rw [add_div, add_tsub_add_eq_tsub_left, ← tsub_div, NNReal.coe_div, NNReal.coe_two, dist_comm,
        dist_eq, ← NNReal.coe_sub h, abs_eq]

Premises used: HSub.hSub, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
suffices :
  ∀ (n : ℕ),
    (x.agmSequences y n).1 ≤ (x.agmSequences y (n + 1)).1 ∧ (x.agmSequences y (n + 1)).2 ≤ (x.agmSequences y n).2
⊢ (Monotone (β := ℝ≥0) fun (n : ℕ) ↦ (x.agmSequences y n).1) ∧ Antitone (β := ℝ≥0) fun (n : ℕ) ↦ (x.agmSequences y n).2

Tactic:
suffices ∀ n, (agmSequences x y n).1 ≤ (agmSequences x y (n + 1)).1 ∧
      (agmSequences x y (n + 1)).2 ≤ (agmSequences x y n).2 from
    ⟨monotone_nat_of_le_succ (this · |>.1), antitone_nat_of_succ_le (this · |>.2)⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ (x.agmSequences y 0).1 ≤ (x.agmSequences y (HAdd.hAdd (α := ℕ) 0 1)).1 ∧
    (x.agmSequences y (HAdd.hAdd (α := ℕ) 0 1)).2 ≤ (x.agmSequences y 0).2

Tactic:
le_gm_and_am_le (sqrt_mul_le_half_add ..)

Premises used: NNReal.le_gm_and_am_le, NNReal.sqrt_mul_le_half_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ (x.agmSequences y 0).1 ≤ (x.agmSequences y (HAdd.hAdd (α := ℕ) 0 1)).1 ∧
    (x.agmSequences y (HAdd.hAdd (α := ℕ) 0 1)).2 ≤ (x.agmSequences y 0).2

Tactic:
exact le_gm_and_am_le (sqrt_mul_le_half_add ..)

Premises used: NNReal.le_gm_and_am_le, NNReal.sqrt_mul_le_half_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
n : ℕ
ih :
  ∀ {x y : ℝ≥0},
    (x.agmSequences y n).1 ≤ (x.agmSequences y (n + 1)).1 ∧ (x.agmSequences y (n + 1)).2 ≤ (x.agmSequences y n).2
x y : ℝ≥0
⊢ (x.agmSequences y (n + 1)).1 ≤ (x.agmSequences y (n + 1 + 1)).1 ∧
    (x.agmSequences y (n + 1 + 1)).2 ≤ (x.agmSequences y (n + 1)).2

Tactic:
Prod.mk_le_mk.mp ih

Premises used: Iff.mp, Prod.mk_le_mk
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
zero :
  ∀ {x y : ℝ≥0},
    (x.agmSequences y 0).1 ≤ (x.agmSequences y (HAdd.hAdd (α := ℕ) 0 1)).1 ∧
      (x.agmSequences y (HAdd.hAdd (α := ℕ) 0 1)).2 ≤ (x.agmSequences y 0).2
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {x y : ℝ≥0},
        (x.agmSequences y n).1 ≤ (x.agmSequences y (n + 1)).1 ∧ (x.agmSequences y (n + 1)).2 ≤ (x.agmSequences y n).2)
    {x y : ℝ≥0},
    (x.agmSequences y (n + 1)).1 ≤ (x.agmSequences y (n + 1 + 1)).1 ∧
      (x.agmSequences y (n + 1 + 1)).2 ≤ (x.agmSequences y (n + 1)).2
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y (n + 1)).1 ∧ (x.agmSequences y (n + 1)).2 ≤ (x.agmSequences y n).2

Tactic:
induction n generalizing x y with
  | zero => exact le_gm_and_am_le (sqrt_mul_le_half_add ..)
  | succ n ih => exact Prod.mk_le_mk.mp ih

Premises used: NNReal.le_gm_and_am_le, NNReal.sqrt_mul_le_half_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ Monotone (β := ℝ≥0) fun (n : ℕ) ↦ (x.agmSequences y n).1

Tactic:
agmSequences_monotone_and_antitone.1

Premises used: NNReal.agmSequences_monotone_and_antitone, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ Antitone (β := ℝ≥0) fun (n : ℕ) ↦ (x.agmSequences y n).2

Tactic:
agmSequences_monotone_and_antitone.2

Premises used: NNReal.agmSequences_monotone_and_antitone, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
inl : ∀ (h : n ≤ m), (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
inr : ∀ (h : m ≤ n), (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
obtain h | h := le_total n m

Premises used: le_total
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : n ≤ m
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
(agmSequences_fst_monotone h).trans this

Premises used: NNReal.agmSequences_fst_monotone, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : n ≤ m
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
exact (agmSequences_fst_monotone h).trans this

Premises used: NNReal.agmSequences_fst_monotone, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : m ≤ n
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
this.trans (agmSequences_snd_antitone h)

Premises used: NNReal.agmSequences_snd_antitone, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : m ≤ n
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
exact this.trans (agmSequences_snd_antitone h)

Premises used: NNReal.agmSequences_snd_antitone, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n m : ℕ
suffices : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
suffices ∀ {k}, (agmSequences x y k).1 ≤ (agmSequences x y k).2 by
    obtain h | h := le_total n m
    · exact (agmSequences_fst_monotone h).trans this
    · exact this.trans (agmSequences_snd_antitone h)
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
n m : ℕ
x y : ℝ≥0
⊢ (x.agmSequences y 0).1 ≤ (x.agmSequences y 0).2

Tactic:
sqrt_mul_le_half_add ..

Premises used: NNReal.sqrt_mul_le_half_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
n m : ℕ
x y : ℝ≥0
⊢ (x.agmSequences y 0).1 ≤ (x.agmSequences y 0).2

Tactic:
exact sqrt_mul_le_half_add ..

Premises used: NNReal.sqrt_mul_le_half_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
n_1 m n : ℕ
ih : ∀ {x y : ℝ≥0}, (x.agmSequences y n).1 ≤ (x.agmSequences y n).2
x y : ℝ≥0
⊢ (x.agmSequences y (n + 1)).1 ≤ (x.agmSequences y (n + 1)).2

Tactic:
ih

Premises used: Function.invFun, dite
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
n_1 m n : ℕ
ih : ∀ {x y : ℝ≥0}, (x.agmSequences y n).1 ≤ (x.agmSequences y n).2
x y : ℝ≥0
⊢ (x.agmSequences y (n + 1)).1 ≤ (x.agmSequences y (n + 1)).2

Tactic:
exact ih
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n m k : ℕ
zero : ∀ {x y : ℝ≥0}, (x.agmSequences y 0).1 ≤ (x.agmSequences y 0).2
succ :
  ∀ (n : ℕ) (ih : ∀ {x y : ℝ≥0}, (x.agmSequences y n).1 ≤ (x.agmSequences y n).2) {x y : ℝ≥0},
    (x.agmSequences y (n + 1)).1 ≤ (x.agmSequences y (n + 1)).2
⊢ (x.agmSequences y k).1 ≤ (x.agmSequences y k).2

Tactic:
induction k generalizing x y with
  | zero => exact sqrt_mul_le_half_add ..
  | succ n ih => exact ih

Premises used: NNReal.sqrt_mul_le_half_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 < (x.agmSequences y k).2
inl : ∀ (h : n ≤ m), (x.agmSequences y n).1 < (x.agmSequences y m).2
inr : ∀ (h : m ≤ n), (x.agmSequences y n).1 < (x.agmSequences y m).2
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2

Tactic:
obtain h | h := le_total n m

Premises used: le_total