awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h_1 : x ≠ y
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_lt this

Premises used: NNReal.agmSequences_fst_monotone, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h_1 : x ≠ y
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_lt this

Premises used: NNReal.agmSequences_fst_monotone, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h_1 : x ≠ y
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_le (agmSequences_snd_antitone h)

Premises used: LT.lt.trans_le, NNReal.agmSequences_snd_antitone
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h_1 : x ≠ y
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_le (agmSequences_snd_antitone h)

Premises used: LT.lt.trans_le, NNReal.agmSequences_snd_antitone
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≠ y
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_lt this
    · exact this.trans_le (agmSequences_snd_antitone h)
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
n m : ℕ
x y : ℝ≥0
h : x ≠ y
⊢ (x.agmSequences y 0).1 < (x.agmSequences y 0).2

Tactic:
sqrt_mul_lt_half_add_of_ne h

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

Tactic:
exact sqrt_mul_lt_half_add_of_ne h

Premises used: NNReal.sqrt_mul_lt_half_add_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
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
⊢ (x.agmSequences y (n + 1)).1 < (x.agmSequences y (n + 1)).2

Tactic:
rw [agmSequences_succ']

Premises used: NNReal.agmSequences_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
⊢ ((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:
sqrt_mul_lt_half_add_of_ne (ih h).ne

Premises used: NNReal.sqrt_mul_lt_half_add_of_ne, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
⊢ ((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:
exact sqrt_mul_lt_half_add_of_ne (ih h).ne

Premises used: NNReal.sqrt_mul_lt_half_add_of_ne, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
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
⊢ (x.agmSequences y k).1 < (x.agmSequences y k).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

Premises used: NNReal.sqrt_mul_lt_half_add_of_ne, NNReal.agmSequences_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
inl : ∀ (h : x ≤ y), (min x y).agmSequences (max x y) = x.agmSequences y
inr : ∀ (h : y ≤ x), (min x y).agmSequences (max x y) = x.agmSequences y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y

Tactic:
obtain h | h := le_total x y

Premises used: le_total
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : x ≤ y
inl : x.agmSequences (max x y) = x.agmSequences y
inl₁ inl₂ : x.agmSequences y = x.agmSequences y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y

Tactic:
rw [min_eq_left h, max_eq_right h]

Premises used: max_eq_right, min_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : y ≤ x
inr : y.agmSequences (max x y) = x.agmSequences y
inr₁ : y.agmSequences x = x.agmSequences y
inr₂ inr₃ : x.agmSequences y = x.agmSequences y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y

Tactic:
rw [min_eq_right h, max_eq_left h, agmSequences_comm]

Premises used: max_eq_left, min_eq_right, NNReal.agmSequences_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ dist (x.agmSequences y 0).1 (x.agmSequences y 0).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp [dist_gm_am_le]

Premises used: NNReal.dist_gm_am_le
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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)
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)
⊢ dist (x.agmSequences y (n + 1)).1 (x.agmSequences y (n + 1)).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 1)

Tactic:
rw [agmSequences_succ']

Premises used: NNReal.agmSequences_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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)
succ : dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 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)

Tactic:
apply dist_gm_am_le.trans

Premises used: LE.le.trans, NNReal.dist_gm_am_le
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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)
succ : dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1) / 2
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1 + 1)

Tactic:
rw [pow_succ, ← div_div]

Premises used: pow_succ, div_div
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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)
succ : LE.le (α := ℝ) 0 2
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 / 2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 1) / 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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)
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)
⊢ dist (x.agmSequences y n).1 (x.agmSequences y n).2 ≤ dist x y / HPow.hPow (α := ℝ) 2 (n + 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

Premises used: pow_succ, LE.le.trans, div_div, NNReal.agmSequences_succ', NNReal.dist_gm_am_le
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
apply : Tendsto (β := ℝ) (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (x.agmSequences y n).1 (x.agmSequences y n).2) atTop (𝓝 0)

Tactic:
apply squeeze_zero (fun _ ↦ dist_nonneg) dist_agmSequences_fst_snd

Premises used: squeeze_zero, NNReal.dist_agmSequences_fst_snd, dist_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
rw : Tendsto (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 (0 * (dist x y / 2)))
| Tendsto (β := ℝ) (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 0)

Tactic:
rw [← zero_mul (dist x y / 2)]

Premises used: MulZeroClass.zero_mul, HDiv.hDiv, Dist.dist, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : ∀ (n : ℕ), dist x y / HPow.hPow (α := ℝ) 2 (n + 1)
| Tendsto (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 (0 * (dist x y / 2)))

Tactic:
enter [1, n]
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
h : HPow.hPow (α := ℝ) 2⁻¹ n * (dist x y / 2)
| dist x y / HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
rw [pow_succ', ← div_div, div_eq_inv_mul, ← inv_pow]

Premises used: inv_pow, div_div, div_eq_inv_mul, pow_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : ∀ (n : ℕ), HPow.hPow (α := ℝ) 2⁻¹ n * (dist x y / 2)
| Tendsto (β := ℝ) (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 0)

Tactic:
rw [← zero_mul (dist x y / 2)]
    enter [1, n]
    rw [pow_succ', ← div_div, div_eq_inv_mul, ← inv_pow]

Premises used: MulZeroClass.zero_mul, HDiv.hDiv, inv_pow, Dist.dist, div_div, div_eq_inv_mul, OfNat.ofNat, pow_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
conv : Tendsto (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) 2⁻¹ n * (dist x y / 2)) atTop (𝓝 (0 * (dist x y / 2)))
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ dist x y / HPow.hPow (α := ℝ) 2 (t + 1)) atTop (𝓝 0)

Tactic:
conv =>
    rw [← zero_mul (dist x y / 2)]
    enter [1, n]
    rw [pow_succ', ← div_div, div_eq_inv_mul, ← inv_pow]

Premises used: MulZeroClass.zero_mul, HDiv.hDiv, inv_pow, Dist.dist, div_div, div_eq_inv_mul, OfNat.ofNat, pow_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ LE.le (α := ℝ) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ Tendsto (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) 2⁻¹ n * (dist x y / 2)) atTop (𝓝 (0 * (dist x y / 2)))

Tactic:
exact (_root_.tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num)).mul_const _

Premises used: Filter.Tendsto.mul_const, tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : ∀ (n : ℕ), (y.agmSequences x n).2
| ⨅ (n : ℕ), (y.agmSequences x n).2

Tactic:
enter [1, n]
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
h : (x.agmSequences y n).2
| (y.agmSequences x n).2

Tactic:
rw [agmSequences_comm]

Premises used: NNReal.agmSequences_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : ∀ (n : ℕ), (x.agmSequences y n).2
| ⨅ (n : ℕ), (y.agmSequences x n).2

Tactic:
enter [1, n]
    rw [agmSequences_comm]

Premises used: NNReal.agmSequences_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
conv_rhs : Eq (α := ℝ≥0) (⨅ (n : ℕ), (x.agmSequences y n).2) (⨅ (n : ℕ), (y.agmSequences x n).2)
conv_rhs₁ : Eq (α := ℝ≥0) (⨅ (n : ℕ), (x.agmSequences y n).2) (⨅ (n : ℕ), (x.agmSequences y n).2)
⊢ Eq (α := ℝ≥0) (⨅ (n : ℕ), (x.agmSequences y n).2) (⨅ (n : ℕ), (y.agmSequences x n).2)

Tactic:
conv_rhs =>
    enter [1, n]
    rw [agmSequences_comm]

Premises used: NNReal.agmSequences_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ x.agm y = ⨅ (n : ℕ), (x.agmSequences y n).2

Tactic:
rfl

Premises used: NNReal.agm, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ Tendsto (fun (n : ℕ) ↦ (x.agmSequences y n).2) atTop (𝓝 (x.agm y))

Tactic:
tendsto_atTop_ciInf agmSequences_snd_antitone (OrderBot.bddBelow _)

Premises used: NNReal.agm, tendsto_atTop_ciInf, NNReal.agmSequences_snd_antitone, OrderBot.bddBelow
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
⊢ x.agm y ≤ (x.agmSequences y n).2

Tactic:
ciInf_le' _ n

Premises used: ciInf_le', NNReal.agm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
wlog : ∀ {x y : ℝ≥0} (h : x ≤ y), x.agm y ≤ max x y
⊢ x.agm y ≤ max x y

Tactic:
wlog h : x ≤ y generalizing x y
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
this : ∀ {x y : ℝ≥0} (h : x ≤ y), x.agm y ≤ max x y
h : ¬x ≤ y
⊢ x.agm y ≤ max x y

Tactic:
simpa [agm_comm, max_comm] using this (not_le.mp h).le

Premises used: not_le, NNReal.agm_comm, LT.lt.le, Iff.mp, max_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
rw : x.agm y ≤ y
⊢ x.agm y ≤ max x y

Tactic:
rw [max_eq_right h]

Premises used: max_eq_right
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
apply : (x.agmSequences y 0).2 ≤ y
⊢ x.agm y ≤ y

Tactic:
apply (agm_le_agmSequences_snd 0).trans

Premises used: NNReal.agm_le_agmSequences_snd, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
rw : (((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2) : ℝ≥0 × ℝ≥0).2 ≤ y
⊢ (x.agmSequences y 0).2 ≤ y

Tactic:
rw [agmSequences_zero]

Premises used: NNReal.agmSequences_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ (((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2) : ℝ≥0 × ℝ≥0).2 ≤ y

Tactic:
(le_gm_and_am_le h).2

Premises used: NNReal.le_gm_and_am_le, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ (((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2) : ℝ≥0 × ℝ≥0).2 ≤ y

Tactic:
exact (le_gm_and_am_le h).2

Premises used: NNReal.le_gm_and_am_le, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
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
⊢ ∃ (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

Tactic:
use (agmSequences x y 0).2

Premises used: NNReal.agmSequences, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : ∀ (a : ℕ), (x.agmSequences y a).1 ≤ (x.agmSequences y 0).2
⊢ ∀ (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:
simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ ∀ (a : ℕ), (x.agmSequences y a).1 ≤ (x.agmSequences y 0).2

Tactic:
fun _ ↦ agmSequences_fst_le_snd ..

Premises used: NNReal.agmSequences_fst_le_snd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ ∀ (a : ℕ), (x.agmSequences y a).1 ≤ (x.agmSequences y 0).2

Tactic:
exact fun _ ↦ agmSequences_fst_le_snd ..

Premises used: NNReal.agmSequences_fst_le_snd
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ x.agm y = ⨆ (n : ℕ), (x.agmSequences y n).1

Tactic:
tendsto_nhds_unique (tendsto_agmSequences_snd_agm.congr_dist ?_)
    (tendsto_atTop_ciSup agmSequences_fst_monotone bddAbove_range_agmSequences_fst)

Premises used: tendsto_atTop_ciSup, NNReal.tendsto_agmSequences_snd_agm, NNReal.bddAbove_range_agmSequences_fst, NNReal.agmSequences_fst_monotone, tendsto_nhds_unique, Filter.Tendsto.congr_dist
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
refine : Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)
⊢ x.agm y = ⨆ (n : ℕ), (x.agmSequences y n).1

Tactic:
refine tendsto_nhds_unique (tendsto_agmSequences_snd_agm.congr_dist ?_)
    (tendsto_atTop_ciSup agmSequences_fst_monotone bddAbove_range_agmSequences_fst)

Premises used: tendsto_atTop_ciSup, NNReal.tendsto_agmSequences_snd_agm, NNReal.bddAbove_range_agmSequences_fst, NNReal.agmSequences_fst_monotone, tendsto_nhds_unique, Filter.Tendsto.congr_dist
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : ∀ (n : ℕ), dist (x.agmSequences y n).2 (x.agmSequences y n).1
| Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)

Tactic:
enter [1, n]
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
h : dist (x.agmSequences y n).1 (x.agmSequences y n).2
| dist (x.agmSequences y n).2 (x.agmSequences y n).1

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
h : ∀ (n : ℕ), dist (x.agmSequences y n).1 (x.agmSequences y n).2
| Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)

Tactic:
enter [1, n]
    rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
conv : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (x.agmSequences y n).1 (x.agmSequences y n).2) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x_1 : ℕ) ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)

Tactic:
conv =>
    enter [1, n]
    rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (x.agmSequences y n).1 (x.agmSequences y n).2) atTop (𝓝 0)

Tactic:
tendsto_dist_agmSequences_atTop_zero

Premises used: NNReal.tendsto_dist_agmSequences_atTop_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (x.agmSequences y n).1 (x.agmSequences y n).2) atTop (𝓝 0)

Tactic:
exact tendsto_dist_agmSequences_atTop_zero

Premises used: NNReal.tendsto_dist_agmSequences_atTop_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
rw : Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (x.agmSequences y n).1) atTop (𝓝 (⨆ (n : ℕ), (x.agmSequences y n).1))
⊢ Tendsto (fun (n : ℕ) ↦ (x.agmSequences y n).1) atTop (𝓝 (x.agm y))

Tactic:
rw [agm_eq_ciSup]

Premises used: NNReal.agm_eq_ciSup
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (x.agmSequences y n).1) atTop (𝓝 (⨆ (n : ℕ), (x.agmSequences y n).1))

Tactic:
tendsto_atTop_ciSup agmSequences_fst_monotone bddAbove_range_agmSequences_fst

Premises used: tendsto_atTop_ciSup, NNReal.bddAbove_range_agmSequences_fst, NNReal.agmSequences_fst_monotone
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (x.agmSequences y n).1) atTop (𝓝 (⨆ (n : ℕ), (x.agmSequences y n).1))

Tactic:
exact tendsto_atTop_ciSup agmSequences_fst_monotone bddAbove_range_agmSequences_fst

Premises used: tendsto_atTop_ciSup, NNReal.bddAbove_range_agmSequences_fst, NNReal.agmSequences_fst_monotone
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
rw : (x.agmSequences y n).1 ≤ ⨆ (n : ℕ), (x.agmSequences y n).1
⊢ (x.agmSequences y n).1 ≤ x.agm y

Tactic:
rw [agm_eq_ciSup]

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

Tactic:
le_ciSup bddAbove_range_agmSequences_fst _

Premises used: NNReal.bddAbove_range_agmSequences_fst, le_ciSup
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
⊢ (x.agmSequences y n).1 ≤ ⨆ (n : ℕ), (x.agmSequences y n).1

Tactic:
exact le_ciSup bddAbove_range_agmSequences_fst _

Premises used: NNReal.bddAbove_range_agmSequences_fst, le_ciSup
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
wlog : ∀ {x y : ℝ≥0} (h : x ≤ y), min x y ≤ x.agm y
⊢ min x y ≤ x.agm y

Tactic:
wlog h : x ≤ y generalizing x y
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
this : ∀ {x y : ℝ≥0} (h : x ≤ y), min x y ≤ x.agm y
h : ¬x ≤ y
⊢ min x y ≤ x.agm y

Tactic:
simpa [agm_comm, min_comm] using this (not_le.mp h).le

Premises used: not_le, min_comm, NNReal.agm_comm, LT.lt.le, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
rw : x ≤ x.agm y
⊢ min x y ≤ x.agm y

Tactic:
rw [min_eq_left h]

Premises used: min_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ x ≤ x.agm y

Tactic:
le_trans ?_ (agmSequences_fst_le_agm 0)

Premises used: NNReal.agmSequences_fst_le_agm, OfNat.ofNat, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
refine : x ≤ (x.agmSequences y 0).1
⊢ x ≤ x.agm y

Tactic:
refine le_trans ?_ (agmSequences_fst_le_agm 0)

Premises used: NNReal.agmSequences_fst_le_agm, OfNat.ofNat, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
rw : x ≤ ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2).1
⊢ x ≤ (x.agmSequences y 0).1

Tactic:
rw [agmSequences_zero]

Premises used: NNReal.agmSequences_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ x ≤ ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2).1

Tactic:
(le_gm_and_am_le h).1

Premises used: NNReal.le_gm_and_am_le, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
h : x ≤ y
⊢ x ≤ ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2).1

Tactic:
exact (le_gm_and_am_le h).1

Premises used: NNReal.le_gm_and_am_le, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x : ℝ≥0
a : x.agm x ≤ x
a₁ : x ≤ x.agm x
⊢ x.agm x = x

Tactic:
apply le_antisymm

Premises used: le_antisymm