awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
rwa : ‖(↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ)‖ < ε
rwa₁ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ) * (↑τ : ℂ)‖ < ε
rwa₂ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ)‖ * ‖(↑τ : ℂ)‖ < ε
rwa₃ : ‖r / ‖(↑τ : ℂ)‖ - 1‖ * ‖(↑τ : ℂ)‖ < ε
rwa₄ : ‖r / ‖‖(↑τ : ℂ)‖‖ - 1‖ * ‖‖(↑τ : ℂ)‖‖ < ε
rwa₅ : ‖(r / ‖‖(↑τ : ℂ)‖‖ - 1) * ‖(↑τ : ℂ)‖‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₆ : ‖r / ‖‖(↑τ : ℂ)‖‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
Tactic: rwa [mem_ball_iff_norm,
      show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,
      norm_mul, norm_real, ← norm_norm (τ : ℂ), ← norm_mul, sub_mul, norm_norm, one_mul,
      div_mul_cancel₀ _ (by simpa using τ.ne_zero), ← mem_ball_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
rwa : ‖(↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ)‖ < ε
rwa₁ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ) * (↑τ : ℂ)‖ < ε
rwa₂ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ)‖ * ‖(↑τ : ℂ)‖ < ε
rwa₃ : ‖r / ‖(↑τ : ℂ)‖ - 1‖ * ‖(↑τ : ℂ)‖ < ε
rwa₄ : ‖r / ‖‖(↑τ : ℂ)‖‖ - 1‖ * ‖‖(↑τ : ℂ)‖‖ < ε
rwa₅ : ‖(r / ‖‖(↑τ : ℂ)‖‖ - 1) * ‖(↑τ : ℂ)‖‖ < ε
rwa₆ : ‖r / ‖‖(↑τ : ℂ)‖‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₇ : ‖r / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
Tactic: rwa [mem_ball_iff_norm,
      show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,
      norm_mul, norm_real, ← norm_norm (τ : ℂ), ← norm_mul, sub_mul, norm_norm, one_mul,
      div_mul_cancel₀ _ (by simpa using τ.ne_zero), ← mem_ball_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
rwa : ‖(↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ)‖ < ε
rwa₁ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ) * (↑τ : ℂ)‖ < ε
rwa₂ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ)‖ * ‖(↑τ : ℂ)‖ < ε
rwa₃ : ‖r / ‖(↑τ : ℂ)‖ - 1‖ * ‖(↑τ : ℂ)‖ < ε
rwa₄ : ‖r / ‖‖(↑τ : ℂ)‖‖ - 1‖ * ‖‖(↑τ : ℂ)‖‖ < ε
rwa₅ : ‖(r / ‖‖(↑τ : ℂ)‖‖ - 1) * ‖(↑τ : ℂ)‖‖ < ε
rwa₆ : ‖r / ‖‖(↑τ : ℂ)‖‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
rwa₇ : ‖r / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₈ : ‖r / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ - ‖(↑τ : ℂ)‖‖ < ε
Tactic: rwa [mem_ball_iff_norm,
      show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,
      norm_mul, norm_real, ← norm_norm (τ : ℂ), ← norm_mul, sub_mul, norm_norm, one_mul,
      div_mul_cancel₀ _ (by simpa using τ.ne_zero), ← mem_ball_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
rwa : ‖(↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ)‖ < ε
rwa₁ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ) * (↑τ : ℂ)‖ < ε
rwa₂ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ)‖ * ‖(↑τ : ℂ)‖ < ε
rwa₃ : ‖r / ‖(↑τ : ℂ)‖ - 1‖ * ‖(↑τ : ℂ)‖ < ε
rwa₄ : ‖r / ‖‖(↑τ : ℂ)‖‖ - 1‖ * ‖‖(↑τ : ℂ)‖‖ < ε
rwa₅ : ‖(r / ‖‖(↑τ : ℂ)‖‖ - 1) * ‖(↑τ : ℂ)‖‖ < ε
rwa₆ : ‖r / ‖‖(↑τ : ℂ)‖‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
rwa₇ : ‖r / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
rwa₈ : ‖r / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ - ‖(↑τ : ℂ)‖‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₉ : ‖r - ‖(↑τ : ℂ)‖‖ < ε
Tactic: rwa [mem_ball_iff_norm,
      show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,
      norm_mul, norm_real, ← norm_norm (τ : ℂ), ← norm_mul, sub_mul, norm_norm, one_mul,
      div_mul_cancel₀ _ (by simpa using τ.ne_zero), ← mem_ball_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
⊢ Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r
have this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
Tactic: have : r / ‖(τ : ℂ)‖ * (τ : ℂ) ∈ Metric.ball (τ : ℂ) ε := by
    rwa [mem_ball_iff_norm,
      show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,
      norm_mul, norm_real, ← norm_norm (τ : ℂ), ← norm_mul, sub_mul, norm_norm, one_mul,
      div_mul_cancel₀ _ (by simpa using τ.ne_zero), ← mem_ball_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
⊢ Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r
have obtain : ∀ (ξ : ℍ) (hξs : ξ ∈ s) (hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)),
  Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r
Tactic: obtain ⟨ξ, hξs, hξτ⟩ := Set.mem_of_mem_of_subset this hεs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)
⊢ Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r
have right : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) ξ = r
Tactic: use ξ, hξs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)
⊢ (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) ξ = r
have right : ‖r‖ / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ = r
Tactic: simp_rw [hξτ, norm_mul, norm_div, norm_real, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)
⊢ ‖r‖ / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ = r
have right : ‖r‖ = r
Tactic: rw [div_mul_cancel₀ _ (by simpa using τ.ne_zero), Real.norm_of_nonneg hr']
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)
right : ‖r‖ = r
⊢ ‖r‖ / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ = r
have right₁ : r = r
Tactic: rw [div_mul_cancel₀ _ (by simpa using τ.ne_zero), Real.norm_of_nonneg hr']
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)) = 0
have simp_rw : log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a + f x) 0)) = 0
Tactic: simp_rw [sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a + f x) 0)) = 0
have rw : log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a) 0)) = 0
Tactic: rw [(meromorphicAt_of_meromorphicOrderAt_ne_zero
    h.ne').meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
rw : log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a) 0)) = 0
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ -a + f x) 0)) = 0
have rw₁ : meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ -a) 0 < meromorphicOrderAt f 0
Tactic: rw [(meromorphicAt_of_meromorphicOrderAt_ne_zero
    h.ne').meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ -a) 0 < meromorphicOrderAt f 0
have rw : (if -a = 0 then ⊤ else 0) < meromorphicOrderAt f 0
Tactic: rw [meromorphicOrderAt_const]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |1|)) (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖)
    fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))
have h : ∀ (a : ℂ) (ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a)
  (ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a),
  log ‖meromorphicTrailingCoeffAt f 0 - a‖ =
    log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))
Tactic: filter_upwards [self_mem_codiscreteWithin (sphere 0 |1|), compl_singleton_mem_codiscreteWithin
    (meromorphicTrailingCoeffAt f 0)] with a ha_sphere ha_ne
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
⊢ log ‖meromorphicTrailingCoeffAt f 0 - a‖ =
    log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))
have h : meromorphicTrailingCoeffAt f 0 - a = meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
⊢ meromorphicTrailingCoeffAt f 0 - a = meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0
have h : meromorphicOrderAt f 0 = meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
Tactic: rw [h₁.meromorphicTrailingCoeffAt_fun_sub_eq_sub
    (by fun_prop), meromorphicTrailingCoeffAt_const, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
h : meromorphicOrderAt f 0 = meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
⊢ meromorphicTrailingCoeffAt f 0 - a = meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0
have h₃ : meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ a) 0 ≠ 0
Tactic: rw [h₁.meromorphicTrailingCoeffAt_fun_sub_eq_sub
    (by fun_prop), meromorphicTrailingCoeffAt_const, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
⊢ meromorphicOrderAt f 0 = meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
have h : meromorphicOrderAt f 0 = if a = 0 then ⊤ else 0
Tactic: simp only [meromorphicOrderAt_const]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
ha_ne : Membership.mem (γ := Set ℂ) {meromorphicTrailingCoeffAt f 0}ᶜ a
⊢ meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ a) 0 ≠ 0
have h : ¬meromorphicTrailingCoeffAt f 0 - a = 0
Tactic: simp only [meromorphicTrailingCoeffAt_const, ne_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
have pos : ∀ (h : ¬MeromorphicAt f 0),
  CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
Tactic: by_cases h: ¬MeromorphicAt f 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
pos :
  ∀ (h : ¬MeromorphicAt f 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
have neg : ∀ (h : ¬¬MeromorphicAt f 0),
  CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
Tactic: by_cases h: ¬MeromorphicAt f 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (hypothesis)
Goal:
f : ℂ → ℂ
h : ¬MeromorphicAt f 0
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
have this : ∀ {a : ℂ}, ¬MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ f x - a) 0
Tactic: have {a : ℂ} : ¬MeromorphicAt (fun x ↦ f x - a) 0 := by
      rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
have neg : ∀ (hneg : meromorphicOrderAt f 0 < 0),
  CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
Tactic: rcases lt_trichotomy (meromorphicOrderAt f 0) 0 with hneg | hzero | hpos
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
neg :
  ∀ (hneg : meromorphicOrderAt f 0 < 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
have neg₁ : ∀ (hzero : meromorphicOrderAt f 0 = 0),
  CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
Tactic: rcases lt_trichotomy (meromorphicOrderAt f 0) 0 with hneg | hzero | hpos
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
neg :
  ∀ (hneg : meromorphicOrderAt f 0 < 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
neg₁ :
  ∀ (hzero : meromorphicOrderAt f 0 = 0),
    CircleIntegrable (E := ℝ)
      (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
have neg₂ : ∀ (hpos : 0 < meromorphicOrderAt f 0),
  CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
Tactic: rcases lt_trichotomy (meromorphicOrderAt f 0) 0 with hneg | hzero | hpos
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)) = log ‖meromorphicTrailingCoeffAt f 0‖
have neg : meromorphicOrderAt f 0 < meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
Tactic: rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
have neg : meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0
Tactic: rw [meromorphicOrderAt_const]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hzero : meromorphicOrderAt f 0 = 0
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
have neg : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1
Tactic: apply CircleIntegrable.congr_codiscreteWithin
     (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero (not_not.1 h) hzero)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hpos : 0 < meromorphicOrderAt f 0
⊢ CircleIntegrable (E := ℝ)
    (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1
have apply : EqOn (β := ℝ) (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)))
  (fun (x : ℂ) ↦ 0) (sphere 0 |1|)
Tactic: apply (circleIntegrable_congr _).2 (circleIntegrable_const 0 0 1)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖
have pos : ∀ (hf : MeromorphicAt f 0),
  circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Tactic: by_cases hf : MeromorphicAt f 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
pos :
  ∀ (hf : MeromorphicAt f 0),
    circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
      log⁺ ‖meromorphicTrailingCoeffAt f 0‖
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖
have neg : ∀ (hf : ¬MeromorphicAt f 0),
  circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Tactic: by_cases hf : MeromorphicAt f 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖
have pos : circleAverage (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Tactic: rw [← circleAverage_congr_codiscreteWithin
      (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero hf h) zero_ne_one.symm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
have pos : circleAverage (fun (x : ℂ) ↦ log ‖x - meromorphicTrailingCoeffAt f 0‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Tactic: simp_rw [norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - meromorphicTrailingCoeffAt f 0‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
have pos : log⁺ ‖meromorphicTrailingCoeffAt f 0‖ = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Tactic: rw [circleAverage_log_norm_sub_const_eq_posLog]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (hypothesis)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log⁺ ‖meromorphicTrailingCoeffAt f 0‖
have this : ∀ {a : ℂ}, ¬MeromorphicAt (E := ℂ) (fun (x : ℂ) ↦ f x - a) 0
Tactic: have {a : ℂ} : ¬ MeromorphicAt (fun x ↦ f x - a) 0 := by
    rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
⊢ circleAverage (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0))) 0 1 =
    log ‖meromorphicTrailingCoeffAt f 0‖
have rw : EqOn (β := ℝ) (fun (a : ℂ) ↦ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)))
  (fun (x : ℂ) ↦ log ‖meromorphicTrailingCoeffAt f 0‖) (sphere 0 |1|)
Tactic: rw [circleAverage_congr_sphere (f₂ := fun _ ↦ log ‖meromorphicTrailingCoeffAt f 0‖),
    circleAverage_const]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ log (Norm.norm (E := ℂ) (meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0)) = log ‖meromorphicTrailingCoeffAt f 0‖
have e_x : meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0 = meromorphicTrailingCoeffAt f 0
Tactic: congr 2