awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x : ℝ≥0
a : x.agm x ≤ max x x
⊢ x.agm x ≤ x

Tactic:
nth_rw 3 [← max_self x]

Premises used: max_self
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x : ℝ≥0
⊢ x.agm x ≤ max x x

Tactic:
agm_le_max

Premises used: NNReal.agm_le_max
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x : ℝ≥0
⊢ x.agm x ≤ max x x

Tactic:
exact agm_le_max

Premises used: NNReal.agm_le_max
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x : ℝ≥0
a : min x x ≤ x.agm x
⊢ x ≤ x.agm x

Tactic:
nth_rw 1 [← min_self x]

Premises used: min_self
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x : ℝ≥0
⊢ min x x ≤ x.agm x

Tactic:
min_le_agm

Premises used: NNReal.min_le_agm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x : ℝ≥0
⊢ min x x ≤ x.agm x

Tactic:
exact min_le_agm

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

Tactic:
simp [agm_eq_ciSup, this]

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

Tactic:
suffices ∀ n, (agmSequences 0 y n).1 = 0 by simp [agm_eq_ciSup, this]
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
y : ℝ≥0
⊢ (agmSequences 0 y 0).1 = 0

Tactic:
simp [agmSequences]

Premises used: NNReal.agmSequences
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
succ₃ succ₄ : Eq (α := ℝ≥0) (0, (0 + (agmSequences 0 y n).2) / 2).1 0
⊢ (agmSequences 0 y (n + 1)).1 = 0

Tactic:
rw [agmSequences_succ', ih, zero_mul, sqrt_zero]

Premises used: NNReal.sqrt_zero, MulZeroClass.zero_mul, NNReal.agmSequences_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
y : ℝ≥0
n : ℕ
zero : (agmSequences 0 y 0).1 = 0
succ : ∀ (n : ℕ) (ih : (agmSequences 0 y n).1 = 0), (agmSequences 0 y (n + 1)).1 = 0
⊢ (agmSequences 0 y n).1 = 0

Tactic:
induction n with
  | zero => simp [agmSequences]
  | succ n ih =>
    rw [agmSequences_succ', ih, zero_mul, sqrt_zero]

Premises used: NNReal.agmSequences, NNReal.sqrt_zero, MulZeroClass.zero_mul, NNReal.agmSequences_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x : ℝ≥0
rw : agm 0 x = 0
rw₁ rw₂ : Eq (α := ℝ≥0) 0 0
⊢ x.agm 0 = 0

Tactic:
rw [agm_comm, agm_zero_left]

Premises used: NNReal.agm_comm, NNReal.agm_zero_left
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ 0 < x.agm y

Tactic:
(lt_min hx hy).trans_le min_le_agm

Premises used: lt_min, NNReal.min_le_agm, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
⊢ x.agm y = (x.agmSequences y n).1.agm (x.agmSequences y n).2

Tactic:
tendsto_nhds_unique ?_ tendsto_agmSequences_snd_agm

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

Tactic:
refine tendsto_nhds_unique ?_ tendsto_agmSequences_snd_agm

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

Tactic:
have key := @tendsto_agmSequences_snd_agm x y
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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 + (n + 1))).2) atTop (𝓝 (x.agm y))

Tactic:
rw [← tendsto_add_atTop_iff_nat (n + 1)] at key

Premises used: HAdd.hAdd, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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 + (n + 1))).2) atTop (𝓝 (x.agm y))

Tactic:
key
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
n : ℕ
key : Tendsto (fun (n_1 : ℕ) ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
h : ∀ (m : ℕ), ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 m).2 = (x.agmSequences y (m + (n + 1))).2
⊢ Tendsto (fun (n_1 : ℕ) ↦ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 n_1).2) atTop (𝓝 (x.agm y))

Tactic:
convert! key using 2 with m
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
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
⊢ ((x.agmSequences y n).1.agmSequences (x.agmSequences y n).2 m).2 = (x.agmSequences y (m + (n + 1))).2

Tactic:
simp_rw [agmSequences, Prod.mk.eta, ← iterate_add_apply, add_right_comm]

Premises used: NNReal.agmSequences, Function.iterate_add_apply, add_right_comm, Prod.mk.eta
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
⊢ x.agm y = agm ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2)

Tactic:
simpa using agm_eq_agm_agmSequences_fst_agmSequences_snd 0

Premises used: NNReal.agm_eq_agm_agmSequences_fst_agmSequences_snd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
rw : (x.agmSequences y n).1 < (x.agmSequences y n).1.agm (x.agmSequences y n).2
⊢ (x.agmSequences y n).1 < x.agm y

Tactic:
rw [agm_eq_agm_agmSequences_fst_agmSequences_snd n]

Premises used: NNReal.agm_eq_agm_agmSequences_fst_agmSequences_snd
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
set :
  let p := (x.agmSequences y n).1;
  p < p.agm (x.agmSequences y n).2
⊢ (x.agmSequences y n).1 < (x.agmSequences y n).1.agm (x.agmSequences y n).2

Tactic:
set p := (agmSequences x y n).1

Premises used: NNReal.agmSequences, Prod.fst
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
set :
  let q := (x.agmSequences y n).2;
  p < p.agm q
⊢ p < p.agm (x.agmSequences y n).2

Tactic:
set q := (agmSequences x y n).2

Premises used: NNReal.agmSequences, Prod.snd
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
apply : p < (sqrt : (a : ℝ≥0) → ℝ≥0) (p * q)
⊢ p < p.agm q

Tactic:
apply (?_ : p < sqrt (p * q)).trans_le (agmSequences_fst_le_agm 0)

Premises used: NNReal.agmSequences_fst_le_agm, LT.lt.trans_le, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
⊢ 0 < p

Tactic:
have ppos : 0 < p :=
    (show 0 < sqrt (x * y) by positivity).trans_le (agmSequences_fst_monotone zero_le)
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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 < q

Tactic:
have plq : p < q := agmSequences_fst_lt_snd_of_ne hn ..
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
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)
⊢ p < (sqrt : (a : ℝ≥0) → ℝ≥0) (p * q)

Tactic:
nth_rw 1 [← mul_self_sqrt p, sqrt_mul]

Premises used: NNReal.sqrt_mul, NNReal.mul_self_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
ha : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) p : ℝ≥0)
⊢ 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:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
rw : (x.agmSequences y n).1.agm (x.agmSequences y n).2 < (x.agmSequences y n).2
⊢ x.agm y < (x.agmSequences y n).2

Tactic:
rw [agm_eq_agm_agmSequences_fst_agmSequences_snd n]

Premises used: NNReal.agm_eq_agm_agmSequences_fst_agmSequences_snd
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
set :
  let p := (x.agmSequences y n).1;
  p.agm (x.agmSequences y n).2 < (x.agmSequences y n).2
⊢ (x.agmSequences y n).1.agm (x.agmSequences y n).2 < (x.agmSequences y n).2

Tactic:
set p := (agmSequences x y n).1

Premises used: NNReal.agmSequences, Prod.fst
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
set :
  let q := (x.agmSequences y n).2;
  p.agm q < q
⊢ p.agm (x.agmSequences y n).2 < (x.agmSequences y n).2

Tactic:
set q := (agmSequences x y n).2

Premises used: NNReal.agmSequences, Prod.snd
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
apply : (p + q) / 2 < q
⊢ p.agm q < q

Tactic:
apply (agm_le_agmSequences_snd 0).trans_lt (?_ : (p + q) / 2 < q)

Premises used: NNReal.agm_le_agmSequences_snd, OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y : ℝ≥0
hn : x ≠ y
n : ℕ
p : ℝ≥0 := (x.agmSequences y n).1
q : ℝ≥0 := (x.agmSequences y n).2
⊢ p < q

Tactic:
have plq : p < q := agmSequences_fst_lt_snd_of_ne hn ..
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
nth_rw : (p + q) / 2 < q / 2 + q / 2
⊢ (p + q) / 2 < q

Tactic:
nth_rw 2 [← add_halves q]

Premises used: add_halves
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
rw : p / 2 + q / 2 < q / 2 + q / 2
⊢ (p + q) / 2 < q / 2 + q / 2

Tactic:
rw [add_div]

Premises used: add_div
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
bc : LT.lt (α := ℝ≥0) 0 2
⊢ p / 2 + q / 2 < q / 2 + q / 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
wlog : ∀ {x y : ℝ≥0} (hx : 0 < x) (hy : 0 < y) (hn : x ≠ y) (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
hx : 0 < x
hy : 0 < y
hn : x ≠ y
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:
simpa [agm_comm, min_comm] using this hy hx hn.symm (hn.gt_or_lt.resolve_right h)

Premises used: min_comm, NNReal.agm_comm, Ne.symm, Ne.gt_or_lt, Or.resolve_right
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
rw : x < x.agm y
⊢ min x y < x.agm y

Tactic:
rw [min_eq_left h.le]

Premises used: LT.lt.le, min_eq_left
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ x < x.agm y

Tactic:
lt_of_le_of_lt ?_ (agmSequences_fst_lt_agm_of_pos_of_ne hx hy hn 0)

Premises used: lt_of_le_of_lt, NNReal.agmSequences_fst_lt_agm_of_pos_of_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
refine : x ≤ (x.agmSequences y 0).1
⊢ x < x.agm y

Tactic:
refine lt_of_le_of_lt ?_ (agmSequences_fst_lt_agm_of_pos_of_ne hx hy hn 0)

Premises used: lt_of_le_of_lt, NNReal.agmSequences_fst_lt_agm_of_pos_of_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
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
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ x ≤ ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2).1

Tactic:
(le_gm_and_am_le h.le).1

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

Tactic:
exact (le_gm_and_am_le h.le).1

Premises used: LT.lt.le, NNReal.le_gm_and_am_le, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
wlog : ∀ {x y : ℝ≥0} (hn : x ≠ y) (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
hn : x ≠ y
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:
simpa [agm_comm, max_comm] using this hn.symm (hn.gt_or_lt.resolve_right h)

Premises used: NNReal.agm_comm, Ne.symm, Ne.gt_or_lt, Or.resolve_right, max_comm
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
hn : x ≠ y
h : x < y
rw : x.agm y < y
⊢ x.agm y < max x y

Tactic:
rw [max_eq_right h.le]

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

Tactic:
apply (agm_lt_agmSequences_snd_of_ne hn 0).trans_le

Premises used: LT.lt.trans_le, OfNat.ofNat, NNReal.agm_lt_agmSequences_snd_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x_1 y_1 x y : ℝ≥0
hn : x ≠ y
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
hn : x ≠ y
h : x < y
⊢ (((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y), (x + y) / 2) : ℝ≥0 × ℝ≥0).2 ≤ y

Tactic:
(le_gm_and_am_le h.le).2

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

Tactic:
exact (le_gm_and_am_le h.le).2

Premises used: LT.lt.le, NNReal.le_gm_and_am_le, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y k : ℝ≥0
simp_rw : Eq (α := ℝ≥0) (⨅ (n : ℕ), ((k * x).agmSequences (k * y) n).2) (⨅ (i : ℕ), k * (x.agmSequences y i).2)
⊢ (k * x).agm (k * y) = k * x.agm y

Tactic:
simp_rw [agm, mul_iInf]

Premises used: NNReal.agm, NNReal.mul_iInf
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y k : ℝ≥0
h : ∀ (n : ℕ), ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2
⊢ Eq (α := ℝ≥0) (⨅ (n : ℕ), ((k * x).agmSequences (k * y) n).2) (⨅ (i : ℕ), k * (x.agmSequences y i).2)

Tactic:
congr! with n
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
k x y : ℝ≥0
⊢ ((k * x).agmSequences (k * y) 0).2 = k * (x.agmSequences y 0).2

Tactic:
simp [← mul_div_assoc, mul_add]

Premises used: mul_div_assoc, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
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
h₁ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * (x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
h₂ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * x * (k * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₃ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (k * k * (x * y))) (k * ((x + y) / 2)) n).2 = k * (x.agmSequences y (n + 1)).2
h₄ :
  (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2 * (x * y))) (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₅ :
  ((HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) (HPow.hPow (β := ℕ) k 2) : ℝ≥0)
            ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences
        (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₆ :
  ((HMul.hMul (β := ℝ≥0) k ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) : ℝ≥0)).agmSequences (k * ((x + y) / 2)) n).2 =
    k * (x.agmSequences y (n + 1)).2
h₇ : k * (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) n).2 = k * (x.agmSequences y (n + 1)).2
h₈ h₉ :
  k * (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) n).2 =
    k * (agmSequences ((sqrt : (a : ℝ≥0) → ℝ≥0) (x * y)) ((x + y) / 2) n).2
⊢ ((k * x).agmSequences (k * y) (n + 1)).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]

Premises used: mul_mul_mul_comm, NNReal.sqrt_sq, mul_div_assoc, NNReal.sqrt_mul, sq, mul_add, NNReal.agmSequences_succ
-- Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
Goal:
x y k : ℝ≥0
n : ℕ
h : ∀ {x y : ℝ≥0}, ((k * x).agmSequences (k * y) 0).2 = k * (x.agmSequences y 0).2
h₁ :
  ∀ (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
⊢ ((k * x).agmSequences (k * y) n).2 = k * (x.agmSequences y n).2

Tactic:
induction n generalizing x y with
  | zero => simp [← mul_div_assoc, mul_add]
  | succ n ih =>
    rw [agmSequences_succ, ← mul_add, mul_div_assoc, mul_mul_mul_comm,
      ← sq, sqrt_mul, sqrt_sq, ih, agmSequences_succ]

Premises used: mul_mul_mul_comm, NNReal.sqrt_sq, mul_div_assoc, NNReal.sqrt_mul, sq, mul_add, NNReal.agmSequences_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
hx : 0 < x + √(1 + HPow.hPow (β := ℕ) x 2)
⊢ rexp (arsinh x) = x + √(1 + HPow.hPow (β := ℕ) x 2)

Tactic:
apply exp_log

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
hx : -x < √(1 + HPow.hPow (β := ℕ) x 2)
⊢ 0 < x + √(1 + HPow.hPow (β := ℕ) x 2)

Tactic:
rw [← neg_lt_iff_pos_add']

Premises used: neg_lt_iff_pos_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
hx : HPow.hPow (β := ℕ) (-x) 2 < 1 + HPow.hPow (β := ℕ) x 2
⊢ -x < √(1 + HPow.hPow (β := ℕ) x 2)

Tactic:
apply lt_sqrt_of_sq_lt

Premises used: Real.lt_sqrt_of_sq_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (-x) 2 < 1 + HPow.hPow (β := ℕ) x 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
⊢ arsinh 0 = 0

Tactic:
simp [arsinh]

Premises used: Real.arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
rw : -x + √(1 + HPow.hPow (β := ℕ) (-x) 2) = (x + √(1 + HPow.hPow (β := ℕ) x 2))⁻¹
⊢ arsinh (-x) = -arsinh x

Tactic:
rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh]

Premises used: Real.exp_eq_exp, Real.exp_arsinh, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
h : (-x + √(1 + HPow.hPow (β := ℕ) (-x) 2)) * (x + √(1 + HPow.hPow (β := ℕ) x 2)) = 1
⊢ -x + √(1 + HPow.hPow (β := ℕ) (-x) 2) = (x + √(1 + HPow.hPow (β := ℕ) x 2))⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_left

Premises used: eq_inv_of_mul_eq_one_left
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
h : 0 ≤ 1 + HPow.hPow (β := ℕ) x 2
⊢ (-x + √(1 + HPow.hPow (β := ℕ) (-x) 2)) * (x + √(1 + HPow.hPow (β := ℕ) x 2)) = 1

Tactic:
rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel_right]

Premises used: neg_add_eq_sub, neg_sq, Real.sq_sqrt, add_comm, mul_comm, add_sub_cancel_right, sq_sub_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ 0 ≤ 1 + HPow.hPow (β := ℕ) x 2

Tactic:
add_nonneg zero_le_one (sq_nonneg _)

Premises used: add_nonneg, zero_le_one, sq_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ 0 ≤ 1 + HPow.hPow (β := ℕ) x 2

Tactic:
exact add_nonneg zero_le_one (sq_nonneg _)

Premises used: add_nonneg, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
rw : (x + √(1 + HPow.hPow (β := ℕ) x 2) - (-x + √(1 + HPow.hPow (β := ℕ) x 2))) / 2 = x
⊢ sinh (arsinh x) = x

Tactic:
rw [sinh_eq, ← arsinh_neg, exp_arsinh, exp_arsinh, neg_sq]

Premises used: Real.sinh_eq, Real.arsinh_neg, neg_sq, Real.exp_arsinh
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
⊢ (x + √(1 + HPow.hPow (β := ℕ) x 2) - (-x + √(1 + HPow.hPow (β := ℕ) x 2))) / 2 = x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Arsinh
Goal:
x : ℝ
rw : √(HPow.hPow (β := ℕ) (cosh (arsinh x)) 2) = √(1 + HPow.hPow (β := ℕ) x 2)
rw₁ : √(1 + HPow.hPow (β := ℕ) (sinh (arsinh x)) 2) = √(1 + HPow.hPow (β := ℕ) x 2)
rw₂ rw₃ : √(1 + HPow.hPow (β := ℕ) x 2) = √(1 + HPow.hPow (β := ℕ) x 2)
⊢ cosh (arsinh x) = √(1 + HPow.hPow (β := ℕ) x 2)

Tactic:
rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]

Premises used: Real.sinh_arsinh, LT.lt.le, Real.cosh_pos, Real.cosh_sq', Real.sqrt_sq