awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, sin x * HPow.hPow (β := ℕ) (cos x) 2 =
    (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x * HPow.hPow (β := ℕ) (cos x) 2 =
    (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, sin x * HPow.hPow (β := ℕ) (cos x) 2 =
    (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x * HPow.hPow (β := ℕ) (cos x) 2 =
    (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3

Tactic:
exact this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (HMul.hMul (α := ℕ) 2 1 + 1) * HPow.hPow (β := ℕ) (cos x) 0)
    (∫ (u : ℝ) in cos b..cos a, HPow.hPow (β := ℕ) u 0 * HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) u 2) 1)

Tactic:
have := @integral_sin_pow_odd_mul_cos_pow a b 1 0
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (HMul.hMul (α := ℕ) 2 1 + 1) * HPow.hPow (β := ℕ) (cos x) 0)
    (∫ (u : ℝ) in cos b..cos a, HPow.hPow (β := ℕ) u 0 * HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) u 2) 1)
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 3 =
    cos a - cos b - (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3

Tactic:
norm_num at this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 3 =
    cos a - cos b - (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 3 =
    cos a - cos b - (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 3 =
    cos a - cos b - (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 3 =
    cos a - cos b - (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3

Tactic:
exact this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
simp :
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, (HSub.hSub (α := ℝ) 1 2⁻¹ - cos (2 * x) / 2) ^ m * (2⁻¹ + cos (2 * x) / 2) ^ n)
    (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (2 * m) * cos x ^ (2 * n))
    (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)

Tactic:
simp [pow_mul, sin_sq, cos_sq, ← sub_sub]

Premises used: Real.sin_sq, pow_mul, sub_sub, Real.cos_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
field_simp :
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, ((HSub.hSub (α := ℝ) 2 1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
    (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (HSub.hSub (α := ℝ) 1 2⁻¹ - cos (2 * x) / 2) ^ m * (2⁻¹ + cos (2 * x) / 2) ^ n)
    (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, ((HSub.hSub (α := ℝ) 2 1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
    (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ HMul.hMul (α := ℕ) 2 1 * cos x ^ HMul.hMul (α := ℕ) 2 1)
    (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1)

Tactic:
integral_sin_pow_even_mul_cos_pow_even 1 1

Premises used: integral_sin_pow_even_mul_cos_pow_even, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h :
  (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * HPow.hPow (β := ℕ) (cos x) 2 =
    (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32

Tactic:
convert! integral_sin_pow_even_mul_cos_pow_even 1 1 using 1

Premises used: integral_sin_pow_even_mul_cos_pow_even, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
⊢ (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4

Tactic:
have h1 : ∀ c : ℝ, (↑1 - c) / ↑2 * ((↑1 + c) / ↑2) = (↑1 - c ^ 2) / 4 := fun c => by ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2

Tactic:
have h2 : Continuous fun x => cos (2 * x) ^ 2 := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
x : ℝ
rw : cos x * sin x = 2 * sin x * cos x / 2
⊢ cos x * sin x = sin (2 * x) / 2

Tactic:
rw [sin_two_mul]

Premises used: Real.sin_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
x : ℝ
⊢ cos x * sin x = 2 * sin x * cos x / 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
⊢ ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2

Tactic:
have h3 : ∀ x, cos x * sin x = sin (2 * x) / 2 := by intro; rw [sin_two_mul]; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
d : ℝ
⊢ 2 * (2 * d) = 4 * d

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
⊢ ∀ (d : ℝ), 2 * (2 * d) = 4 * d

Tactic:
have h4 : ∀ d : ℝ, 2 * (2 * d) = 4 * d := fun d => by ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
h :
  (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    (b - a - 2⁻¹ * ((sin (4 * b) / 2 - sin (4 * a) / 2 + 2 * b - 2 * a) / 2)) / 4
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1

Tactic:
simp [h1, h2.intervalIntegrable, integral_comp_mul_left fun x => cos x ^ 2, h3, h4]

Premises used: intervalIntegral.integral_comp_mul_left, Real.cos, Continuous.intervalIntegrable, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    (b - a - 2⁻¹ * ((sin (4 * b) / 2 - sin (4 * a) / 2 + 2 * b - 2 * a) / 2)) / 4

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2))
    (∫ (x : ℝ) in -sin (π / 2)..sin (π / 2), √(1 - HPow.hPow (β := ℕ) x 2))
rw₁ rw₂ :
  Eq (α := ℝ) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2)) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2))
    (∫ (x : ℝ) in sin (-(π / 2))..sin (π / 2), √(1 - HPow.hPow (β := ℕ) x 2))

Tactic:
rw [sin_neg, sin_pi_div_two]

Premises used: Real.sin_pi_div_two, Real.sin_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -(π / 2)..π / 2, √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x)
    (∫ (x : ℝ) in -(π / 2)..π / 2, HPow.hPow (β := ℕ) (cos x) 2)

Tactic:
integral_congr_ae (MeasureTheory.ae_of_all _ fun _ h => ?_)

Premises used: MeasureTheory.ae_of_all, intervalIntegral.integral_congr_ae
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
refine :
  ∀ (x : ℝ) (h : x ∈ Ι (-(π / 2)) (π / 2)), √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x = HPow.hPow (β := ℕ) (cos x) 2
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -(π / 2)..π / 2, √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x)
    (∫ (x : ℝ) in -(π / 2)..π / 2, HPow.hPow (β := ℕ) (cos x) 2)

Tactic:
refine integral_congr_ae (MeasureTheory.ae_of_all _ fun _ h => ?_)

Premises used: MeasureTheory.ae_of_all, intervalIntegral.integral_congr_ae
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
x : ℝ
h : x ∈ Ι (-(π / 2)) (π / 2)
⊢ -(π / 2) < x ∧ x ≤ π / 2

Tactic:
rw [uIoc_of_le (neg_le_self (le_of_lt (half_pos Real.pi_pos))), Set.mem_Ioc] at h

Premises used: half_pos, le_of_lt, Real.pi_pos, neg_le_self, Set.mem_Ioc, Set.uIoc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
x : ℝ
h : -(π / 2) < x ∧ x ≤ π / 2
rw : cos x * cos x = HPow.hPow (β := ℕ) (cos x) 2
rw₁ rw₂ : cos x * cos x = cos x * cos x
⊢ √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x = HPow.hPow (β := ℕ) (cos x) 2

Tactic:
rw [← Real.cos_eq_sqrt_one_sub_sin_sq (le_of_lt h.1) h.2, pow_two]

Premises used: pow_two, le_of_lt, And.right, And.left, Real.cos_eq_sqrt_one_sub_sin_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
⊢ ∫ (x : ℝ) in -(π / 2)..π / 2, HPow.hPow (β := ℕ) (cos x) 2 = π / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin x)) MeasureTheory.volume 0 (π / 2)

Tactic:
apply intervalIntegrable_log_sin

Premises used: intervalIntegrable_log_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin x)) MeasureTheory.volume (π / 2) π

Tactic:
apply intervalIntegrable_log_sin

Premises used: intervalIntegrable_log_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin x)) =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))
⊢ ∫ (x : ℝ) in 0..π, log (sin x) = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))

Tactic:
rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)
    (by apply intervalIntegrable_log_sin) (by apply intervalIntegrable_log_sin)]

Premises used: intervalIntegral.integral_add_adjacent_intervals
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
left : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin x))
| HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin x)) =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
right : ∫ (x : ℝ) in π / 2..π, log (sin x)
| HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin x))

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
arg : fun (x : ℝ) ↦ log (sin x)
| ∫ (x : ℝ) in π / 2..π, log (sin x)

Tactic:
arg 1
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
x : ℝ
h : log (sin (π - x))
| log (sin x)

Tactic:
rw [← sin_pi_sub]

Premises used: Real.sin_pi_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
h : ∀ (x : ℝ), log (sin (π - x))
| HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin x)) =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))

Tactic:
left; right; arg 1
    intro x
    rw [← sin_pi_sub]

Premises used: Real.sin_pi_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
conv :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin (π - x))) =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin x)) =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))

Tactic:
conv =>
    left; right; arg 1
    intro x
    rw [← sin_pi_sub]

Premises used: Real.sin_pi_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₃ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π - π / 2 < π / 2 → 2 * π - 1 * π - 1 * π = 0
linarith₆ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₇ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₉ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₀ : π / 2 < π - π / 2 → GT.gt (α := ℝ) 2 0
linarith₁₁ : π / 2 < π - π / 2 → 1 * π - (2 * π - 1 * π) = 0
⊢ π - π / 2 = π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in 0..π / 2, log (sin x)) =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin (π - x))) =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))

Tactic:
rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)), sub_self,
    (by linarith : π - π / 2 = π / 2)]

Premises used: intervalIntegral.integral_comp_sub_left, sub_self, Real.log, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in 0..π / 2, log (sin x)) =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))

Tactic:
ring!
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
hf :
  (codiscreteWithin (Ι 0 (π / 2))).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log (sin x)) fun (x : ℝ) ↦
    log (sin (2 * x)) - log 2 - log (cos x)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x))

Tactic:
apply intervalIntegral.integral_congr_codiscreteWithin

Premises used: intervalIntegral.integral_congr_codiscreteWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ ⦃a : ℝ⦄, a ∈ Ι 0 (π / 2) → Membership.mem (γ := Set ℝ) Set.univ a
⊢ Ι 0 (π / 2) ⊆ Set.univ

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
hf :
  Membership.mem (γ := Filter ℝ) (codiscreteWithin Set.univ)
    {x : ℝ |
      (fun (x : ℝ) ↦
          Eq (α := ℝ) ((fun (x : ℝ) ↦ log (sin x)) x) ((fun (x : ℝ) ↦ log (sin (2 * x)) - log 2 - log (cos x)) x))
        x}
⊢ (codiscreteWithin (Ι 0 (π / 2))).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log (sin x)) fun (x : ℝ) ↦
    log (sin (2 * x)) - log 2 - log (cos x)

Tactic:
apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)

Premises used: Filter.codiscreteWithin_mono
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
apply : sin (π / 2) ≠ 0
⊢ sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ

Tactic:
apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)

Premises used: Real.analyticOnNhd_sin, AnalyticOnNhd.preimage_zero_mem_codiscrete
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ sin (π / 2) ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ

Tactic:
have t₀ : sin ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
        simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
apply : cos 0 ≠ 0
⊢ cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ

Tactic:
apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)

Premises used: AnalyticOnNhd.preimage_zero_mem_codiscrete, Real.analyticOnNhd_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ cos 0 ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ

Tactic:
have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
h : ∀ (y : ℝ) (h₁y : y ∈ sin ⁻¹' {0}ᶜ) (h₂y : y ∈ cos ⁻¹' {0}ᶜ), log (sin y) = log (sin (2 * y)) - log 2 - log (cos y)
⊢ Membership.mem (γ := Filter ℝ) (codiscreteWithin Set.univ)
    {x : ℝ |
      (fun (x : ℝ) ↦
          Eq (α := ℝ) ((fun (x : ℝ) ↦ log (sin x)) x) ((fun (x : ℝ) ↦ log (sin (2 * x)) - log 2 - log (cos x)) x))
        x}

Tactic:
filter_upwards [t₀, t₁] with y h₁y h₂y
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
y : ℝ
h₁y : y ∈ sin ⁻¹' {0}ᶜ
h₂y : y ∈ cos ⁻¹' {0}ᶜ
h :
  ∀ (t₀ : (sin ⁻¹' {0})ᶜ ∈ codiscrete ℝ) (t₁ : (cos ⁻¹' {0})ᶜ ∈ codiscrete ℝ) (h₁y : ¬sin y = 0) (h₂y : ¬cos y = 0),
    log (sin y) = log 2 + log (sin y) + log (cos y) - log 2 - log (cos y)
⊢ log (sin y) = log (sin (2 * y)) - log 2 - log (cos y)

Tactic:
simp_all only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        sin_two_mul, ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, or_self, not_false_eq_true, log_mul]

Premises used: OfNat.ofNat_ne_zero, Real.sin_two_mul, mul_eq_zero, ne_eq, Set.mem_singleton_iff, or_self, Set.preimage_compl, not_false_eq_true, Real.log_mul, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
y : ℝ
t₀ : (sin ⁻¹' {0})ᶜ ∈ codiscrete ℝ
t₁ : (cos ⁻¹' {0})ᶜ ∈ codiscrete ℝ
h₁y : ¬sin y = 0
h₂y : ¬cos y = 0
⊢ log (sin y) = log 2 + log (sin y) + log (cos y) - log 2 - log (cos y)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
rw :
  (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - (π / 2 - 0) • log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x)
rw₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x))) MeasureTheory.volume 0 (π / 2)
rw₂ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)
rw₃ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (cos x)) MeasureTheory.volume 0 (π / 2)
⊢ ∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x)

Tactic:
rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]

Premises used: intervalIntegral.integral_sub, intervalIntegrable_const, intervalIntegral.integral_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - (π / 2 - 0) • log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x))) MeasureTheory.volume 0 (π / 2)

Tactic:
simpa using (intervalIntegrable_log_sin (a := 0) (b := π)).comp_mul_left

Premises used: IntervalIntegrable.comp_mul_left, intervalIntegrable_log_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
apply : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x))) MeasureTheory.volume 0 (π / 2)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)

Tactic:
apply IntervalIntegrable.sub _ intervalIntegrable_const

Premises used: IntervalIntegrable.sub, intervalIntegrable_const
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (cos x)) MeasureTheory.volume 0 (π / 2)

Tactic:
intervalIntegrable_log_cos

Premises used: Real.log, dite, intervalIntegrable_log_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (cos x)) MeasureTheory.volume 0 (π / 2)

Tactic:
exact intervalIntegrable_log_cos

Premises used: intervalIntegrable_log_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
⊢ (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (sin x)

Tactic:
simp [← sin_pi_div_two_sub,
        intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]

Premises used: Real.pi, intervalIntegral.integral_comp_sub_left, Real.sin_pi_div_two_sub, HDiv.hDiv, Real.log, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
linarith : 2 * (π / 2) < π → 2 / 2 = 1
linarith₁ linarith₂ : 2 * (π / 2) < π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 2 * (π / 2) < π → GT.gt (α := ℝ) 2 0
linarith₄ : 2 * (π / 2) < π → HMul.hMul (α := ℝ) 1 2 * (1 * π) - 2 * π = 0
linarith₅ : π < 2 * (π / 2) → 2 / 2 = 1
linarith₆ linarith₇ : π < 2 * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π < 2 * (π / 2) → GT.gt (α := ℝ) 2 0
linarith₉ : π < 2 * (π / 2) → 2 * π - HMul.hMul (α := ℝ) 1 2 * (1 * π) = 0
⊢ 2 * (π / 2) = π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric
Goal:
simp : -(π / 2 * log 2) = -(log 2 * π) / 2
⊢ (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (sin x) = -log 2 * π / 2

Tactic:
simp only [intervalIntegral.integral_comp_mul_left (f := fun x ↦ log (sin x)) two_ne_zero,
        mul_zero, (by linarith : 2 * (π / 2) = π),
        integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two, smul_eq_mul, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_mul_cancel_left₀, sub_sub_cancel_left, neg_mul]

Premises used: intervalIntegral.integral_comp_mul_left, OfNat.ofNat_ne_zero, inv_mul_cancel_left₀, sub_sub_cancel_left, ne_eq, Real.log, MulZeroClass.mul_zero, two_ne_zero, _private.0.integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two, neg_mul, smul_eq_mul, not_false_eq_true, Real.sin