awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑R : ℂ) * (z - w)))
    x
have inl : AnalyticAt ℂ (F := ℂ)
  (fun (z : ℂ) ↦
    (HPow.hPow (β := ℕ) (↑0 : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) / ((↑0 : ℂ) * (z - w)))
  x
Tactic: obtain (rfl | h) := eq_or_ne R 0
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
inl :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑0 : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑0 : ℂ) * (z - w)))
    x
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑R : ℂ) * (z - w)))
    x
have inr : ∀ (h : R ≠ 0),
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑R : ℂ) * (z - w)))
    x
Tactic: obtain (rfl | h) := eq_or_ne R 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
h : R ≠ 0
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑R : ℂ) * (z - w)))
    x
have this : x - w ≠ 0
Tactic: have : x - w ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
h : R ≠ 0
this : x - w ≠ 0
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑R : ℂ) * (z - w)))
    x
have funProp : (↑R : ℂ) * (x - w) ≠ 0
Tactic: fun_prop (disch := positivity)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦
        (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
          ((↑R : ℂ) * (z - w)))
      w =
    -1
have rw : meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w -
    (meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ (↑R : ℂ)) w + meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ z - w) w) =
  -1
Tactic: rw [fun_meromorphicOrderAt_div (by fun_prop) (by fun_prop),
    fun_meromorphicOrderAt_mul (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w =
    0
have refine_1 : MeromorphicNFAt (E := ℂ)
  (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w
Tactic: refine (MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff ?_).2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
refine_1 :
  MeromorphicNFAt (E := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w
⊢ meromorphicOrderAt (E := ℂ)
      (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w =
    0
have refine_2 : HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) w ≠ 0
Tactic: refine (MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff ?_).2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ MeromorphicNFAt (E := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w
have refine_1 : AnalyticAt ℂ (F := ℂ)
  (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w
Tactic: apply AnalyticAt.meromorphicNFAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) w ≠ 0
have refine_2 : ¬R = ‖w‖
Tactic: rw [← normSq_eq_conj_mul_self, normSq_eq_norm_sq w, sub_ne_zero, ne_eq, ← ofReal_pow,
        ofReal_inj, sq_eq_sq₀ (pos_of_mem_ball h).le (norm_nonneg w)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ ¬R = ‖w‖
have h₁ : ‖w‖ < R
Tactic: rw [mem_ball_iff_norm, sub_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ meromorphicOrderAt (E := ℂ)
        (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w -
      (meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ (↑R : ℂ)) w + meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ z - w) w) =
    -1
have this : meromorphicOrderAt (E := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) w =
  0
Tactic: have : meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w = 0 := by
    refine (MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff ?_).2 ?_
    · apply AnalyticAt.meromorphicNFAt
      fun_prop
    · rw [← normSq_eq_conj_mul_self, normSq_eq_norm_sq w, sub_ne_zero, ne_eq, ← ofReal_pow,
        ofReal_inj, sq_eq_sq₀ (pos_of_mem_ball h).le (norm_nonneg w)]
      rw [mem_ball_iff_norm, sub_zero] at h
      grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
⊢ MeromorphicNFAt (canonicalFactor R w) z
have inl : ∀ (h : Membership.mem (γ := Set ℂ) (ball 0 R) z), MeromorphicNFAt (canonicalFactor R z) z
Tactic: obtain (rfl | h₁) := eq_or_ne z w
Cleared hypotheses: w, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w : ℂ
h : Membership.mem (γ := Set ℂ) (ball 0 R) w
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
inl : ∀ (h : Membership.mem (γ := Set ℂ) (ball 0 R) z), MeromorphicNFAt (canonicalFactor R z) z
⊢ MeromorphicNFAt (canonicalFactor R w) z
have inr : ∀ (h₁ : z ≠ w), MeromorphicNFAt (canonicalFactor R w) z
Tactic: obtain (rfl | h₁) := eq_or_ne z w
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
⊢ MeromorphicNFAt (canonicalFactor R z) z
have inl : AnalyticAt ℂ (canonicalFactor R z) z ∨
  MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0
Tactic: rw [meromorphicNFAt_iff_analyticAt_or]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
⊢ AnalyticAt ℂ (canonicalFactor R z) z ∨
    MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0
have inl : MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
z : ℂ
hz : Membership.mem (γ := Set ℂ) Set.univ z
h : Membership.mem (γ := Set ℂ) (ball 0 R) z
⊢ MeromorphicAt (canonicalFactor R z) z ∧ meromorphicOrderAt (canonicalFactor R z) z < 0 ∧ canonicalFactor R z z = 0
have inl : meromorphicOrderAt (canonicalFactor R z) z < 0
Tactic: refine ⟨meromorphicOn_canonicalFactor R z z (Set.mem_univ z), ?_, by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
⊢ canonicalFactor R w z ≠ 0
have hR : 0 < R
Tactic: obtain ⟨hR, hzw⟩ : 0 < R ∧ z - w ≠ 0 := by grind [mem_ball_zero_iff, norm_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
hR : 0 < R
⊢ canonicalFactor R w z ≠ 0
have hzw : z - w ≠ 0
Tactic: obtain ⟨hR, hzw⟩ : 0 < R ∧ z - w ≠ 0 := by grind [mem_ball_zero_iff, norm_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
⊢ canonicalFactor R w z ≠ 0
have hw₁ : ‖w‖ < R
Tactic: simp only [mem_ball, dist_zero_right, mem_closedBall] at hw h₁z
Cleared hypotheses: hw, h₁z
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
h₁z : Membership.mem (γ := Set ℂ) (closedBall 0 R) z
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw₁ : ‖w‖ < R
⊢ canonicalFactor R w z ≠ 0
have h₁z₁ : ‖z‖ ≤ R
Tactic: simp only [mem_ball, dist_zero_right, mem_closedBall] at hw h₁z
Cleared hypotheses: hw, h₁z
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
⊢ HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z ≠ 0
have suffices : ‖HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ < ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2‖
Tactic: suffices ‖conj w * z‖ < ‖(R : ℂ) ^ 2‖ by grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
⊢ ‖HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ < ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2‖
have suffices : ‖w‖ * ‖z‖ < R * R
Tactic: suffices ‖w‖ * ‖z‖ < R * R by simpa [sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
⊢ ‖w‖ * ‖z‖ < R * R
have grw : ‖w‖ * R < R * R
Tactic: grw [h₁z]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
⊢ canonicalFactor R w z ≠ 0
have h_num_ne_zero : HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z ≠ 0
Tactic: have h_num_ne_zero : R ^ 2 - conj w * z ≠ 0 := by
    suffices ‖conj w * z‖ < ‖(R : ℂ) ^ 2‖ by grind
    suffices ‖w‖ * ‖z‖ < R * R by simpa [sq]
    grw [h₁z]
    gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
⊢ ‖canonicalFactor R w z‖ = 1
have hR : 0 < R
Tactic: obtain ⟨hR, hzw⟩ : 0 < R ∧ z - w ≠ 0 := by
    grind [mem_ball_zero_iff, norm_nonneg, mem_sphere_zero_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (hypothesis)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
⊢ ‖canonicalFactor R w z‖ = 1
have hzw : z - w ≠ 0
Tactic: obtain ⟨hR, hzw⟩ : 0 < R ∧ z - w ≠ 0 := by
    grind [mem_ball_zero_iff, norm_nonneg, mem_sphere_zero_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖(↑R : ℂ) * (z - w)‖ ≠ 0
have rw : ¬(↑R : ℂ) * (z - w) = 0
Tactic: rw [ne_eq, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖canonicalFactor R w z‖ = 1
have rw : ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ = ‖(↑R : ℂ) * (z - w)‖
Tactic: rw [canonicalFactor, norm_div, div_eq_iff (by rw [ne_eq, norm_eq_zero]; positivity), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
R : ℝ
w z : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 R) z
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ = ‖(↑R : ℂ) * (z - w)‖
have obtain : ∀ (hw : Membership.mem (γ := Set ℂ) (ball 0 ‖z‖) w) (hz : Membership.mem (γ := Set ℂ) (sphere 0 ‖z‖) z) (hR : 0 < ‖z‖),
  ‖HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ =
    ‖(↑‖z‖ : ℂ) * (z - w)‖
Tactic: obtain rfl := by simpa [mem_sphere_zero_iff_norm] using hz
Cleared hypotheses: R, hw, hz, hR
-- Lean 4 proof step from Mathlib.Analysis.Complex.CanonicalDecomposition (goal)
Goal:
w z : ℂ
hzw : z - w ≠ 0
hw : Membership.mem (γ := Set ℂ) (ball 0 ‖z‖) w
hz : Membership.mem (γ := Set ℂ) (sphere 0 ‖z‖) z
hR : 0 < ‖z‖
⊢ ‖HPow.hPow (β := ℕ) (↑‖z‖ : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z‖ =
    ‖(↑‖z‖ : ℂ) * (z - w)‖
have rw : ‖z * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)‖ =
  ‖(↑‖z‖ : ℂ) * (z - w)‖
Tactic: rw [← ofReal_pow, ← normSq_eq_norm_sq, normSq_eq_conj_mul_self, ← sub_mul, mul_comm _ z]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Cardinality (goal)
Goal:
⊢ #ℂ = 𝔠
have rw : #(ℝ × ℝ) = 𝔠
Tactic: rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Cardinality (goal)
Goal:
rw : #(ℝ × ℝ) = 𝔠
⊢ #ℂ = 𝔠
have rw₁ : lift.{0, 0} #ℝ * lift.{0, 0} #ℝ = 𝔠
Tactic: rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Cardinality (goal)
Goal:
rw : #(ℝ × ℝ) = 𝔠
rw₁ : lift.{0, 0} #ℝ * lift.{0, 0} #ℝ = 𝔠
⊢ #ℂ = 𝔠
have rw₂ : #ℝ * #ℝ = 𝔠
Tactic: rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Cardinality (goal)
Goal:
rw : #(ℝ × ℝ) = 𝔠
rw₁ : lift.{0, 0} #ℝ * lift.{0, 0} #ℝ = 𝔠
rw₂ : #ℝ * #ℝ = 𝔠
⊢ #ℂ = 𝔠
have rw₃ : 𝔠 * 𝔠 = 𝔠
Tactic: rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Cardinality (goal)
Goal:
rw : #(ℝ × ℝ) = 𝔠
rw₁ : lift.{0, 0} #ℝ * lift.{0, 0} #ℝ = 𝔠
rw₂ : #ℝ * #ℝ = 𝔠
rw₃ : 𝔠 * 𝔠 = 𝔠
⊢ #ℂ = 𝔠
have rw₄ : 𝔠 = 𝔠
Tactic: rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Cardinality (goal)
Goal:
⊢ #(↑Set.univ : Type) = 𝔠
have rw : #ℂ = 𝔠
Tactic: rw [mk_univ, mk_complex]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Cardinality (goal)
Goal:
rw : #ℂ = 𝔠
⊢ #(↑Set.univ : Type) = 𝔠
have rw₁ : 𝔠 = 𝔠
Tactic: rw [mk_univ, mk_complex]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Cardinality (goal)
Goal:
⊢ ¬Set.Countable (α := ℂ) Set.univ
have rw : ℵ₀ < 𝔠
Tactic: rw [← le_aleph0_iff_set_countable, not_le, Cardinal.mk_univ_complex]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) 1 : E))
          ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) I : E)
have he : ∀ (x y : ℝ), (↑x : ℂ) + (↑y : ℂ) * I = (e : (a : ℝ × ℝ) → ℂ) (x, y)
Tactic: have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y) := fun x y => (mk_eq_add_mul_I x y).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), (↑x : ℂ) + (↑y : ℂ) * I = (e : (a : ℝ × ℝ) → ℂ) (x, y)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) 1 : E))
          ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) I : E)
have he₁ : Eq (α := ℂ) ((e : (a : ℝ × ℝ) → ℂ) (1, 0) : ℂ) (1 : ℂ)
Tactic: have he₁ : e (1, 0) = 1 := rfl
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), (↑x : ℂ) + (↑y : ℂ) * I = (e : (a : ℝ × ℝ) → ℂ) (x, y)
he₁ : Eq (α := ℂ) ((e : (a : ℝ × ℝ) → ℂ) (1, 0) : ℂ) (1 : ℂ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) 1 : E))
          ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) I : E)
have he₂ : (e : (a : ℝ × ℝ) → ℂ) (0, 1) = I
Tactic: have he₂ : e (0, 1) = I := rfl
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), (↑x : ℂ) + (↑y : ℂ) * I = (e : (a : ℝ × ℝ) → ℂ) (x, y)
he₁ : Eq (α := ℂ) ((e : (a : ℝ × ℝ) → ℂ) (1, 0) : ℂ) (1 : ℂ)
he₂ : (e : (a : ℝ × ℝ) → ℂ) (0, 1) = I
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) 1 : E))
          ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) I : E)
have simp : ∀ (he : ∀ (x y : ℝ), True),
  HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((e : (a : ℝ × ℝ) → ℂ) (x, z.im)))
          (∫ (x : ℝ) in z.re..w.re, f ((e : (a : ℝ × ℝ) → ℂ) (x, w.im))) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((e : (a : ℝ × ℝ) → ℂ) (w.re, y))) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((e : (a : ℝ × ℝ) → ℂ) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((e : (a : ℝ × ℝ) → ℂ) (x, y)) : (a : ℂ) → E) 1 : E))
          ((f' ((e : (a : ℝ × ℝ) → ℂ) (x, y)) : (a : ℂ) → E) I : E)
Tactic: simp only [he] at *
Cleared hypotheses: he