awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ ∫ (x : ℝ) in 0..π, log (sin x) = HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in 0..π / 2, log (sin x))
have 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))
Tactic: rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)
    (by apply intervalIntegrable_log_sin) (by apply intervalIntegrable_log_sin)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
| 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))
have left : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin x))
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
| HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in π / 2..π, log (sin x))
have right : ∫ (x : ℝ) in π / 2..π, log (sin x)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
| ∫ (x : ℝ) in π / 2..π, log (sin x)
have arg : fun (x : ℝ) ↦ log (sin x)
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
x : ℝ
| log (sin x)
have h : log (sin (π - x))
Tactic: rw [← sin_pi_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
| 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))
have h : ∀ (x : ℝ), log (sin (π - x))
Tactic: left; right; arg 1
    intro x
    rw [← sin_pi_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ 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))
have 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))
Tactic: conv =>
    left; right; arg 1
    intro x
    rw [← sin_pi_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ π - π / 2 = π / 2
have linarith : π - π / 2 < π / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
⊢ π - π / 2 = π / 2
have linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ π - π / 2 = π / 2
have linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ π - π / 2 = π / 2
have linarith₅ : π - π / 2 < π / 2 → 2 * π - 1 * π - 1 * π = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ π - π / 2 = π / 2
have linarith₆ : π / 2 < π - π / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ π - π / 2 = π / 2
have linarith₇ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ π - π / 2 = π / 2
have linarith₁₀ : π / 2 < π - π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ π - π / 2 = π / 2
have linarith₁₁ : π / 2 < π - π / 2 → 1 * π - (2 * π - 1 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ 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))
have 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))
Tactic: rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)), sub_self,
    (by linarith : π - π / 2 = π / 2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, log (sin x)) (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x)) - log 2 - log (cos x))
have hf : (codiscreteWithin (Ι 0 (π / 2))).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log (sin x)) fun (x : ℝ) ↦
  log (sin (2 * x)) - log 2 - log (cos x)
Tactic: apply intervalIntegral.integral_congr_codiscreteWithin
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ Ι 0 (π / 2) ⊆ Set.univ
have tauto : ∀ ⦃a : ℝ⦄, a ∈ Ι 0 (π / 2) → Membership.mem (γ := Set ℝ) Set.univ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ (codiscreteWithin (Ι 0 (π / 2))).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ log (sin x)) fun (x : ℝ) ↦
    log (sin (2 * x)) - log 2 - log (cos x)
have 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}
Tactic: apply Filter.codiscreteWithin_mono (by tauto : Ι 0 (π / 2) ⊆ Set.univ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
have apply : sin (π / 2) ≠ 0
Tactic: apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (hypothesis)
Goal:
⊢ 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}
have t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
Tactic: have t₀ : sin ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_sin.preimage_zero_mem_codiscrete (x := π / 2)
        simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
have apply : cos 0 ≠ 0
Tactic: apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (hypothesis)
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ 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}
have t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
Tactic: have t₁ : cos ⁻¹' {0}ᶜ ∈ Filter.codiscrete ℝ := by
        apply analyticOnNhd_cos.preimage_zero_mem_codiscrete (x := 0)
        simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
⊢ 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}
have h : ∀ (y : ℝ) (h₁y : y ∈ sin ⁻¹' {0}ᶜ) (h₂y : y ∈ cos ⁻¹' {0}ᶜ), log (sin y) = log (sin (2 * y)) - log 2 - log (cos y)
Tactic: filter_upwards [t₀, t₁] with y h₁y h₂y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
y : ℝ
h₁y : y ∈ sin ⁻¹' {0}ᶜ
h₂y : y ∈ cos ⁻¹' {0}ᶜ
⊢ log (sin y) = log (sin (2 * y)) - log 2 - log (cos y)
have 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)
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]
Cleared hypotheses: t₀, t₁, h₁y, h₂y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ ∫ (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)
have 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)
Tactic: rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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)
⊢ ∫ (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)
have rw₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x))) MeasureTheory.volume 0 (π / 2)
Tactic: rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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)
⊢ ∫ (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)
have rw₂ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)
Tactic: rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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)
⊢ ∫ (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)
have rw₃ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (cos x)) MeasureTheory.volume 0 (π / 2)
Tactic: rw [intervalIntegral.integral_sub _ _,
        intervalIntegral.integral_sub _ intervalIntegrable_const,
        intervalIntegral.integral_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x)) - log 2) MeasureTheory.volume 0 (π / 2)
have apply : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log (sin (2 * x))) MeasureTheory.volume 0 (π / 2)
Tactic: apply IntervalIntegrable.sub _ intervalIntegrable_const
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ 2 * (π / 2) = π
have linarith : 2 * (π / 2) < π → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : 2 * (π / 2) < π → 2 / 2 = 1
⊢ 2 * (π / 2) = π
have linarith₁ : 2 * (π / 2) < π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : 2 * (π / 2) < π → 2 / 2 = 1
linarith₁ linarith₂ : 2 * (π / 2) < π → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 2 * (π / 2) = π
have linarith₃ : 2 * (π / 2) < π → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : 2 * (π / 2) < π → 2 / 2 = 1
linarith₁ linarith₂ : 2 * (π / 2) < π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 2 * (π / 2) < π → GT.gt (α := ℝ) 2 0
⊢ 2 * (π / 2) = π
have linarith₄ : 2 * (π / 2) < π → HMul.hMul (α := ℝ) 1 2 * (1 * π) - 2 * π = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ 2 * (π / 2) = π
have linarith₅ : π < 2 * (π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ 2 * (π / 2) = π
have linarith₆ : π < 2 * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ 2 * (π / 2) = π
have linarith₈ : π < 2 * (π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
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
⊢ 2 * (π / 2) = π
have linarith₉ : π < 2 * (π / 2) → 2 * π - HMul.hMul (α := ℝ) 1 2 * (1 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (sin x) = -log 2 * π / 2
have simp : -(π / 2 * log 2) = -(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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₅ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₆ : -(π / 2 * log 2) < -(log 2 * π) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₅ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : -(π / 2 * log 2) < -(log 2 * π) / 2 → GT.gt (α := ℝ) 2 0
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₇ : -(π / 2 * log 2) < -(log 2 * π) / 2 → -(1 * π * (1 * log 2)) - -(1 * log 2 * (1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₅ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : -(π / 2 * log 2) < -(log 2 * π) / 2 → GT.gt (α := ℝ) 2 0
linarith₇ : -(π / 2 * log 2) < -(log 2 * π) / 2 → -(1 * π * (1 * log 2)) - -(1 * log 2 * (1 * π)) = 0
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₈ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₅ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : -(π / 2 * log 2) < -(log 2 * π) / 2 → GT.gt (α := ℝ) 2 0
linarith₇ : -(π / 2 * log 2) < -(log 2 * π) / 2 → -(1 * π * (1 * log 2)) - -(1 * log 2 * (1 * π)) = 0
linarith₈ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 1 = 1
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₉ : -(log 2 * π) / 2 < -(π / 2 * log 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric (goal)
Goal:
linarith : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₁ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₄ : -(π / 2 * log 2) < -(log 2 * π) / 2 → 2 / 2 = 1
linarith₅ : -(π / 2 * log 2) < -(log 2 * π) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : -(π / 2 * log 2) < -(log 2 * π) / 2 → GT.gt (α := ℝ) 2 0
linarith₇ : -(π / 2 * log 2) < -(log 2 * π) / 2 → -(1 * π * (1 * log 2)) - -(1 * log 2 * (1 * π)) = 0
linarith₈ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₉ : -(log 2 * π) / 2 < -(π / 2 * log 2) → 2 / 2 = 1
⊢ -(π / 2 * log 2) = -(log 2 * π) / 2
have linarith₁₀ : -(log 2 * π) / 2 < -(π / 2 * log 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith