awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0)
have h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * HPow.hPow (β := ℝ) x 1) (𝓝[>] 0) (𝓝 0)
Tactic: have h := tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * HPow.hPow (β := ℝ) x 1) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0)
have h₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
Tactic: simp only [Real.rpow_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
have simp : ∀ x < 0, -(log x * |x|) = log x * x
Tactic: simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0)
have h_eq : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
Tactic: have h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ (fun x ↦ |x|)) x = log x * x := by
    simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]
    intro x hx
    simp only [abs_of_nonpos hx.le, mul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[<] 0) (𝓝 0)
have refine : Tendsto (α := ℝ) (β := ℝ) (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) (𝓝[<] 0) (𝓝 0)
Tactic: refine tendsto_nhdsWithin_congr h_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
⊢ Tendsto (α := ℝ) (β := ℝ) (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) (𝓝[<] 0) (𝓝 0)
have nth_rewrite : Tendsto (α := ℝ) (β := ℝ) (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) (𝓝[<] 0) (𝓝 (-0))
Tactic: nth_rewrite 3 [← neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (goal)
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
⊢ LE.le (α := Filter ℝ) (𝓝[<] 0) (𝓝[≠] 0)
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Iio 0) x), Membership.mem (γ := Set ℝ) {0}ᶜ x
Tactic: refine nhdsWithin_mono 0 (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (hypothesis)
Goal:
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Iio 0) x → (-(fun (x : ℝ) ↦ log x * x) ∘ fun (x : ℝ) ↦ |x|) x = log x * x
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Iio 0) x
⊢ Membership.mem (γ := Set ℝ) {0}ᶜ x
have hx₁ : x < 0
Tactic: push _ ∈ _ at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
have pos : x = 0 → y = 0 → (Eq (α := ℂ) 1 0 ↔ x = 0 ∧ y ≠ 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
pos : x = 0 → y = 0 → (Eq (α := ℂ) 1 0 ↔ x = 0 ∧ y ≠ 0)
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
have neg : x = 0 → ¬y = 0 → (Eq (α := ℂ) 0 0 ↔ x = 0 ∧ y ≠ 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
pos : x = 0 → y = 0 → (Eq (α := ℂ) 1 0 ↔ x = 0 ∧ y ≠ 0)
neg : x = 0 → ¬y = 0 → (Eq (α := ℂ) 0 0 ↔ x = 0 ∧ y ≠ 0)
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0
have neg₁ : ¬x = 0 → (cexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
⊢ x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0
have rw : ¬x ^ y = 0 ↔ x ≠ 0 ∨ y = 0
Tactic: rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
rw : ¬x ^ y = 0 ↔ x ≠ 0 ∨ y = 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0
have rw₁ : ¬(x = 0 ∧ y ≠ 0) ↔ x ≠ 0 ∨ y = 0
Tactic: rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
rw : ¬x ^ y = 0 ↔ x ≠ 0 ∨ y = 0
rw₁ : ¬(x = 0 ∧ y ≠ 0) ↔ x ≠ 0 ∨ y = 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0
have rw₂ : ¬x = 0 ∨ ¬y ≠ 0 ↔ x ≠ 0 ∨ y = 0
Tactic: rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
rw : ¬x ^ y = 0 ↔ x ≠ 0 ∨ y = 0
rw₁ : ¬(x = 0 ∧ y ≠ 0) ↔ x ≠ 0 ∨ y = 0
rw₂ : ¬x = 0 ∨ ¬y ≠ 0 ↔ x ≠ 0 ∨ y = 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0
have rw₃ : ¬x = 0 ∨ ¬¬y = 0 ↔ x ≠ 0 ∨ y = 0
Tactic: rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
rw : ¬x ^ y = 0 ↔ x ≠ 0 ∨ y = 0
rw₁ : ¬(x = 0 ∧ y ≠ 0) ↔ x ≠ 0 ∨ y = 0
rw₂ : ¬x = 0 ∨ ¬y ≠ 0 ↔ x ≠ 0 ∨ y = 0
rw₃ : ¬x = 0 ∨ ¬¬y = 0 ↔ x ≠ 0 ∨ y = 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0 ∨ y = 0
have rw₄ : ¬x = 0 ∨ y = 0 ↔ x ≠ 0 ∨ y = 0
Tactic: rw [ne_eq, cpow_eq_zero_iff, not_and_or, ne_eq, not_not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x a : ℂ
⊢ HPow.hPow (α := ℂ) 0 x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have mp : HPow.hPow (α := ℂ) 0 x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x a : ℂ
mp : HPow.hPow (α := ℂ) 0 x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
⊢ HPow.hPow (α := ℂ) 0 x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have mpr : x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → HPow.hPow (α := ℂ) 0 x = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (hypothesis)
Goal:
x a : ℂ
hyp : HPow.hPow (α := ℂ) 0 x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have hyp₁ : (if x = 0 then 1 else 0) = a
Tactic: simp only [cpow_def, if_true] at hyp
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x a : ℂ
⊢ a = HPow.hPow (α := ℂ) 0 x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have rw : a = HPow.hPow (α := ℂ) 0 x ↔ HPow.hPow (α := ℂ) 0 x = a
Tactic: rw [← zero_cpow_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x a : ℂ
rw : a = HPow.hPow (α := ℂ) 0 x ↔ HPow.hPow (α := ℂ) 0 x = a
⊢ a = HPow.hPow (α := ℂ) 0 x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
have rw₁ : HPow.hPow (α := ℂ) 0 x = a ↔ HPow.hPow (α := ℂ) 0 x = a
Tactic: rw [← zero_cpow_eq_iff, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
hx : ¬x = 0
⊢ HPow.hPow (β := ℂ) x 1 = x
have rw : (if x = 0 then if Eq (α := ℂ) 1 0 then 1 else 0 else cexp (log x * 1)) = x
Tactic: rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
hx : ¬x = 0
rw : (if x = 0 then if Eq (α := ℂ) 1 0 then 1 else 0 else cexp (log x * 1)) = x
⊢ HPow.hPow (β := ℂ) x 1 = x
have rw₁ : (if x = 0 then 0 else cexp (log x * 1)) = x
Tactic: rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
hx : ¬x = 0
rw : (if x = 0 then if Eq (α := ℂ) 1 0 then 1 else 0 else cexp (log x * 1)) = x
rw₁ : (if x = 0 then 0 else cexp (log x * 1)) = x
⊢ HPow.hPow (β := ℂ) x 1 = x
have rw₂ : cexp (log x * 1) = x
Tactic: rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
hx : ¬x = 0
rw : (if x = 0 then if Eq (α := ℂ) 1 0 then 1 else 0 else cexp (log x * 1)) = x
rw₁ : (if x = 0 then 0 else cexp (log x * 1)) = x
rw₂ : cexp (log x * 1) = x
⊢ HPow.hPow (β := ℂ) x 1 = x
have rw₃ : cexp (log x) = x
Tactic: rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
hx : ¬x = 0
rw : (if x = 0 then if Eq (α := ℂ) 1 0 then 1 else 0 else cexp (log x * 1)) = x
rw₁ : (if x = 0 then 0 else cexp (log x * 1)) = x
rw₂ : cexp (log x * 1) = x
rw₃ : cexp (log x) = x
⊢ HPow.hPow (β := ℂ) x 1 = x
have rw₄ : x = x
Tactic: rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
⊢ (if Eq (α := ℂ) 1 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1
have pos : Eq (α := ℂ) 1 0 → x = 0 → Eq (α := ℂ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
pos : Eq (α := ℂ) 1 0 → x = 0 → Eq (α := ℂ) 1 1
⊢ (if Eq (α := ℂ) 1 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1
have neg : Eq (α := ℂ) 1 0 → ¬x = 0 → Eq (α := ℂ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
pos : Eq (α := ℂ) 1 0 → x = 0 → Eq (α := ℂ) 1 1
neg : Eq (α := ℂ) 1 0 → ¬x = 0 → Eq (α := ℂ) 0 1
⊢ (if Eq (α := ℂ) 1 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1
have neg₁ : ¬Eq (α := ℂ) 1 0 → cexp (log 1 * x) = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z
have simp : (if x = 0 then if y + z = 0 then 1 else 0 else cexp (log x * (y + z))) =
  if x = 0 then
    if z = 0 then
      if x = 0 then if y = 0 then HMul.hMul (α := ℂ) 1 1 else HMul.hMul (α := ℂ) 0 1 else cexp (log x * y) * 1
    else if x = 0 then if y = 0 then HMul.hMul (α := ℂ) 1 0 else HMul.hMul (α := ℂ) 0 0 else cexp (log x * y) * 0
  else
    if x = 0 then if y = 0 then 1 * cexp (log x * z) else 0 * cexp (log x * z) else cexp (log x * y) * cexp (log x * z)
Tactic: simp only [cpow_def, ite_mul, mul_ite]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₄ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
neg₄ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 0 0
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₅ : x = 0 → ¬y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 0 = cexp (log 1 * z)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
neg₄ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₅ : x = 0 → ¬y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 0 = cexp (log 1 * z)
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have pos₃ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
neg₄ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₅ : x = 0 → ¬y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 0 = cexp (log 1 * z)
pos₃ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 0 1
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₆ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
neg₄ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₅ : x = 0 → ¬y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 0 = cexp (log 1 * z)
pos₃ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 0 1
neg₆ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 0 0
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₇ : x = 0 → ¬y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 0 = cexp (log 0 * z)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
neg₄ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₅ : x = 0 → ¬y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 0 = cexp (log 1 * z)
pos₃ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 0 1
neg₆ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₇ : x = 0 → ¬y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 0 = cexp (log 0 * z)
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have pos₄ : ¬x = 0 → cexp (log x * y) = 0 → z = 0 → cexp (log x * (y * z)) = 1
Tactic: split_ifs