awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.CompareExp (goal)
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ l.EventuallyEq (β := ℂ) (fun (z : ℂ) ↦ z ^ a₂ * cexp ((↑b₁ : ℂ) * z) * cexp ((↑(b₂ - b₁) : ℂ) * z)) fun (z : ℂ) ↦
    z ^ a₂ * cexp ((↑b₂ : ℂ) * z)
have simp : l.EventuallyEq (β := ℂ) (fun (z : ℂ) ↦ z ^ a₂ * cexp ((↑b₂ : ℂ) * z)) fun (z : ℂ) ↦ z ^ a₂ * cexp ((↑b₂ : ℂ) * z)
Tactic: simp only [ofReal_sub, sub_mul, mul_assoc, ← exp_add, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (goal)
Goal:
z : ℂ
m : z ∈ slitPlane
⊢ AnalyticAt ℂ log z
have rw : ∀ᶠ (z : ℂ) in 𝓝 z, DifferentiableAt ℂ log z
Tactic: rw [analyticAt_iff_eventually_differentiableAt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (goal)
Goal:
z : ℂ
m : z ∈ slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 z, DifferentiableAt ℂ log z
have h : ∀ a ∈ slitPlane, DifferentiableAt ℂ log a
Tactic: filter_upwards [isOpen_slitPlane.eventually_mem m]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ (𝓝[insert x s] x).EventuallyEq (β := ℂ) (fun (z : E) ↦ f z ^ g z) fun (z : E) ↦ cexp (log (f z) * g z)
have h : ∀ (a : E), f a ≠ 0 → f a ^ g a = cexp (log (f a) * g a)
Tactic: filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) s x
have e : (𝓝[insert x s] x).EventuallyEq (β := ℂ) (fun (z : E) ↦ f z ^ g z) fun (z : E) ↦ cexp (log (f z) * g z)
Tactic: have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ exp (log (f z) * g z) := by
    filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]
    intro z fz
    simp only [fz, cpow_def, if_false]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (𝓝[insert x s] x).EventuallyEq (β := ℂ) (fun (z : E) ↦ f z ^ g z) fun (z : E) ↦ cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) s x
have apply : AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ cexp (log (f z) * g z)) s x
Tactic: apply AnalyticWithinAt.congr_of_eventuallyEq_insert _ e
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticAt ℂ f x
ga : AnalyticAt ℂ g x
m : f x ∈ slitPlane
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) x
have rw : ∀ (fa : AnalyticWithinAt ℂ f univ x) (ga : AnalyticWithinAt ℂ g univ x) (m : f x ∈ slitPlane),
  AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) univ x
Tactic: rw [← analyticWithinAt_univ] at fa ga ⊢
Cleared hypotheses: fa, ga, m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re
have h : ∀ (x : ℝ), Real.log x = (log (↑x : ℂ)).re
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (hypothesis)
Goal:
x : ℝ
hx : 0 < x
⊢ AnalyticAt ℝ Real.log x
have this : Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re
Tactic: have : Real.log = fun x : ℝ ↦ (Complex.log x).re := by ext x; exact (Complex.log_ofReal_re x).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (goal)
Goal:
x : ℝ
hx : 0 < x
this : Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re
⊢ AnalyticAt ℝ Real.log x
have rw : AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (log (↑x : ℂ)).re) x
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Analytic (goal)
Goal:
x : ℝ
hx : 0 < x
this : Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re
⊢ AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (log (↑x : ℂ)).re) x
have refine : (↑x : ℂ) ∈ slitPlane
Tactic: refine AnalyticAt.re_ofReal <| analyticAt_clog ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp (-z.arctan * I) - cexp (z.arctan * I)) * I / 2 / ((cexp (z.arctan * I) + cexp (-z.arctan * I)) / 2) = z
have rw : (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
Tactic: rw [div_div_eq_mul_div, div_mul_cancel₀ _ two_ne_zero, ← div_mul_eq_mul_div,
    -- multiply top and bottom by `exp (arctan z * I)`
    ← mul_div_mul_right _ _ (exp_ne_zero (arctan z * I)), sub_mul, add_mul,
    ← exp_add, neg_mul, neg_add_cancel, exp_zero, ← exp_add, ← two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ 1 + z * I ≠ 0
have contrapose : ∀ (h₁ : 1 + z * I = 0), z = I
Tactic: contrapose h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
h₂ : z ≠ -I
h₁ : 1 + z * I = 0
⊢ z = I
have h₃ : I = z
Tactic: rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have z₁ : 1 + z * I ≠ 0
Tactic: have z₁ : 1 + z * I ≠ 0 := by
    contrapose h₁
    rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁
    exact h₁.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
⊢ 1 - z * I ≠ 0
have contrapose : ∀ (h₂ : 1 - z * I = 0), z = -I
Tactic: contrapose h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : 1 - z * I = 0
⊢ z = -I
have h₃ : -I = z
Tactic: rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have z₂ : 1 - z * I ≠ 0
Tactic: have z₂ : 1 - z * I ≠ 0 := by
    contrapose h₂
    rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂
    exact h₂.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
have rw : (1 + z * I) / (1 - z * I) ≠ 0
Tactic: rw [arctan, ← mul_rotate, ← mul_assoc,
      show 2 * (I * (-I / 2)) = 1 by simp [field], one_mul, exp_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
Tactic: have key : exp (2 * (arctan z * I)) = (1 + z * I) / (1 - z * I) := by
    rw [arctan, ← mul_rotate, ← mul_assoc,
      show 2 * (I * (-I / 2)) = 1 by simp [field], one_mul, exp_log]
    · exact div_ne_zero z₁ z₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₂ : (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₂ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₃ : (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
      ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
    I =
  z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₂ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₃ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
        ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
      I =
    z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₄ : (1 * (1 - z * I) - (1 + z * I)) / (1 + z * I + 1 * (1 - z * I)) * I = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₂ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₃ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
        ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
      I =
    z
rw₄ : (1 * (1 - z * I) - (1 + z * I)) / (1 + z * I + 1 * (1 - z * I)) * I = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₅ : (1 - z * I - (1 + z * I)) / (1 + z * I + (1 - z * I)) * I = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₂ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₃ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
        ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
      I =
    z
rw₄ : (1 * (1 - z * I) - (1 + z * I)) / (1 + z * I + 1 * (1 - z * I)) * I = z
rw₅ : (1 - z * I - (1 + z * I)) / (1 + z * I + (1 - z * I)) * I = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₆ : -(I * I) * z = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₂ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₃ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
        ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
      I =
    z
rw₄ : (1 * (1 - z * I) - (1 + z * I)) / (1 + z * I + 1 * (1 - z * I)) * I = z
rw₅ : (1 - z * I - (1 + z * I)) / (1 + z * I + (1 - z * I)) * I = z
rw₆ : -(I * I) * z = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₇ : - -1 * z = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₂ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₃ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
        ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
      I =
    z
rw₄ : (1 * (1 - z * I) - (1 + z * I)) / (1 + z * I + 1 * (1 - z * I)) * I = z
rw₅ : (1 - z * I - (1 + z * I)) / (1 + z * I + (1 - z * I)) * I = z
rw₆ : -(I * I) * z = z
rw₇ : - -1 * z = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₈ : 1 * z = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)
rw : (1 - (1 + z * I) / (1 - z * I)) / ((1 + z * I) / (1 - z * I) + 1) * I = z
rw₁ : (1 - (1 + z * I) / (1 - z * I)) * (1 - z * I) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₂ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) / (((1 + z * I) / (1 - z * I) + 1) * (1 - z * I)) * I = z
rw₃ :
  (1 * (1 - z * I) - (1 + z * I) / (1 - z * I) * (1 - z * I)) /
        ((1 + z * I) / (1 - z * I) * (1 - z * I) + 1 * (1 - z * I)) *
      I =
    z
rw₄ : (1 * (1 - z * I) - (1 + z * I)) / (1 + z * I + 1 * (1 - z * I)) * I = z
rw₅ : (1 - z * I - (1 + z * I)) / (1 + z * I + (1 - z * I)) * I = z
rw₆ : -(I * I) * z = z
rw₇ : - -1 * z = z
rw₈ : 1 * z = z
⊢ (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
have rw₉ : z = z
Tactic: rw [key, ← mul_div_mul_right _ _ z₂, sub_mul, add_mul, div_mul_cancel₀ _ z₂, one_mul,
    show _ / _ * I = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
⊢ cos z ≠ 0
have refine : ∀ (k : ℤ), z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
Tactic: refine cos_ne_zero_iff.mpr (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
⊢ z ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2
have rw : ∀ (h₀ : ¬z.re = ((↑π : ℂ) / 2).re ∨ ¬z.im = ((↑π : ℂ) / 2).im) (h₁ : -(π / 2) < z.re) (h₂ : z.re ≤ π / 2) (k : ℤ),
  ¬z.re = ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2).re ∨
    ¬z.im = ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2).im
Tactic: rw [ne_eq, Complex.ext_iff, not_and_or] at h₀ ⊢
Cleared hypotheses: h₀, h₁, h₂, k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₀ : ¬z.re = ((↑π : ℂ) / 2).re ∨ ¬z.im = ((↑π : ℂ) / 2).im
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
⊢ ¬z.re = ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2).re ∨
    ¬z.im = ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2).im
have norm_cast : ∀ (h₀ : ¬z.re = π / 2 ∨ ¬z.im = 0), ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
Tactic: norm_cast at h₀ ⊢
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
h₀ : ¬z.re = π / 2 ∨ ¬z.im = 0
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
have inl : ∀ (nr : ¬z.re = π / 2), ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
Tactic: rcases h₀ with nr | ni
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
h₀ : ¬z.re = π / 2 ∨ ¬z.im = 0
inl : ∀ (nr : ¬z.re = π / 2), ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
have inr : ∀ (ni : ¬z.im = 0), ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
Tactic: rcases h₀ with nr | ni
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : ¬z.re = π / 2
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2 ∨ ¬z.im = 0
have inl : ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : ¬z.re = π / 2
⊢ ¬z.re = (↑(2 * k + 1) : ℝ) * π / 2
have inl : ∀ (nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2), z.re = π / 2
Tactic: contrapose nr
Cleared hypotheses: nr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ z.re = π / 2
have h₃ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
Tactic: rw [nr, mul_div_assoc, neg_eq_neg_one_mul, mul_lt_mul_iff_of_pos_right (by positivity)] at h₁
Cleared hypotheses: h₁, nr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
h₂ : z.re ≤ π / 2
k : ℤ
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ z.re = π / 2
have h₃ : LE.le (α := ℝ) (↑(2 * k + 1) : ℝ) 1
Tactic: rw [nr, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_of_pos_right (by positivity)] at h₂
Cleared hypotheses: h₂, h₁, nr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
k : ℤ
h₂ : LE.le (α := ℝ) (↑(2 * k + 1) : ℝ) 1
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
⊢ z.re = π / 2
have h₃ : Int.negSucc 0 < 2 * k + 1
Tactic: norm_cast at h₁ h₂
Cleared hypotheses: h₂, h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
k : ℤ
h₂ : LE.le (α := ℝ) (↑(2 * k + 1) : ℝ) 1
h₁ : LT.lt (α := ℝ) (-1) (↑(2 * k + 1) : ℝ)
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₃ : Int.negSucc 0 < 2 * k + 1
⊢ z.re = π / 2
have h₄ : 2 * k + 1 ≤ 1
Tactic: norm_cast at h₁ h₂
Cleared hypotheses: h₂, h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₁ : Int.negSucc 0 < 2 * k + 1
h₂ : 2 * k + 1 ≤ 1
⊢ z.re = π / 2
have h₃ : -1 < 2 * k + 1
Tactic: change -1 < _ at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
⊢ z.re = π / 2
have inl : ∀ (nr : z.re = (↑1 : ℝ) * π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
Tactic: rwa [show 2 * k + 1 = 1 by lia, Int.cast_one, one_mul] at nr
Cleared hypotheses: nr, h₂, h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
inl : ∀ (nr : z.re = (↑1 : ℝ) * π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
⊢ z.re = π / 2
have inl₁ : ∀ (nr : z.re = 1 * π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
Tactic: rwa [show 2 * k + 1 = 1 by lia, Int.cast_one, one_mul] at nr
Cleared hypotheses: nr, h₂, h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
k : ℤ
nr : z.re = (↑(2 * k + 1) : ℝ) * π / 2
h₂ : 2 * k + 1 ≤ 1
h₁ : -1 < 2 * k + 1
inl : ∀ (nr : z.re = (↑1 : ℝ) * π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
inl₁ : ∀ (nr : z.re = 1 * π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
⊢ z.re = π / 2
have inl₂ : ∀ (nr : z.re = π / 2) (h₂ : 2 * k + 1 ≤ 1) (h₁ : -1 < 2 * k + 1), z.re = π / 2
Tactic: rwa [show 2 * k + 1 = 1 by lia, Int.cast_one, one_mul] at nr
Cleared hypotheses: nr, h₂, h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (hypothesis)
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
⊢ (tan z).arctan = z
have h : cos z ≠ 0
Tactic: have h := cos_ne_zero_of_arctan_bounds h₀ h₁ h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ -I / 2 * log ((1 + sin z / cos z * I) / (1 - sin z / cos z * I)) = z
have rw : -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I)) = z
Tactic: rw [← mul_div_mul_right (1 + _) _ h, add_mul, sub_mul, one_mul, ← mul_rotate, mul_div_cancel₀ _ h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
| -I / 2 * log ((cos z + sin z * I) / (cos z - sin z * I))
have enter : cos z - sin z * I
Tactic: enter [2, 1, 2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Arctan (goal)
Goal:
z : ℂ
h₀ : z ≠ (↑π : ℂ) / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
| cos z - sin z * I
have rw : cos (-z) + sin (-z) * I
Tactic: rw [sub_eq_add_neg, ← neg_mul, ← sin_neg, ← cos_neg]