mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have hv₁ (x) : HasDerivAt v₁ (v₁' x) x := (hasDerivAt_mul_const θ).sin

Goal state after:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
h : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → y < x → sqrt (x * y) < (x + y) / 2
hl : ¬y < x
⊢ sqrt (x * y) < (x + y) / 2

pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
·

Goal state after:
case inr
x y : ℝ≥0
h : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → y < x → sqrt (x * y) < (x + y) / 2
hl : ¬y < x
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case left
x y : ℝ≥0
h : x ≤ y
⊢ x ≤ sqrt (x * y)

pp: case right
x y : ℝ≥0
h : x ≤ y
⊢ (x + y) / 2 ≤ y

Tactic:
·

Goal state after:
case left
x y : ℝ≥0
h : x ≤ y
⊢ x ≤ sqrt (x * y)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case right
x y : ℝ≥0
h : x ≤ y
⊢ (x + y) / 2 ≤ y

Tactic:
·

Goal state after:
case right
x y : ℝ≥0
h : x ≤ y
⊢ (x + y) / 2 ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < 2 * z.re

pp: case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ 2 * z.re ≤ π

Tactic:
·

Goal state after:
case hx₁
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -π < 2 * z.re
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2
h : ¬x ≤ y
⊢ dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2

pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2

Tactic:
·

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2
h : ¬x ≤ y
⊢ dist (sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ 2 * z.re ≤ π

Tactic:
·

Goal state after:
case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ 2 * z.re ≤ π
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 = (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ

pp: case convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
·

Goal state after:
case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 = (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inl
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : n ≤ m
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

pp: case inr
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : m ≤ n
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
·

Goal state after:
case inl
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : n ≤ m
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : m ≤ n
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
·

Goal state after:
case inr
x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
h : m ≤ n
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inl
x y : ℝ≥0
h✝ : 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

pp: case inr
x y : ℝ≥0
h✝ : 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:
·

Goal state after:
case inl
x y : ℝ≥0
h✝ : 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
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
h✝ : 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:
·

Goal state after:
case inr
x y : ℝ≥0
h✝ : 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
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₀
x : ℝ
⊢ ¬Real.arctan x = π / 2

pp: case h₁
x : ℝ
⊢ -(π / 2) < Real.arctan x

pp: case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2

Tactic:
·

Goal state after:
case h₀
x : ℝ
⊢ ¬Real.arctan x = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₁
x : ℝ
⊢ -(π / 2) < Real.arctan x

pp: case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2

Tactic:
·

Goal state after:
case h₁
x : ℝ
⊢ -(π / 2) < Real.arctan x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2

Tactic:
·

Goal state after:
case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inl
x y : ℝ≥0
h : x ≤ y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y

pp: case inr
x y : ℝ≥0
h : y ≤ x
⊢ (min x y).agmSequences (max x y) = x.agmSequences y

Tactic:
·

Goal state after:
case inl
x y : ℝ≥0
h : x ≤ y
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
h : y ≤ x
⊢ (min x y).agmSequences (max x y) = x.agmSequences y

Tactic:
·

Goal state after:
case inr
x y : ℝ≥0
h : y ≤ x
⊢ (min x y).agmSequences (max x y) = x.agmSequences y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → x.agm y ≤ max x y
h : ¬x ≤ y
⊢ x.agm y ≤ max x y

pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ x.agm y ≤ max x y

Tactic:
·

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → x.agm y ≤ max x y
h : ¬x ≤ y
⊢ x.agm y ≤ max x y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → min x y ≤ x.agm y
h : ¬x ≤ y
⊢ min x y ≤ x.agm y

pp: x✝ y✝ x y : ℝ≥0
h : x ≤ y
⊢ min x y ≤ x.agm y

Tactic:
·

Goal state after:
case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → min x y ≤ x.agm y
h : ¬x ≤ y
⊢ min x y ≤ x.agm y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case a
x : ℝ≥0
⊢ x.agm x ≤ x

pp: case a
x : ℝ≥0
⊢ x ≤ x.agm x

Tactic:
·

Goal state after:
case a
x : ℝ≥0
⊢ x.agm x ≤ x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case a
x : ℝ≥0
⊢ x ≤ x.agm x

Tactic:
·

Goal state after:
case a
x : ℝ≥0
⊢ x ≤ x.agm x
Module: Mathlib.Analysis.SpecialFunctions.Artanh

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
this : 0 < √((1 + x) / (1 - x))
⊢ cosh (artanh x) = 1 / √(1 - x ^ 2)

Tactic:
rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]
    <;> grind [artanh, cosh_eq, exp_neg, exp_log, sqrt_div]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: 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 (p * q)

Tactic:
have ppos : 0 < p :=
    (show 0 < sqrt (x * y) by positivity).trans_le (agmSequences_fst_monotone zero_le)

Goal state after:
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 (p * q)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
n : ℕ
⊢ (x.agmSequences y n).1 < x.agm y

Tactic:
by
  rw [agm_eq_agm_agmSequences_fst_agmSequences_snd n]
  set p := (agmSequences x y n).1
  set q := (agmSequences x y n).2
  apply (?_ : p < sqrt (p * q)).trans_le (agmSequences_fst_le_agm 0)
  have ppos : 0 < p :=
    (show 0 < sqrt (x * y) by positivity).trans_le (agmSequences_fst_monotone zero_le)
  have plq : p < q := agmSequences_fst_lt_snd_of_ne hn ..
  nth_rw 1 [← mul_self_sqrt p, sqrt_mul]
  gcongr

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
this : ∀ {x y : ℝ≥0}, 0 < x → 0 < y → x ≠ y → x < y → min x y < x.agm y
h : ¬x < y
⊢ min x y < x.agm y

pp: x✝ y✝ x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
h : x < y
⊢ min x y < x.agm y

Tactic:
·

Goal state after:
case inr
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
hn : x ≠ y
this : ∀ {x y : ℝ≥0}, 0 < x → 0 < y → x ≠ y → x < y → min x y < x.agm y
h : ¬x < y
⊢ min x y < x.agm y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
hn : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → x < y → x.agm y < max x y
h : ¬x < y
⊢ x.agm y < max x y

pp: x✝ y✝ x y : ℝ≥0
hn : x ≠ y
h : x < y
⊢ x.agm y < max x y

Tactic:
·

Goal state after:
case inr
x y : ℝ≥0
hn : x ≠ y
this : ∀ {x y : ℝ≥0}, x ≠ y → x < y → x.agm y < max x y
h : ¬x < y
⊢ x.agm y < max x y
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = -2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x

pp: case convert_2.convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ -2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
·

Goal state after:
case e'_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x ↦ 1 - x ^ 2
u₁ : ℝ → ℝ := fun x ↦ f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x ↦ -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x ↦ sin (x * θ)
v₁' : ℝ → ℝ := fun x ↦ cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x ↦ x * f x ^ n
u₂' : ℝ → ℝ := fun x ↦ f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x ↦ cos (x * θ)
v₂' : ℝ → ℝ := fun x ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = -2 * (↑n + 1) * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ 0 ≤ binEntropy 0

pp: case inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ binEntropy p

Tactic:
·

Goal state after:
case inl
hp₀ : 0 ≤ 0
hp₁ : 0 ≤ 1
⊢ 0 ≤ binEntropy 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ binEntropy 1

pp: case inr.inr
p : ℝ
hp₀✝ : 0 ≤ p
hp₁✝ : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ binEntropy p

Tactic:
·

Goal state after:
case inr.inl
hp₀✝ : 0 ≤ 1
hp₁ : 1 ≤ 1
hp₀ : 0 < 1
⊢ 0 ≤ binEntropy 1
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case pos
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

pp: case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
·

Goal state after:
case pos
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
·

Goal state after:
case neg
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ}, p < 0 → ¬p < -1 → -1 < p → -p * log p ≤ 0
h : ¬-1 < p
⊢ -p * log p ≤ 0

pp: p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0

Tactic:
·

Goal state after:
case inr
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ}, p < 0 → ¬p < -1 → -1 < p → -p * log p ≤ 0
h : ¬-1 < p
⊢ -p * log p ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0

Tactic:
·

Goal state after:
p✝ p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inl
hp : 0 ≤ 0
⊢ binEntropy 0 ≤ 0

pp: case inr
p : ℝ
hp✝ : p ≤ 0
hp : p < 0
⊢ binEntropy p ≤ 0

Tactic:
·

Goal state after:
case inl
hp : 0 ≤ 0
⊢ binEntropy 0 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr
p : ℝ
hp✝ : p ≤ 0
hp : p < 0
⊢ binEntropy p ≤ 0

Tactic:
·

Goal state after:
case inr
p : ℝ
hp✝ : p ≤ 0
hp : p < 0
⊢ binEntropy p ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : p < 0
⊢ binEntropy p ≠ 0

pp: case inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
⊢ binEntropy p ≠ 0

Tactic:
·

Goal state after:
case inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : p < 0
⊢ binEntropy p ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr.inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : 1 < p
⊢ binEntropy p ≠ 0

pp: case inr.inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ binEntropy p ≠ 0

Tactic:
·

Goal state after:
case inr.inl
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : 1 < p
⊢ binEntropy p ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr.inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ binEntropy p ≠ 0

Tactic:
·

Goal state after:
case inr.inr
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ binEntropy p ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
p : ℝ
⊢ binEntropy p < log 2 → p ≠ 2⁻¹

case refine_2
p : ℝ
h : p ≠ 2⁻¹
⊢ binEntropy p < log 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_1
p : ℝ
⊢ binEntropy p < log 2 → p ≠ 2⁻¹

pp: case refine_2
p : ℝ
h : p ≠ 2⁻¹
⊢ binEntropy p < log 2

Tactic:
·

Goal state after:
case refine_1
p : ℝ
⊢ binEntropy p < log 2 → p ≠ 2⁻¹
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ binEntropy p < log 2

pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
⊢ binEntropy p < log 2

Tactic:
·

Goal state after:
case refine_2.inr
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ binEntropy p < log 2
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: case inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : |z.im| ≤ z.re
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

pp: case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

Tactic:
·

Goal state after:
case inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : |z.im| ≤ z.re
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

Tactic:
·

Goal state after:
case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inl
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : p ≤ 0
⊢ binEntropy p < log 2

pp: case inr
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
⊢ binEntropy p < log 2

Tactic:
·

Goal state after:
case inl
p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : p ≤ 0
⊢ binEntropy p < log 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inl
⊢ binEntropy 2⁻¹ ≤ log 2

pp: case inr
p : ℝ
hp : p ≠ 2⁻¹
⊢ binEntropy p ≤ log 2

Tactic:
·

Goal state after:
case inl
⊢ binEntropy 2⁻¹ ≤ log 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 2⁻¹
⊢ binEntropy p ≤ log 2

Tactic:
·

Goal state after:
case inr
p : ℝ
hp : p ≠ 2⁻¹
⊢ binEntropy p ≤ log 2
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ False

pp: case refine_2
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ False

Tactic:
·

Goal state after:
case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹) 0
⊢ False

pp: case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p) * log (1 - p)⁻¹) 0

Tactic:
·

Goal state after:
case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹) 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p) * log (1 - p)⁻¹) 0

Tactic:
·

Goal state after:
case refine_1
h : DifferentiableAt ℝ (fun p ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ DifferentiableAt ℝ (fun p ↦ (1 - p) * log (1 - p)⁻¹) 0