awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≤ y + y
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2
have 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
Tactic: wlog h : x ≤ y generalizing x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2
have wlog : ∀ {x y : ℝ≥0} (h : x ≤ y), dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2
Tactic: wlog h : x ≤ y generalizing x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ dist ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) ≤ dist x y / 2
have rw : (↑(HSub.hSub (β := ℝ≥0) ((x + y) / 2) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)) : ℝ) ≤ dist x y / 2
Tactic: rw [dist_comm, dist_eq, ← NNReal.coe_sub (sqrt_mul_le_half_add ..), abs_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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) : ℝ)
have a : x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)
have a : x * x ≤ x * y
Tactic: rw [le_sqrt_iff_sq_le, sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ (↑((x + y) / 2 - x) : ℝ) = dist x y / 2
have nth_rw : (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
Tactic: nth_rw 2 [← add_halves x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw : (↑(x / 2 + 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
rw : (↑(x / 2 + y / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw₁ : (↑(y / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw₂ : (↑((y - 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw₃ : (↑(y - 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw₄ : (↑(y - 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw₅ : (↑(y - x) : ℝ) / 2 = dist y x / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw₆ : (↑(y - x) : ℝ) / 2 = |(↑y : ℝ) - (↑x : ℝ)| / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw₇ : (↑(y - x) : ℝ) / 2 = |(↑(y - x) : ℝ)| / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (↑((x + y) / 2 - (x / 2 + x / 2)) : ℝ) = dist x y / 2
have rw₈ : (↑(y - x) : ℝ) / 2 = (↑(y - x) : ℝ) / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ (↑(HSub.hSub (β := ℝ≥0) ((x + y) / 2) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)) : ℝ) ≤ dist x y / 2
have _ : (↑(HSub.hSub (β := ℝ≥0) ((x + y) / 2) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)) : ℝ) ≤ (↑((x + y) / 2 - x) : ℝ)
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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) : ℝ)
⊢ (↑(HSub.hSub (β := ℝ≥0) ((x + y) / 2) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)) : ℝ) ≤ dist x y / 2
have _₁ : (↑((x + y) / 2 - x) : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ (Monotone (β := ℝ≥0) fun (n : ℕ) ↦ (x.agmSequences y n).1) ∧ Antitone (β := ℝ≥0) fun (n : ℕ) ↦ (x.agmSequences y n).2
have suffices : ∀ (n : ℕ), (x.agmSequences y n).1 ≤ (x.agmSequences y (n + 1)).1 ∧ (x.agmSequences y (n + 1)).2 ≤ (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)⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y (n + 1)).1 ∧ (x.agmSequences y (n + 1)).2 ≤ (x.agmSequences y n).2
have 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
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
Cleared hypotheses: x, y, n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y (n + 1)).1 ∧ (x.agmSequences y (n + 1)).2 ≤ (x.agmSequences y n).2
have 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
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
Cleared hypotheses: x, y, n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
have inl : ∀ (h : n ≤ m), (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
Tactic: obtain h | h := le_total n m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
have inr : ∀ (h : m ≤ n), (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
Tactic: obtain h | h := le_total n m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n m : ℕ
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
have suffices : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n m k : ℕ
⊢ (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
have zero : ∀ {x y : ℝ≥0}, (x.agmSequences y 0).1 ≤ (x.agmSequences y 0).2
Tactic: induction k generalizing x y with
  | zero => exact sqrt_mul_le_half_add ..
  | succ n ih => exact ih
Cleared hypotheses: x, y, k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n m k : ℕ
zero : ∀ {x y : ℝ≥0}, (x.agmSequences y 0).1 ≤ (x.agmSequences y 0).2
⊢ (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
have 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
Tactic: induction k generalizing x y with
  | zero => exact sqrt_mul_le_half_add ..
  | succ n ih => exact ih
Cleared hypotheses: x, y, k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 < (x.agmSequences y k).2
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2
have inl : ∀ (h : n ≤ m), (x.agmSequences y n).1 < (x.agmSequences y m).2
Tactic: obtain h | h := le_total n m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
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
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2
have inr : ∀ (h : m ≤ n), (x.agmSequences y n).1 < (x.agmSequences y m).2
Tactic: obtain h | h := le_total n m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
n m : ℕ
⊢ (x.agmSequences y n).1 < (x.agmSequences y m).2
have suffices : ∀ {k : ℕ}, (x.agmSequences y k).1 < (x.agmSequences y k).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_lt this
    · exact this.trans_le (agmSequences_snd_antitone h)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
n_1 m n : ℕ
ih : ∀ {x y : ℝ≥0} (h : x ≠ y), (x.agmSequences y n).1 < (x.agmSequences y n).2
x y : ℝ≥0
h : x ≠ y
⊢ (x.agmSequences y (n + 1)).1 < (x.agmSequences y (n + 1)).2
have succ : ((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).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) :
      ℝ≥0 × ℝ≥0).2
Tactic: rw [agmSequences_succ']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
n m k : ℕ
⊢ (x.agmSequences y k).1 < (x.agmSequences y k).2
have zero : ∀ {x y : ℝ≥0} (h : x ≠ y), (x.agmSequences y 0).1 < (x.agmSequences y 0).2
Tactic: induction k generalizing x y with
  | zero => exact sqrt_mul_lt_half_add_of_ne h
  | succ n ih =>
    rw [agmSequences_succ']
    exact sqrt_mul_lt_half_add_of_ne (ih h).ne
Cleared hypotheses: x, y, h, k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≠ y
n m k : ℕ
zero : ∀ {x y : ℝ≥0} (h : x ≠ y), (x.agmSequences y 0).1 < (x.agmSequences y 0).2
⊢ (x.agmSequences y k).1 < (x.agmSequences y k).2
have succ : ∀ (n : ℕ) (ih : ∀ {x y : ℝ≥0} (h : x ≠ y), (x.agmSequences y n).1 < (x.agmSequences y n).2) {x y : ℝ≥0} (h : x ≠ y),
  (x.agmSequences y (n + 1)).1 < (x.agmSequences y (n + 1)).2
Tactic: induction k generalizing x y with
  | zero => exact sqrt_mul_lt_half_add_of_ne h
  | succ n ih =>
    rw [agmSequences_succ']
    exact sqrt_mul_lt_half_add_of_ne (ih h).ne
Cleared hypotheses: x, y, h, k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
have inl : ∀ (h : x ≤ y), (min x y).agmSequences (max x y) = x.agmSequences y
Tactic: obtain h | h := le_total x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
inl : ∀ (h : x ≤ y), (min x y).agmSequences (max x y) = x.agmSequences y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
have inr : ∀ (h : y ≤ x), (min x y).agmSequences (max x y) = x.agmSequences y
Tactic: obtain h | h := le_total x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≤ y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
have inl : x.agmSequences (max x y) = x.agmSequences y
Tactic: rw [min_eq_left h, max_eq_right h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : x ≤ y
inl : x.agmSequences (max x y) = x.agmSequences y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
have inl₁ : x.agmSequences y = x.agmSequences y
Tactic: rw [min_eq_left h, max_eq_right h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : y ≤ x
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
have inr : y.agmSequences (max x y) = x.agmSequences y
Tactic: rw [min_eq_right h, max_eq_left h, agmSequences_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : y ≤ x
inr : y.agmSequences (max x y) = x.agmSequences y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
have inr₁ : y.agmSequences x = x.agmSequences y
Tactic: rw [min_eq_right h, max_eq_left h, agmSequences_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
h : y ≤ x
inr : y.agmSequences (max x y) = x.agmSequences y
inr₁ : y.agmSequences x = x.agmSequences y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
have inr₂ : x.agmSequences y = x.agmSequences y
Tactic: rw [min_eq_right h, max_eq_left h, agmSequences_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ dist (x.agmSequences y (n + 1)).1 (x.agmSequences y (n + 1)).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
have succ : dist
    ((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).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) :
        ℝ≥0 × ℝ≥0).2 ≤
  dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
Tactic: rw [agmSequences_succ']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ dist
      ((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).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) :
          ℝ≥0 × ℝ≥0).2 ≤
    dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
have succ : dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
Tactic: apply dist_gm_am_le.trans
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
have succ : dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1) / 2
Tactic: rw [pow_succ, ← div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1) / 2
have succ : LE.le (α := ℝ) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
have zero : dist (x.agmSequences y 0).1 (x.agmSequences y 0).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)
Tactic: induction n with
  | zero => simp [dist_gm_am_le]
  | succ n ih =>
    rw [agmSequences_succ']
    apply dist_gm_am_le.trans
    rw [pow_succ, ← div_div]
    gcongr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
zero : dist (x.agmSequences y 0).1 (x.agmSequences y 0).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
have succ : ∀ (n : ℕ) (ih : dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1)),
  dist (x.agmSequences y (n + 1)).1 (x.agmSequences y (n + 1)).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 1)
Tactic: induction n with
  | zero => simp [dist_gm_am_le]
  | succ n ih =>
    rw [agmSequences_succ']
    apply dist_gm_am_le.trans
    rw [pow_succ, ← div_div]
    gcongr
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (x.agmSequences y n).1 (x.agmSequences y n).2) atTop (𝓝 0)
have apply : Tendsto (β := ℝ) (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 0)
Tactic: apply squeeze_zero (fun _ ↦ dist_nonneg) dist_agmSequences_fst_snd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
| Tendsto (β := ℝ) (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 0)
have rw : Tendsto (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 (0 * (dist x y / 2)))
Tactic: rw [← zero_mul (dist x y / 2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
| Tendsto (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 (0 * (dist x y / 2)))
have h : ∀ (n : ℕ), dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: enter [1, n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
| dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
have h : HPow.hPow (α := ℝ) 2⁻¹ n * (dist x y / 2)
Tactic: rw [pow_succ', ← div_div, div_eq_inv_mul, ← inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
| Tendsto (β := ℝ) (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 0)
have h : ∀ (n : ℕ), HPow.hPow (α := ℝ) 2⁻¹ n * (dist x y / 2)
Tactic: rw [← zero_mul (dist x y / 2)]
    enter [1, n]
    rw [pow_succ', ← div_div, div_eq_inv_mul, ← inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 0)
have conv : Tendsto (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) 2⁻¹ n * (dist x y / 2)) atTop (𝓝 (0 * (dist x y / 2)))
Tactic: conv =>
    rw [← zero_mul (dist x y / 2)]
    enter [1, n]
    rw [pow_succ', ← div_div, div_eq_inv_mul, ← inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
| ⨅ (n : ℕ), (y.agmSequences x n).2
have h : ∀ (n : ℕ), (y.agmSequences x n).2
Tactic: enter [1, n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
| (y.agmSequences x n).2
have h : (x.agmSequences y n).2
Tactic: rw [agmSequences_comm]