awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
⊢ (t ∩ (ball c R \ s)).Nonempty
have rcases : ∀ (l u : ℝ) (hlu₀ : 0 ∈ Ioo l u) (hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)), (t ∩ (ball c R \ s)).Nonempty
Tactic: rcases mem_nhds_iff_exists_Ioo_subset.1 (this <| inter_mem ht <| isOpen_ball.mem_nhds hw) with
    ⟨l, u, hlu₀, hlu_sub⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
⊢ (Ioo l u \ g ⁻¹' s).Nonempty
have refine : ∀ (hsub : Ioo l u ⊆ g ⁻¹' s), False
Tactic: refine diff_nonempty.2 fun hsub => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
⊢ False
have this₁ : (Ioo l u).Countable
Tactic: have : (Ioo l u).Countable :=
      (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this_1 : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
hsub : Ioo l u ⊆ g ⁻¹' s
this : (Ioo l u).Countable
⊢ False
have this₁ : Cardinal.continuum ≤ Cardinal.aleph0
Tactic: rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
hR : 0 < R
t : Set ℂ
ht : t ∈ 𝓝 w
g : ℝ → ℂ := fun (x : ℝ) ↦ w + (↑x : ℂ)
this : Tendsto g (𝓝 0) (𝓝 w)
l u : ℝ
hlu₀ : 0 ∈ Ioo l u
hlu_sub : Ioo l u ⊆ g ⁻¹' (t ∩ ball c R)
⊢ (t ∩ (ball c R \ s)).Nonempty
have obtain : ∀ (x : ℝ) (hx : x ∈ Ioo l u \ g ⁻¹' s), (t ∩ (ball c R \ s)).Nonempty
Tactic: obtain ⟨x, hx⟩ : (Ioo l u \ g ⁻¹' s).Nonempty := by
    refine diff_nonempty.2 fun hsub => ?_
    have : (Ioo l u).Countable :=
      (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub
    rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this
    exact this.not_gt Cardinal.aleph0_lt_continuum
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * (↑π : ℂ) * I) • f w
have ha : 2 * (↑π : ℂ) * I ≠ 0
Tactic: rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    hs hw hc hd, smul_inv_smul₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
have hR : 0 < R
Tactic: have hR : 0 < R := not_le.mp (ball_eq_empty.not.mp (Set.nonempty_of_mem hw).ne_empty)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
have refine_1 : ContinuousOn f (closedBall c R)
Tactic: refine two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    countable_empty hw ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
refine_1 : ContinuousOn f (closedBall c R)
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = f w
have refine_2 : ∀ x ∈ ball c R \ ∅, DifferentiableAt ℂ f x
Tactic: refine two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
    countable_empty hw ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ z ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : Membership.mem (γ := Set ℂ) (eball 0 (↑R : ℝ≥0∞)) w
⊢ HasSum (fun (n : ℕ) ↦ (cauchyPowerSeries f c (↑R : ℝ) n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ w) (f (c + w))
have hw' : c + w ∈ ball c (↑R : ℝ)
Tactic: have hw' : c + w ∈ ball c R := by
      simpa only [add_mem_ball_iff_norm, ← coe_nnnorm, mem_eball_zero_iff,
        NNReal.coe_lt_coe, enorm_lt_coe] using hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ≥0
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c (↑R : ℝ))
hd : ∀ z ∈ ball c (↑R : ℝ) \ s, DifferentiableAt ℂ f z
hR : 0 < R
w : ℂ
hw : Membership.mem (γ := Set ℂ) (eball 0 (↑R : ℝ≥0∞)) w
hw' : c + w ∈ ball c (↑R : ℝ)
⊢ HasSum (fun (n : ℕ) ↦ (cauchyPowerSeries f c (↑R : ℝ) n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ w) (f (c + w))
have rw : HasSum (fun (n : ℕ) ↦ (cauchyPowerSeries f c (↑R : ℝ) n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ w)
  (HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, (↑R : ℝ)), (z - (c + w))⁻¹ • f z))
Tactic: rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
      hs hw' hc hd]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
⊢ AnalyticAt ℂ f z
have rcases : ∀ (R : ℝ) (hR0 : 0 < R) (hRs : closedBall z R ⊆ s), AnalyticAt ℂ f z
Tactic: rcases nhds_basis_closedBall.mem_iff.1 hz with ⟨R, hR0, hRs⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ
hR0 : 0 < R
hRs : closedBall z R ⊆ s
⊢ AnalyticAt ℂ f z
have lift : ∀ (R : ℝ≥0) (hR0 : 0 < (↑R : ℝ)) (hRs : closedBall z (↑R : ℝ) ⊆ s), AnalyticAt ℂ f z
Tactic: lift R to ℝ≥0 using hR0.le
Cleared hypotheses: R, hR0, hRs
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s
have rw : AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s
Tactic: rw [o.analyticOn_iff_analyticOnNhd]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f
have simp : AnalyticOnNhd ℂ f univ ↔ DifferentiableOn ℂ f univ
Tactic: simp only [← differentiableOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
⊢ AnalyticOn ℂ f univ ↔ Differentiable ℂ f
have rw : AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f
Tactic: rw [analyticOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ AnalyticAt ℂ f c ↔ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
have mp : AnalyticAt ℂ f c → ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
mp : AnalyticAt ℂ f c → ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
⊢ AnalyticAt ℂ f c ↔ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
have mpr : (∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z) → AnalyticAt ℂ f c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
fa : AnalyticAt ℂ f c
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
have h : ∀ (a : ℂ), AnalyticAt ℂ f a → DifferentiableAt ℂ f a
Tactic: filter_upwards [fa.eventually_analyticAt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
d : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
⊢ AnalyticAt ℂ f c
have mpr : ∀ (s : Set ℂ) (d : ∀ y ∈ s, DifferentiableAt ℂ f y) (o : IsOpen s) (m : c ∈ s), AnalyticAt ℂ f c
Tactic: rcases _root_.eventually_nhds_iff.mp d with ⟨s, d, o, m⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
d_1 : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
s : Set ℂ
d : ∀ y ∈ s, DifferentiableAt ℂ f y
o : IsOpen s
m : c ∈ s
⊢ AnalyticOnNhd ℂ f s
have refine : DifferentiableOn ℂ f s
Tactic: refine DifferentiableOn.analyticOnNhd ?_ o
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
d_1 : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
s : Set ℂ
d : ∀ y ∈ s, DifferentiableAt ℂ f y
o : IsOpen s
m : c ∈ s
⊢ AnalyticAt ℂ f c
have h : AnalyticOnNhd ℂ f s
Tactic: have h : AnalyticOnNhd ℂ f s := by
      refine DifferentiableOn.analyticOnNhd ?_ o
      intro z m
      exact (d z m).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c
have this : HSMul.hSMul (β := E) n.factorial
    ((cauchyPowerSeries f c (↑(NNReal.mk R sorry) : ℝ) n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ 1 : E) =
  (iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ 1
Tactic: have := hasFPowerSeriesOnBall_of_differentiable_off_countable (R := .mk R h0.le) hs hc hd h0
      |>.factorial_smul 1 n
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this :
  HSMul.hSMul (β := E) n.factorial
      ((cauchyPowerSeries f c (↑(NNReal.mk R ⋯) : ℝ) n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ 1 : E) =
    (iteratedFDeriv ℂ n f c : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ 1
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c
have this₁ : HSMul.hSMul (β := E) n.factorial
    ((cauchyPowerSeries f c (↑(NNReal.mk R sorry) : ℝ) n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ 1 : E) =
  iteratedDeriv n f c
Tactic: rw [iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod, Finset.prod_const_one, one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
n : ℕ
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
this :
  HSMul.hSMul (β := E) n.factorial
      ((cauchyPowerSeries f c (↑(NNReal.mk R ⋯) : ℝ) n : (a : (i : Fin n) → ℂ) → E) fun (x : Fin n) ↦ 1 : E) =
    iteratedDeriv n f c
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c
have rw : ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
  HSMul.hSMul (α := ℂ) (β := E) 1 (∮ (z : ℂ) in C(c, (↑(NNReal.mk R sorry) : ℝ)), (1 / (z - c)) ^ n • (z - c)⁻¹ • f z)
Tactic: rw [← this, cauchyPowerSeries_apply, ← Nat.cast_smul_eq_nsmul ℂ, ← mul_smul, ← mul_smul,
    div_mul_cancel₀ _ (mod_cast n.factorial_ne_zero), mul_inv_cancel₀ two_pi_I_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x : Circle
⊢ (↑x : ℂ) = 1 ↔ x = 1
have rw : (↑x : ℂ) = 1 ↔ (↑x : ℂ) = (↑1 : ℂ)
Tactic: rw [← coe_inj, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x : Circle
rw : (↑x : ℂ) = 1 ↔ (↑x : ℂ) = (↑1 : ℂ)
⊢ (↑x : ℂ) = 1 ↔ x = 1
have rw₁ : (↑x : ℂ) = 1 ↔ (↑x : ℂ) = 1
Tactic: rw [← coe_inj, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
z : Circle
⊢ (↑z⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
have rw : (↑z : ℂ)⁻¹ = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
Tactic: rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
z : Circle
rw : (↑z : ℂ)⁻¹ = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
⊢ (↑z⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
have rw₁ : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑((normSq : (a : ℂ) → ℝ) (↑z : ℂ))⁻¹ : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
Tactic: rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
z : Circle
rw : (↑z : ℂ)⁻¹ = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑((normSq : (a : ℂ) → ℝ) (↑z : ℂ))⁻¹ : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
⊢ (↑z⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
have rw₂ : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑1⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
Tactic: rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
z : Circle
rw : (↑z : ℂ)⁻¹ = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑((normSq : (a : ℂ) → ℝ) (↑z : ℂ))⁻¹ : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₂ :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑1⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
⊢ (↑z⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
have rw₃ : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
Tactic: rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
z : Circle
rw : (↑z : ℂ)⁻¹ = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑((normSq : (a : ℂ) → ℝ) (↑z : ℂ))⁻¹ : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₂ :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑1⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₃ : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
⊢ (↑z⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
have rw₄ : HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (1 : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
Tactic: rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
z : Circle
rw : (↑z : ℂ)⁻¹ = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑((normSq : (a : ℂ) → ℝ) (↑z : ℂ))⁻¹ : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₂ :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑1⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₃ : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (↑1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
rw₄ :
  HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
⊢ (↑z⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)
have rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)
Tactic: rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x y : Circle
z : ℂ
hz : z ≠ 0
⊢ ‖HDiv.hDiv (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z‖ = 1
have rw : ‖z‖ ≠ 0
Tactic: rw [norm_div, RCLike.norm_conj, div_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) 0) : ℂ) (↑1 : ℂ)
have rw : cexp ((↑0 : ℂ) * I) = (↑1 : ℂ)
Tactic: rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
rw : cexp ((↑0 : ℂ) * I) = (↑1 : ℂ)
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) 0) : ℂ) (↑1 : ℂ)
have rw₁ : cexp (0 * I) = (↑1 : ℂ)
Tactic: rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
rw : cexp ((↑0 : ℂ) * I) = (↑1 : ℂ)
rw₁ : cexp (0 * I) = (↑1 : ℂ)
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) 0) : ℂ) (↑1 : ℂ)
have rw₂ : cexp 0 = (↑1 : ℂ)
Tactic: rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
rw : cexp ((↑0 : ℂ) * I) = (↑1 : ℂ)
rw₁ : cexp (0 * I) = (↑1 : ℂ)
rw₂ : cexp 0 = (↑1 : ℂ)
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) 0) : ℂ) (↑1 : ℂ)
have rw₃ : Eq (α := ℂ) 1 (↑1 : ℂ)
Tactic: rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
rw : cexp ((↑0 : ℂ) * I) = (↑1 : ℂ)
rw₁ : cexp (0 * I) = (↑1 : ℂ)
rw₂ : cexp 0 = (↑1 : ℂ)
rw₃ : Eq (α := ℂ) 1 (↑1 : ℂ)
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) 0) : ℂ) (↑1 : ℂ)
have rw₄ : Eq (α := ℂ) 1 1
Tactic: rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x : ℝ
n : ℕ
⊢ (exp : (a : ℝ) → Circle) ((↑n : ℝ) * x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n
have rw : (exp : (a : ℝ) → Circle) (n • x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n
Tactic: rw [← nsmul_eq_mul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x : ℝ
n : ℕ
rw : (exp : (a : ℝ) → Circle) (n • x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n
⊢ (exp : (a : ℝ) → Circle) ((↑n : ℝ) * x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n
have rw₁ : HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n =
  HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n
Tactic: rw [← nsmul_eq_mul, exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x : ℝ
z : ℤ
⊢ (exp : (a : ℝ) → Circle) ((↑z : ℝ) * x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z
have rw : (exp : (a : ℝ) → Circle) (z • x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z
Tactic: rw [← zsmul_eq_mul, exp_zsmul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x : ℝ
z : ℤ
rw : (exp : (a : ℝ) → Circle) (z • x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z
⊢ (exp : (a : ℝ) → Circle) ((↑z : ℝ) * x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z
have rw₁ : HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z =
  HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z
Tactic: rw [← zsmul_eq_mul, exp_zsmul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (hypothesis)
Goal:
h : Eq (α := Circle) ((exp : (a : ℝ) → Circle) Real.pi : Circle) (1 : Circle)
⊢ False
have heq : Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) Real.pi) : ℂ) 1
Tactic: have heq : (Circle.exp Real.pi : ℂ) = 1 := by simp [h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (hypothesis)
Goal:
h : Eq (α := Circle) ((exp : (a : ℝ) → Circle) Real.pi : Circle) (1 : Circle)
heq : Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) Real.pi) : ℂ) 1
⊢ False
have heq₁ : Eq (α := ℂ) (-1) 1
Tactic: rw [Circle.coe_exp, exp_pi_mul_I] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
e : AddChar ℝ Circle
x : ℝ
⊢ Eq (α := ℂ) (star (↑((e : (a : ℝ) → Circle) x) : ℂ)) (↑((e : (a : ℝ) → Circle) (-x)) : ℂ)
have refine_2 : ∀
  (h :
    (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
              (↑((e : (a : ℝ) → Circle) x) : ℂ) sorry)⁻¹ :
        ℂ) =
      (starRingEnd ℂ : (a : ℂ) → ℂ)
        (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
              (↑((e : (a : ℝ) → Circle) x) : ℂ) sorry) :
          ℂ)),
  Eq (α := ℂ) (star (↑((e : (a : ℝ) → Circle) x) : ℂ)) (↑((e : (a : ℝ) → Circle) (-x)) : ℂ)
Tactic: have h := Circle.coe_inv_eq_conj ⟨e x, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
e : AddChar ℝ Circle
x : ℝ
refine_2 :
  ∀
    (h :
      (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                (↑((e : (a : ℝ) → Circle) x) : ℂ) ⋯)⁻¹ :
          ℂ) =
        (starRingEnd ℂ : (a : ℂ) → ℂ)
          (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                (↑((e : (a : ℝ) → Circle) x) : ℂ) ⋯) :
            ℂ)),
    Eq (α := ℂ) (star (↑((e : (a : ℝ) → Circle) x) : ℂ)) (↑((e : (a : ℝ) → Circle) (-x)) : ℂ)
⊢ Eq (α := ℂ) (star (↑((e : (a : ℝ) → Circle) x) : ℂ)) (↑((e : (a : ℝ) → Circle) (-x)) : ℂ)
have refine_1 : Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) (↑((e : (a : ℝ) → Circle) x) : ℂ)
Tactic: have h := Circle.coe_inv_eq_conj ⟨e x, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
u : Circle
v : E
⊢ ‖u • v‖ = ‖v‖
have rw : ‖(↑u : ℂ) • v‖ = ‖v‖
Tactic: rw [smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]