awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
| ⨅ (n : ℕ), (y.agmSequences x n).2
have h : ∀ (n : ℕ), (x.agmSequences y n).2
Tactic: enter [1, n]
    rw [agmSequences_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ Eq (α := ℝ≥0) (⨅ (n : ℕ), (x.agmSequences y n).2) (⨅ (n : ℕ), (y.agmSequences x n).2)
have conv_rhs : Eq (α := ℝ≥0) (⨅ (n : ℕ), (x.agmSequences y n).2) (⨅ (n : ℕ), (y.agmSequences x n).2)
Tactic: conv_rhs =>
    enter [1, n]
    rw [agmSequences_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
conv_rhs : Eq (α := ℝ≥0) (⨅ (n : ℕ), (x.agmSequences y n).2) (⨅ (n : ℕ), (y.agmSequences x n).2)
⊢ Eq (α := ℝ≥0) (⨅ (n : ℕ), (x.agmSequences y n).2) (⨅ (n : ℕ), (y.agmSequences x n).2)
have conv_rhs₁ : Eq (α := ℝ≥0) (⨅ (n : ℕ), (x.agmSequences y n).2) (⨅ (n : ℕ), (x.agmSequences y n).2)
Tactic: conv_rhs =>
    enter [1, n]
    rw [agmSequences_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ x.agm y ≤ max x y
have inr : ∀ (this : ∀ {x y : ℝ≥0} (h : x ≤ y), x.agm y ≤ max x y) (h : ¬x ≤ y), x.agm y ≤ max x y
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), x.agm y ≤ max x y) (h : ¬x ≤ y), x.agm y ≤ max x y
⊢ x.agm y ≤ max x y
have wlog : ∀ {x y : ℝ≥0} (h : x ≤ y), x.agm y ≤ max x y
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
⊢ x.agm y ≤ max x y
have rw : x.agm y ≤ y
Tactic: rw [max_eq_right h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ x.agm y ≤ y
have apply : (x.agmSequences y 0).2 ≤ y
Tactic: apply (agm_le_agmSequences_snd 0).trans
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ (x.agmSequences y 0).2 ≤ y
have rw : (((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2) : ℝ≥0 × ℝ≥0).2 ≤ y
Tactic: rw [agmSequences_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ ∃ (x_1 : ℝ≥0),
    ∀ (y_1 : ℝ≥0), Membership.mem (γ := Set ℝ≥0) (Set.range fun (n : ℕ) ↦ (x.agmSequences y n).1) y_1 → y_1 ≤ x_1
have h : ∀ (y_1 : ℝ≥0),
  Membership.mem (γ := Set ℝ≥0) (Set.range fun (n : ℕ) ↦ (x.agmSequences y n).1) y_1 → y_1 ≤ (x.agmSequences y 0).2
Tactic: use (agmSequences x y 0).2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ ∀ (y_1 : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) (Set.range fun (n : ℕ) ↦ (x.agmSequences y n).1) y_1 → y_1 ≤ (x.agmSequences y 0).2
have h : ∀ (a : ℕ), (x.agmSequences y a).1 ≤ (x.agmSequences y 0).2
Tactic: simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ x.agm y = ⨆ (n : ℕ), (x.agmSequences y n).1
have refine : Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)
Tactic: refine tendsto_nhds_unique (tendsto_agmSequences_snd_agm.congr_dist ?_)
    (tendsto_atTop_ciSup agmSequences_fst_monotone bddAbove_range_agmSequences_fst)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
| Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)
have h : ∀ (n : ℕ), dist (x.agmSequences y n).2 (x.agmSequences y n).1
Tactic: enter [1, n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
| dist (x.agmSequences y n).2 (x.agmSequences y n).1
have h : dist (x.agmSequences y n).1 (x.agmSequences y n).2
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
| Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)
have h : ∀ (n : ℕ), dist (x.agmSequences y n).1 (x.agmSequences y n).2
Tactic: enter [1, n]
    rw [dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)
have conv : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (x.agmSequences y n).1 (x.agmSequences y n).2) atTop (𝓝 0)
Tactic: conv =>
    enter [1, n]
    rw [dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ Tendsto (fun (n : ℕ) ↦ (x.agmSequences y n).1) atTop (𝓝 (x.agm y))
have rw : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (x.agmSequences y n).1) atTop (𝓝 (⨆ (n : ℕ), (x.agmSequences y n).1))
Tactic: rw [agm_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
⊢ (x.agmSequences y n).1 ≤ x.agm y
have rw : (x.agmSequences y n).1 ≤ ⨆ (n : ℕ), (x.agmSequences y n).1
Tactic: rw [agm_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
⊢ min x y ≤ x.agm y
have inr : ∀ (this : ∀ {x y : ℝ≥0} (h : x ≤ y), min x y ≤ x.agm y) (h : ¬x ≤ y), min x y ≤ x.agm y
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), min x y ≤ x.agm y) (h : ¬x ≤ y), min x y ≤ x.agm y
⊢ min x y ≤ x.agm y
have wlog : ∀ {x y : ℝ≥0} (h : x ≤ y), min x y ≤ x.agm y
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
⊢ min x y ≤ x.agm y
have rw : x ≤ x.agm y
Tactic: rw [min_eq_left h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ x ≤ x.agm y
have refine : x ≤ (x.agmSequences y 0).1
Tactic: refine le_trans ?_ (agmSequences_fst_le_agm 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ x ≤ (x.agmSequences y 0).1
have rw : x ≤ ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2).1
Tactic: rw [agmSequences_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x : ℝ≥0
⊢ x.agm x = x
have a : x.agm x ≤ x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x : ℝ≥0
a : x.agm x ≤ x
⊢ x.agm x = x
have a₁ : x ≤ x.agm x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x : ℝ≥0
⊢ x.agm x ≤ x
have a : x.agm x ≤ max x x
Tactic: nth_rw 3 [← max_self x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x : ℝ≥0
⊢ x ≤ x.agm x
have a : min x x ≤ x.agm x
Tactic: nth_rw 1 [← min_self x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
y : ℝ≥0
⊢ agm 0 y = 0
have suffices : ∀ (n : ℕ), (agmSequences 0 y n).1 = 0
Tactic: suffices ∀ n, (agmSequences 0 y n).1 = 0 by simp [agm_eq_ciSup, this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
y : ℝ≥0
n : ℕ
ih : (agmSequences 0 y n).1 = 0
⊢ (agmSequences 0 y (n + 1)).1 = 0
have succ : Eq (α := ℝ≥0)
  (((sqrt : (a : ℝ≥0) → ℝ≥0) ((agmSequences 0 y n).1 * (agmSequences 0 y n).2),
        ((agmSequences 0 y n).1 + (agmSequences 0 y n).2) / 2).1 :
    ℝ≥0)
  (0 : ℝ≥0)
Tactic: rw [agmSequences_succ', ih, zero_mul, sqrt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
y : ℝ≥0
n : ℕ
ih : (agmSequences 0 y n).1 = 0
succ :
  Eq (α := ℝ≥0)
    (((sqrt : (a : ℝ≥0) → ℝ≥0) ((agmSequences 0 y n).1 * (agmSequences 0 y n).2),
          ((agmSequences 0 y n).1 + (agmSequences 0 y n).2) / 2).1 :
      ℝ≥0)
    (0 : ℝ≥0)
⊢ (agmSequences 0 y (n + 1)).1 = 0
have succ₁ : Eq (α := ℝ≥0) (((sqrt : (a : ℝ≥0) → ℝ≥0) (0 * (agmSequences 0 y n).2), (0 + (agmSequences 0 y n).2) / 2).1 : ℝ≥0)
  (0 : ℝ≥0)
Tactic: rw [agmSequences_succ', ih, zero_mul, sqrt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
y : ℝ≥0
n : ℕ
ih : (agmSequences 0 y n).1 = 0
succ :
  Eq (α := ℝ≥0)
    (((sqrt : (a : ℝ≥0) → ℝ≥0) ((agmSequences 0 y n).1 * (agmSequences 0 y n).2),
          ((agmSequences 0 y n).1 + (agmSequences 0 y n).2) / 2).1 :
      ℝ≥0)
    (0 : ℝ≥0)
succ₁ :
  Eq (α := ℝ≥0) (((sqrt : (a : ℝ≥0) → ℝ≥0) (0 * (agmSequences 0 y n).2), (0 + (agmSequences 0 y n).2) / 2).1 : ℝ≥0)
    (0 : ℝ≥0)
⊢ (agmSequences 0 y (n + 1)).1 = 0
have succ₂ : Eq (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 0, (0 + (agmSequences 0 y n).2) / 2).1 0
Tactic: rw [agmSequences_succ', ih, zero_mul, sqrt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
y : ℝ≥0
n : ℕ
ih : (agmSequences 0 y n).1 = 0
succ :
  Eq (α := ℝ≥0)
    (((sqrt : (a : ℝ≥0) → ℝ≥0) ((agmSequences 0 y n).1 * (agmSequences 0 y n).2),
          ((agmSequences 0 y n).1 + (agmSequences 0 y n).2) / 2).1 :
      ℝ≥0)
    (0 : ℝ≥0)
succ₁ :
  Eq (α := ℝ≥0) (((sqrt : (a : ℝ≥0) → ℝ≥0) (0 * (agmSequences 0 y n).2), (0 + (agmSequences 0 y n).2) / 2).1 : ℝ≥0)
    (0 : ℝ≥0)
succ₂ : Eq (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 0, (0 + (agmSequences 0 y n).2) / 2).1 0
⊢ (agmSequences 0 y (n + 1)).1 = 0
have succ₃ : Eq (α := ℝ≥0) (0, (0 + (agmSequences 0 y n).2) / 2).1 0
Tactic: rw [agmSequences_succ', ih, zero_mul, sqrt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
y : ℝ≥0
n : ℕ
⊢ (agmSequences 0 y n).1 = 0
have zero : (agmSequences 0 y 0).1 = 0
Tactic: induction n with
  | zero => simp [agmSequences]
  | succ n ih =>
    rw [agmSequences_succ', ih, zero_mul, sqrt_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
y : ℝ≥0
n : ℕ
zero : (agmSequences 0 y 0).1 = 0
⊢ (agmSequences 0 y n).1 = 0
have succ : ∀ (n : ℕ) (ih : (agmSequences 0 y n).1 = 0), (agmSequences 0 y (n + 1)).1 = 0
Tactic: induction n with
  | zero => simp [agmSequences]
  | succ n ih =>
    rw [agmSequences_succ', ih, zero_mul, sqrt_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x : ℝ≥0
⊢ x.agm 0 = 0
have rw : agm 0 x = 0
Tactic: rw [agm_comm, agm_zero_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x : ℝ≥0
rw : agm 0 x = 0
⊢ x.agm 0 = 0
have rw₁ : Eq (α := ℝ≥0) 0 0
Tactic: rw [agm_comm, agm_zero_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
⊢ x.agm y = (x.agmSequences y n).1.agm (x.agmSequences y n).2
have refine : Tendsto (fun (n_1 : ℕ) ↦ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 n_1).2) atTop (𝓝 (x.agm y))
Tactic: refine tendsto_nhds_unique ?_ tendsto_agmSequences_snd_agm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (hypothesis)
Goal:
x y : ℝ≥0
n : ℕ
⊢ Tendsto (fun (n_1 : ℕ) ↦ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 n_1).2) atTop (𝓝 (x.agm y))
have key : Tendsto (fun (n : ℕ) ↦ (x.agmSequences y n).2) atTop (𝓝 (x.agm y))
Tactic: have key := @tendsto_agmSequences_snd_agm x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (hypothesis)
Goal:
x y : ℝ≥0
n : ℕ
key : Tendsto (fun (n : ℕ) ↦ (x.agmSequences y n).2) atTop (𝓝 (x.agm y))
⊢ Tendsto (fun (n_1 : ℕ) ↦ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 n_1).2) atTop (𝓝 (x.agm y))
have key₁ : Tendsto (fun (n_1 : ℕ) ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
Tactic: rw [← tendsto_add_atTop_iff_nat (n + 1)] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
key : Tendsto (fun (n_1 : ℕ) ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
⊢ Tendsto (fun (n_1 : ℕ) ↦ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 n_1).2) atTop (𝓝 (x.agm y))
have h : ∀ (m : ℕ), ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 m).2 = (x.agmSequences y (m + (n + 1))).2
Tactic: convert! key using 2 with m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
key : Tendsto (fun (n_1 : ℕ) ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
m : ℕ
⊢ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 m).2 = (x.agmSequences y (m + (n + 1))).2
have h : ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[m + 1]
      (((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 =
  ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[m + (n + 1) + 1] (x, y)).2
Tactic: simp_rw [agmSequences, Prod.mk.eta, ← iterate_add_apply, add_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
n : ℕ
key : Tendsto (fun (n_1 : ℕ) ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
m : ℕ
h :
  ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[m + 1]
        (((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 =
    ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[m + (n + 1) + 1] (x, y)).2
h₁ :
  ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[m + 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))^[m + (n + 1) + 1] (x, y)).2
⊢ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 m).2 = (x.agmSequences y (m + (n + 1))).2
have h₂ : ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[m + 1 + (n + 1)] (x, y)).2 =
  ((fun (p : ℝ≥0 × ℝ≥0) ↦ ((sqrt : (a : ℝ≥0) → ℝ≥0) (p.1 * p.2), (p.1 + p.2) / 2))^[m + (n + 1) + 1] (x, y)).2
Tactic: simp_rw [agmSequences, Prod.mk.eta, ← iterate_add_apply, add_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
⊢ (x.agmSequences y n).1 < x.agm y
have rw : (x.agmSequences y n).1 < (x.agmSequences y n).1.agm (x.agmSequences y n).2
Tactic: rw [agm_eq_agm_agmSequences_fst_agmSequences_snd n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
⊢ p < p.agm q
have apply : p < (sqrt : (a : ℝ≥0) → ℝ≥0) (p * q)
Tactic: apply (?_ : p < sqrt (p * q)).trans_le (agmSequences_fst_le_agm 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (hypothesis)
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
⊢ p < (sqrt : (a : ℝ≥0) → ℝ≥0) (p * q)
have ppos : 0 < p
Tactic: have ppos : 0 < p :=
    (show 0 < sqrt (x * y) by positivity).trans_le (agmSequences_fst_monotone zero_le)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (hypothesis)
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
⊢ p < (sqrt : (a : ℝ≥0) → ℝ≥0) (p * q)
have plq : p < q
Tactic: have plq : p < q := agmSequences_fst_lt_snd_of_ne hn ..
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
plq : p < q
⊢ p < (sqrt : (a : ℝ≥0) → ℝ≥0) (p * q)
have nth_rw : HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) p : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) p : ℝ≥0) <
  HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) p : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) q : ℝ≥0)
Tactic: nth_rw 1 [← mul_self_sqrt p, sqrt_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
ppos : 0 < p
plq : p < q
⊢ HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) p : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) p : ℝ≥0) <
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) p : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) q : ℝ≥0)
have ha : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) p : ℝ≥0)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
⊢ x.agm y < (x.agmSequences y n).2
have rw : (x.agmSequences y n).1.agm (x.agmSequences y n).2 < (x.agmSequences y n).2
Tactic: rw [agm_eq_agm_agmSequences_fst_agmSequences_snd n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
⊢ p.agm q < q
have apply : (p + q) / 2 < q
Tactic: apply (agm_le_agmSequences_snd 0).trans_lt (?_ : (p + q) / 2 < q)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (hypothesis)
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
⊢ (p + q) / 2 < q
have plq : p < q
Tactic: have plq : p < q := agmSequences_fst_lt_snd_of_ne hn ..
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
plq : p < q
⊢ (p + q) / 2 < q
have nth_rw : (p + q) / 2 < q / 2 + q / 2
Tactic: nth_rw 2 [← add_halves q]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
plq : p < q
⊢ (p + q) / 2 < q / 2 + q / 2
have rw : p / 2 + q / 2 < q / 2 + q / 2
Tactic: rw [add_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
plq : p < q
⊢ p / 2 + q / 2 < q / 2 + q / 2
have bc : LT.lt (α := ℝ≥0) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
⊢ min x y < x.agm y
have inr : ∀ (this : ∀ {x y : ℝ≥0} (hx : 0 < x) (hy : 0 < y) (hn : x ≠ y) (h : x < y), min x y < x.agm y) (h : ¬x < y),
  min x y < x.agm y
Tactic: wlog h : x < y generalizing x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
inr :
  ∀ (this : ∀ {x y : ℝ≥0} (hx : 0 < x) (hy : 0 < y) (hn : x ≠ y) (h : x < y), min x y < x.agm y) (h : ¬x < y),
    min x y < x.agm y
⊢ min x y < x.agm y
have wlog : ∀ {x y : ℝ≥0} (hx : 0 < x) (hy : 0 < y) (hn : x ≠ y) (h : x < y), min x y < x.agm y
Tactic: wlog h : x < y generalizing x y
Cleared hypotheses: hx, hy, hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ min x y < x.agm y
have rw : x < x.agm y
Tactic: rw [min_eq_left h.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ x < x.agm y
have refine : x ≤ (x.agmSequences y 0).1
Tactic: refine lt_of_le_of_lt ?_ (agmSequences_fst_lt_agm_of_pos_of_ne hx hy hn 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ x ≤ (x.agmSequences y 0).1
have rw : x ≤ ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2).1
Tactic: rw [agmSequences_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hn : x ≠ y
⊢ x.agm y < max x y
have inr : ∀ (this : ∀ {x y : ℝ≥0} (hn : x ≠ y) (h : x < y), x.agm y < max x y) (h : ¬x < y), x.agm y < max x y
Tactic: wlog h : x < y generalizing x y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y : ℝ≥0
hn : x ≠ y
inr : ∀ (this : ∀ {x y : ℝ≥0} (hn : x ≠ y) (h : x < y), x.agm y < max x y) (h : ¬x < y), x.agm y < max x y
⊢ x.agm y < max x y
have wlog : ∀ {x y : ℝ≥0} (hn : x ≠ y) (h : x < y), x.agm y < max x y
Tactic: wlog h : x < y generalizing x y
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
hn : x ≠ y
h : x < y
⊢ x.agm y < max x y
have rw : x.agm y < y
Tactic: rw [max_eq_right h.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
hn : x ≠ y
h : x < y
⊢ x.agm y < y
have apply : (x.agmSequences y 0).2 ≤ y
Tactic: apply (agm_lt_agmSequences_snd_of_ne hn 0).trans_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x_1 y_1 x y : ℝ≥0
hn : x ≠ y
h : x < y
⊢ (x.agmSequences y 0).2 ≤ y
have rw : (((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2) : ℝ≥0 × ℝ≥0).2 ≤ y
Tactic: rw [agmSequences_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y k : ℝ≥0
⊢ (k * x).agm (k * y) = k * x.agm y
have simp_rw : Eq (α := ℝ≥0) (⨅ (n : ℕ), ((k * x).agmSequences (k * y) n).2) (⨅ (i : ℕ), k * (x.agmSequences y i).2)
Tactic: simp_rw [agm, mul_iInf]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
x y k : ℝ≥0
⊢ Eq (α := ℝ≥0) (⨅ (n : ℕ), ((k * x).agmSequences (k * y) n).2) (⨅ (i : ℕ), k * (x.agmSequences y i).2)
have h : ∀ (n : ℕ), ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
Tactic: congr! with n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h : (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean (goal)
Goal:
k : ℝ≥0
n : ℕ
ih : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
x y : ℝ≥0
h :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) ((k * x + k * y) / 2) n).2 =
    k * (x.agmSequences y (n + 1)).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).2 = k * (x.agmSequences y (n + 1)).2
have h₁ : (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
Tactic: rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]