awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
linarith : x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) < x
have linarith₂ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
linarith : x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : x ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) < x
have linarith₆ : x ≤ -(π / 2) → 4 * (0 - x) + (2 * y - 1 * π) + 2 * (x - y) + (2 * x - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
linarith : x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : x ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : x ≤ -(π / 2) → 4 * (0 - x) + (2 * y - 1 * π) + 2 * (x - y) + (2 * x - -(1 * π)) = 0
⊢ -(π / 2) < x
have linarith₇ : x ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ tan π = 0
have rw : tan 0 = 0
Tactic: rw [tan_periodic.eq, tan_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : tan 0 = 0
⊢ tan π = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [tan_periodic.eq, tan_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
⊢ tan (π / 2 - x) = (tan x)⁻¹
have rw : sin (π / 2 - x) / cos (π / 2 - x) = (tan x)⁻¹
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : sin (π / 2 - x) / cos (π / 2 - x) = (tan x)⁻¹
⊢ tan (π / 2 - x) = (tan x)⁻¹
have rw₁ : sin (π / 2 - x) / cos (π / 2 - x) = (sin x / cos x)⁻¹
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : sin (π / 2 - x) / cos (π / 2 - x) = (tan x)⁻¹
rw₁ : sin (π / 2 - x) / cos (π / 2 - x) = (sin x / cos x)⁻¹
⊢ tan (π / 2 - x) = (tan x)⁻¹
have rw₂ : sin (π / 2 - x) / cos (π / 2 - x) = cos x / sin x
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : sin (π / 2 - x) / cos (π / 2 - x) = (tan x)⁻¹
rw₁ : sin (π / 2 - x) / cos (π / 2 - x) = (sin x / cos x)⁻¹
rw₂ : sin (π / 2 - x) / cos (π / 2 - x) = cos x / sin x
⊢ tan (π / 2 - x) = (tan x)⁻¹
have rw₃ : cos x / cos (π / 2 - x) = cos x / sin x
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : sin (π / 2 - x) / cos (π / 2 - x) = (tan x)⁻¹
rw₁ : sin (π / 2 - x) / cos (π / 2 - x) = (sin x / cos x)⁻¹
rw₂ : sin (π / 2 - x) / cos (π / 2 - x) = cos x / sin x
rw₃ : cos x / cos (π / 2 - x) = cos x / sin x
⊢ tan (π / 2 - x) = (tan x)⁻¹
have rw₄ : cos x / sin x = cos x / sin x
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Tendsto sin (𝓝[<] (π / 2)) (𝓝 1)
have h : 1 = sin (π / 2)
Tactic: convert! continuous_sin.continuousWithinAt.tendsto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝[>] 0)
have h1 : Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h1 : Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝[>] 0)
have h2 : ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Tendsto cos (𝓝[<] (π / 2)) (𝓝 0)
have h : 0 = cos (π / 2)
Tactic: convert! continuous_cos.continuousWithinAt.tendsto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] (π / 2), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
have h : ∀ (x : ℝ) (hx : x ∈ Ioo (-(π / 2)) (π / 2)), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
Tactic: filter_upwards [Ioo_mem_nhdsLT (neg_lt_self pi_div_two_pos)] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop
have h : tan = fun (x : ℝ) ↦ cos⁻¹ x * sin x
Tactic: convert!
    tendsto_cos_pi_div_two.inv_tendsto_nhdsGT_zero.atTop_mul_pos zero_lt_one
      tendsto_sin_pi_div_two using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (-1))
have h : -1 = sin (-(π / 2))
Tactic: convert! continuous_sin.continuousWithinAt.tendsto using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝[>] 0)
have h1 : Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
h1 : Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝[>] 0)
have h2 : ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝 0)
have h : 0 = cos (-(π / 2))
Tactic: convert! continuous_cos.continuousWithinAt.tendsto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] (-(π / 2)), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
have h : ∀ (x : ℝ) (hx : x ∈ Ioo (-(π / 2)) (π / 2)), Membership.mem (γ := Set ℝ) (Ioi 0) (cos x)
Tactic: filter_upwards [Ioo_mem_nhdsGT (neg_lt_self pi_div_two_pos)] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot
have h : tan = fun (x : ℝ) ↦ cos⁻¹ x * sin x
Tactic: convert!
    tendsto_cos_neg_pi_div_two.inv_tendsto_nhdsGT_zero.atTop_mul_neg (by simp)
      tendsto_sin_neg_pi_div_two using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1
have rw : sin z = 0 ↔ cos z * cos z = 1
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : sin z = 0 ↔ cos z * cos z = 1
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1
have rw₁ : sin z = 0 ↔ cos z * cos z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : sin z = 0 ↔ cos z * cos z = 1
rw₁ : sin z = 0 ↔ cos z * cos z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1
have rw₃ : sin z = 0 ↔ cos z * cos z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : sin z = 0 ↔ cos z * cos z = 1
rw₁ : sin z = 0 ↔ cos z * cos z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : sin z = 0 ↔ cos z * cos z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1
have rw₅ : sin z = 0 ↔ cos z * cos z = sin z * sin z + cos z * cos z
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : sin z = 0 ↔ cos z * cos z = 1
rw₁ : sin z = 0 ↔ cos z * cos z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : sin z = 0 ↔ cos z * cos z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
rw₅ : sin z = 0 ↔ cos z * cos z = sin z * sin z + cos z * cos z
rw₆ : ℂ
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1
have rw₇ : sin z = 0 ↔ sin z * sin z = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : sin z = 0 ↔ cos z * cos z = 1
rw₁ : sin z = 0 ↔ cos z * cos z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : sin z = 0 ↔ cos z * cos z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
rw₅ : sin z = 0 ↔ cos z * cos z = sin z * sin z + cos z * cos z
rw₆ : ℂ
rw₇ : sin z = 0 ↔ sin z * sin z = 0
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1
have rw₈ : sin z = 0 ↔ sin z = 0 ∨ sin z = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : sin z = 0 ↔ cos z * cos z = 1
rw₁ : sin z = 0 ↔ cos z * cos z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : sin z = 0 ↔ cos z * cos z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
rw₅ : sin z = 0 ↔ cos z * cos z = sin z * sin z + cos z * cos z
rw₆ : ℂ
rw₇ : sin z = 0 ↔ sin z * sin z = 0
rw₈ : sin z = 0 ↔ sin z = 0 ∨ sin z = 0
⊢ sin z = 0 ↔ cos z = 1 ∨ cos z = -1
have rw₉ : sin z = 0 ↔ sin z = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -1
have rw : cos z = 0 ↔ sin z * sin z = 1
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : cos z = 0 ↔ sin z * sin z = 1
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -1
have rw₁ : cos z = 0 ↔ sin z * sin z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : cos z = 0 ↔ sin z * sin z = 1
rw₁ : cos z = 0 ↔ sin z * sin z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -1
have rw₃ : cos z = 0 ↔ sin z * sin z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : cos z = 0 ↔ sin z * sin z = 1
rw₁ : cos z = 0 ↔ sin z * sin z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : cos z = 0 ↔ sin z * sin z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -1
have rw₅ : cos z = 0 ↔ sin z * sin z = sin z * sin z + cos z * cos z
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : cos z = 0 ↔ sin z * sin z = 1
rw₁ : cos z = 0 ↔ sin z * sin z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : cos z = 0 ↔ sin z * sin z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
rw₅ : cos z = 0 ↔ sin z * sin z = sin z * sin z + cos z * cos z
rw₆ : ℂ
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -1
have rw₇ : cos z = 0 ↔ cos z * cos z = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : cos z = 0 ↔ sin z * sin z = 1
rw₁ : cos z = 0 ↔ sin z * sin z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : cos z = 0 ↔ sin z * sin z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
rw₅ : cos z = 0 ↔ sin z * sin z = sin z * sin z + cos z * cos z
rw₆ : ℂ
rw₇ : cos z = 0 ↔ cos z * cos z = 0
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -1
have rw₈ : cos z = 0 ↔ cos z = 0 ∨ cos z = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
z : ℂ
rw : cos z = 0 ↔ sin z * sin z = 1
rw₁ : cos z = 0 ↔ sin z * sin z = HPow.hPow (β := ℕ) (sin z) 2 + HPow.hPow (β := ℕ) (cos z) 2
rw₂ : ℂ
rw₃ : cos z = 0 ↔ sin z * sin z = sin z * sin z + HPow.hPow (β := ℕ) (cos z) 2
rw₄ : ℂ
rw₅ : cos z = 0 ↔ sin z * sin z = sin z * sin z + cos z * cos z
rw₆ : ℂ
rw₇ : cos z = 0 ↔ cos z * cos z = 0
rw₈ : cos z = 0 ↔ cos z = 0 ∨ cos z = 0
⊢ cos z = 0 ↔ sin z = 1 ∨ sin z = -1
have rw₉ : cos z = 0 ↔ cos z = 0
Tactic: rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, left_eq_add, mul_eq_zero, or_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos ((↑π : ℂ) / 2) = (↑(Real.cos (π / 2)) : ℂ)
have rw : cos ((↑π : ℂ) / 2) = cos (↑(π / 2) : ℂ)
Tactic: rw [ofReal_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin ((↑π : ℂ) / 2) = (↑(Real.sin (π / 2)) : ℂ)
have rw : sin ((↑π : ℂ) / 2) = sin (↑(π / 2) : ℂ)
Tactic: rw [ofReal_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin (↑π : ℂ) = 0
have rw : (↑0 : ℂ) = 0
Tactic: rw [← ofReal_sin, Real.sin_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (↑π : ℂ) = -1
have rw : (↑(-1) : ℂ) = -1
Tactic: rw [← ofReal_cos, Real.cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℂ
⊢ cos ((↑π : ℂ) / 2 - x) = sin x
have rw : cos (-((↑π : ℂ) / 2 - x)) = sin x
Tactic: rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℂ
rw : cos (-((↑π : ℂ) / 2 - x)) = sin x
⊢ cos ((↑π : ℂ) / 2 - x) = sin x
have rw₁ : cos (x - (↑π : ℂ) / 2) = sin x
Tactic: rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℂ
rw : cos (-((↑π : ℂ) / 2 - x)) = sin x
rw₁ : cos (x - (↑π : ℂ) / 2) = sin x
⊢ cos ((↑π : ℂ) / 2 - x) = sin x
have rw₂ : sin x = sin x
Tactic: rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℂ
⊢ tan ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
have rw : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℂ
rw : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
⊢ tan ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
have rw₁ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (sin x / cos x)⁻¹
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℂ
rw : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
rw₁ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (sin x / cos x)⁻¹
⊢ tan ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
have rw₂ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = cos x / sin x
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℂ
rw : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
rw₁ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (sin x / cos x)⁻¹
rw₂ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = cos x / sin x
⊢ tan ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
have rw₃ : cos x / cos ((↑π : ℂ) / 2 - x) = cos x / sin x
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℂ
rw : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
rw₁ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (sin x / cos x)⁻¹
rw₂ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = cos x / sin x
rw₃ : cos x / cos ((↑π : ℂ) / 2 - x) = cos x / sin x
⊢ tan ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
have rw₄ : cos x / sin x = cos x / sin x
Tactic: rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cexp ((↑π : ℂ) / 2 * I) = I
have rw : cos ((↑π : ℂ) / 2) + sin ((↑π : ℂ) / 2) * I = I
Tactic: rw [← cos_add_sin_I, cos_pi_div_two, sin_pi_div_two, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos ((↑π : ℂ) / 2) + sin ((↑π : ℂ) / 2) * I = I
⊢ cexp ((↑π : ℂ) / 2 * I) = I
have rw₁ : 0 + sin ((↑π : ℂ) / 2) * I = I
Tactic: rw [← cos_add_sin_I, cos_pi_div_two, sin_pi_div_two, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos ((↑π : ℂ) / 2) + sin ((↑π : ℂ) / 2) * I = I
rw₁ : 0 + sin ((↑π : ℂ) / 2) * I = I
⊢ cexp ((↑π : ℂ) / 2 * I) = I
have rw₂ : 0 + 1 * I = I
Tactic: rw [← cos_add_sin_I, cos_pi_div_two, sin_pi_div_two, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos ((↑π : ℂ) / 2) + sin ((↑π : ℂ) / 2) * I = I
rw₁ : 0 + sin ((↑π : ℂ) / 2) * I = I
rw₂ : 0 + 1 * I = I
⊢ cexp ((↑π : ℂ) / 2 * I) = I
have rw₃ : 0 + I = I
Tactic: rw [← cos_add_sin_I, cos_pi_div_two, sin_pi_div_two, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos ((↑π : ℂ) / 2) + sin ((↑π : ℂ) / 2) * I = I
rw₁ : 0 + sin ((↑π : ℂ) / 2) * I = I
rw₂ : 0 + 1 * I = I
rw₃ : 0 + I = I
⊢ cexp ((↑π : ℂ) / 2 * I) = I
have rw₄ : I = I
Tactic: rw [← cos_add_sin_I, cos_pi_div_two, sin_pi_div_two, one_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw₂ : cos ((↑π : ℂ) / 2) + sin (-((↑π : ℂ) / 2)) * I = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₂ : cos ((↑π : ℂ) / 2) + sin (-((↑π : ℂ) / 2)) * I = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw₃ : 0 + sin (-((↑π : ℂ) / 2)) * I = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₂ : cos ((↑π : ℂ) / 2) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₃ : 0 + sin (-((↑π : ℂ) / 2)) * I = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw₄ : 0 + -sin ((↑π : ℂ) / 2) * I = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₂ : cos ((↑π : ℂ) / 2) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₃ : 0 + sin (-((↑π : ℂ) / 2)) * I = -I
rw₄ : 0 + -sin ((↑π : ℂ) / 2) * I = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw₅ : 0 + -1 * I = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₂ : cos ((↑π : ℂ) / 2) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₃ : 0 + sin (-((↑π : ℂ) / 2)) * I = -I
rw₄ : 0 + -sin ((↑π : ℂ) / 2) * I = -I
rw₅ : 0 + -1 * I = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw₆ : -1 * I = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₂ : cos ((↑π : ℂ) / 2) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₃ : 0 + sin (-((↑π : ℂ) / 2)) * I = -I
rw₄ : 0 + -sin ((↑π : ℂ) / 2) * I = -I
rw₅ : 0 + -1 * I = -I
rw₆ : -1 * I = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw₇ : -(1 * I) = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₂ : cos ((↑π : ℂ) / 2) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₃ : 0 + sin (-((↑π : ℂ) / 2)) * I = -I
rw₄ : 0 + -sin ((↑π : ℂ) / 2) * I = -I
rw₅ : 0 + -1 * I = -I
rw₆ : -1 * I = -I
rw₇ : -(1 * I) = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I
have rw₈ : -I = -I
Tactic: rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ ‖cexp ((↑a : ℂ) * (cexp z + cexp (-z)))‖ ≤ rexp (a * Real.cos b * rexp |z.re|)
have simp : a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)
Tactic: simp only [norm_exp, Real.exp_le_exp, re_ofReal_mul, add_re, exp_re, neg_im, Real.cos_neg, ←
    add_mul, mul_assoc, mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]