awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
hf : Differentiable ℂ f
n : WithTop ℕ∞
⊢ ContDiff ℂ n f

Tactic:
contDiff_iff_contDiffAt.mpr fun z ↦ (hf.analyticAt z).contDiffAt

Premises used: Iff.mpr, AnalyticAt.contDiffAt, contDiff_iff_contDiffAt, Differentiable.analyticAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
h : Differentiable ℂ f
z : ℂ
R : ℝ≥0
hR : 0 < R
⊢ HasFPowerSeriesOnBall f (cauchyPowerSeries f z (↑R : ℝ)) z ∞

Tactic:
(h.differentiableOn.hasFPowerSeriesOnBall hR).r_eq_top_of_exists fun _r hr =>
    ⟨_, h.differentiableOn.hasFPowerSeriesOnBall hr⟩

Premises used: DifferentiableOn.hasFPowerSeriesOnBall, HasFPowerSeriesOnBall.r_eq_top_of_exists, Exists.intro, Differentiable.differentiableOn, NNReal.toReal, cauchyPowerSeries
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s

Tactic:
⟨AnalyticOnNhd.differentiableOn, fun d _ zs ↦ d.analyticAt (o.mem_nhds zs)⟩

Premises used: IsOpen.mem_nhds, Iff.intro, DifferentiableOn.analyticAt, AnalyticOnNhd.differentiableOn
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
rw : AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s
⊢ AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s

Tactic:
rw [o.analyticOn_iff_analyticOnNhd]

Premises used: IsOpen.analyticOn_iff_analyticOnNhd
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s

Tactic:
analyticOnNhd_iff_differentiableOn o

Premises used: Complex.analyticOnNhd_iff_differentiableOn
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s

Tactic:
exact analyticOnNhd_iff_differentiableOn o

Premises used: Complex.analyticOnNhd_iff_differentiableOn
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
simp : AnalyticOnNhd ℂ f univ ↔ DifferentiableOn ℂ f univ
⊢ AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f

Tactic:
simp only [← differentiableOn_univ]

Premises used: differentiableOn_univ
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ DifferentiableOn ℂ f univ

Tactic:
analyticOnNhd_iff_differentiableOn isOpen_univ

Premises used: isOpen_univ, Complex.analyticOnNhd_iff_differentiableOn
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ DifferentiableOn ℂ f univ

Tactic:
exact analyticOnNhd_iff_differentiableOn isOpen_univ

Premises used: isOpen_univ, Complex.analyticOnNhd_iff_differentiableOn
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
rw : AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f
⊢ AnalyticOn ℂ f univ ↔ Differentiable ℂ f

Tactic:
rw [analyticOn_univ]

Premises used: analyticOn_univ
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f

Tactic:
analyticOnNhd_univ_iff_differentiable

Premises used: Complex.analyticOnNhd_univ_iff_differentiable
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f

Tactic:
exact analyticOnNhd_univ_iff_differentiable

Premises used: Complex.analyticOnNhd_univ_iff_differentiable
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
mpr : (∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z) → AnalyticAt ℂ f c
⊢ AnalyticAt ℂ f c ↔ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
fa : AnalyticAt ℂ f c
h : ∀ (a : ℂ), AnalyticAt ℂ f a → DifferentiableAt ℂ f a
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z

Tactic:
filter_upwards [fa.eventually_analyticAt]

Premises used: AnalyticAt.eventually_analyticAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
fa : AnalyticAt ℂ f c
⊢ ∀ (a : ℂ), AnalyticAt ℂ f a → DifferentiableAt ℂ f a

Tactic:
apply AnalyticAt.differentiableAt

Premises used: AnalyticAt.differentiableAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
mpr : ∀ (s : Set ℂ) (d : ∀ y ∈ s, DifferentiableAt ℂ f y) (o : IsOpen s) (m : c ∈ s), AnalyticAt ℂ f c
⊢ AnalyticAt ℂ f c

Tactic:
rcases _root_.eventually_nhds_iff.mp d with ⟨s, d, o, m⟩

Premises used: eventually_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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

Tactic:
DifferentiableOn.analyticOnNhd ?_ o

Premises used: DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
refine : DifferentiableOn ℂ f s
⊢ AnalyticOnNhd ℂ f s

Tactic:
refine DifferentiableOn.analyticOnNhd ?_ o

Premises used: DifferentiableOn.analyticOnNhd
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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_1 : c ∈ s
z : ℂ
m : z ∈ s
⊢ DifferentiableWithinAt ℂ f s z

Tactic:
(d z m).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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_1 : c ∈ s
z : ℂ
m : z ∈ s
⊢ DifferentiableWithinAt ℂ f s z

Tactic:
exact (d z m).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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

Tactic:
have h : AnalyticOnNhd ℂ f s := by
      refine DifferentiableOn.analyticOnNhd ?_ o
      intro z m
      exact (d z m).differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
h : AnalyticOnNhd ℂ f s
⊢ AnalyticAt ℂ f c

Tactic:
h _ m
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
h : AnalyticOnNhd ℂ f s
⊢ AnalyticAt ℂ f c

Tactic:
exact h _ m
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ 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

Tactic:
have := hasFPowerSeriesOnBall_of_differentiable_off_countable (R := .mk R h0.le) hs hc hd h0
      |>.factorial_smul 1 n
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
⊢ 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

Tactic:
rw [iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod, Finset.prod_const_one, one_smul] at this

Premises used: one_smul, Finset.prod_const_one, iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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
rw :
  ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z =
    HSMul.hSMul (α := ℂ) (β := E) 1 (∮ (z : ℂ) in C(c, (↑(NNReal.mk R ⋯) : ℝ)), (1 / (z - c)) ^ n • (z - c)⁻¹ • f z)
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c

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]

Premises used: div_mul_cancel₀, mul_inv_cancel₀, Complex.two_pi_I_ne_zero, cauchyPowerSeries_apply, Nat.cast_smul_eq_nsmul, Complex, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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 =
    HSMul.hSMul (α := ℂ) (β := E) 1 (∮ (z : ℂ) in C(c, (↑(NNReal.mk R ⋯) : ℝ)), (1 / (z - c)) ^ n • (z - c)⁻¹ • f z)

Tactic:
simp [← mul_smul, pow_succ, mul_comm]

Premises used: pow_succ, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
s : Set ℂ
h0 : 0 < R
hs : s.Countable
hc : ContinuousOn f (closedBall c R)
hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z
⊢ ∮ (z : ℂ) in C(c, R), (1 / HPow.hPow (β := ℕ) (z - c) 2) • f z = (2 * (↑π : ℂ) * I) • deriv f c

Tactic:
simpa using circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable
    h0 1 hs hc hd

Premises used: Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
h0 : 0 < R
n : ℕ
hc : DiffContOnCl ℂ f (ball c R)
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c

Tactic:
c.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable h0 n
    Set.countable_empty hc.continuousOn_ball fun _ hx ↦ hc.differentiableAt isOpen_ball hx.1

Premises used: DiffContOnCl.continuousOn_ball, Metric.isOpen_ball, And.left, Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable, DiffContOnCl.differentiableAt, Set.countable_empty
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
h0 : 0 < R
hc : DiffContOnCl ℂ f (ball c R)
⊢ ∮ (z : ℂ) in C(c, R), (1 / HPow.hPow (β := ℕ) (z - c) 2) • f z = (2 * (↑π : ℂ) * I) • deriv f c

Tactic:
simpa using DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul h0 1 hc

Premises used: DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
h0 : 0 < R
n : ℕ
hc : DifferentiableOn ℂ f (closedBall c R)
⊢ ∮ (z : ℂ) in C(c, R), (1 / (z - c) ^ (n + 1)) • f z = (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c

Tactic:
(hc.mono closure_ball_subset_closedBall).diffContOnCl
    |>.circleIntegral_one_div_sub_center_pow_smul h0 n

Premises used: DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul, Metric.closure_ball_subset_closedBall, DifferentiableOn.diffContOnCl, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
R : ℝ
f : ℂ → E
c : ℂ
h0 : 0 < R
hc : DifferentiableOn ℂ f (closedBall c R)
⊢ ∮ (z : ℂ) in C(c, R), (1 / HPow.hPow (β := ℕ) (z - c) 2) • f z = (2 * (↑π : ℂ) * I) • deriv f c

Tactic:
simpa using DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul h0 1 hc

Premises used: OfNat.ofNat, DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
⊢ ContinuousNeg Circle

Tactic:
inferInstanceAs <| ContinuousNeg (sphere _ _)

Premises used: _private.0.Circle.instContinuousNeg._proof_1
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
⊢ (↑x : ℂ) = (↑y : ℂ) → x = y

Tactic:
Subtype.ext

Premises used: Circle, Subtype.ext
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
⊢ Injective (α := ↥(Submonoid.unitSphere ℂ))
    (Subtype.val (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x))

Tactic:
fun _ _ ↦ ext

Premises used: Circle.ext, Circle, Function.Injective
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
⊢ (↑x : ℂ) = (↑y : ℂ) ↔ x = y

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, Circle, Circle.coe_injective
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z : Circle
⊢ ‖(↑z : ℂ)‖ = 1

Tactic:
mem_sphere_zero_iff_norm.1 z.2

Premises used: mem_sphere_zero_iff_norm, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z : Circle
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)

Tactic:
simp [normSq_eq_norm_sq]

Premises used: Complex.normSq_eq_norm_sq
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z : Circle
⊢ (↑z : ℂ) ≠ 0

Tactic:
ne_zero_of_mem_unit_sphere z

Premises used: ne_zero_of_mem_unit_sphere
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
⊢ Eq (α := ℂ) (↑1 : ℂ) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : Circle
rw : (↑x : ℂ) = 1 ↔ (↑x : ℂ) = (↑1 : ℂ)
rw₁ rw₂ : (↑x : ℂ) = 1 ↔ (↑x : ℂ) = 1
⊢ (↑x : ℂ) = 1 ↔ x = 1

Tactic:
rw [← coe_inj, coe_one]

Premises used: Circle.coe_inj, Circle.coe_one
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z w : Circle
⊢ (↑(z * w) : ℂ) = (↑z : ℂ) * (↑w : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z : Circle
⊢ (↑z⁻¹ : ℂ) = (↑z : ℂ)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
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 : ℂ)
rw₅ rw₆ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)
⊢ (↑z⁻¹ : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)

Tactic:
rw [coe_inv, inv_def, normSq_coe, inv_one, ofReal_one, mul_one]

Premises used: inv_one, Complex.ofReal_one, Complex.inv_def, Circle.coe_inv, Circle.normSq_coe, mul_one
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z w : Circle
⊢ (↑(z / w) : ℂ) = (↑z : ℂ) / (↑w : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z : Circle
n : ℕ
⊢ (↑(z ^ n) : ℂ) = (↑z : ℂ) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z : Circle
n : ℤ
⊢ (↑(z ^ n) : ℂ) = (↑z : ℂ) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : Circle
⊢ (↑(-x) : ℂ) = -(↑x : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : Circle
⊢ -x ≠ x

Tactic:
fun h ↦ coe_ne_zero x <| neg_eq_self.mp <| coe_neg x ▸ congrArg Subtype.val h

Premises used: neg_eq_self, congrArg, Eq.rec, Circle.coe_ne_zero, Iff.mp, Circle.coe_neg, Subtype.val, Not
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
z : Circle
⊢ (toUnits : (a : Circle) → ℂˣ) z = Units.mk0 (↑z : ℂ) ⋯

Tactic:
rfl

Premises used: Units.mk0, rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
⊢ CompactSpace Circle

Tactic:
inferInstanceAs <| CompactSpace (sphere _ _)

Premises used: _private.0.Circle.instCompactSpace._proof_1
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
⊢ IsTopologicalGroup Circle

Tactic:
inferInstanceAs <| IsTopologicalGroup (sphere _ _)

Premises used: _private.0.Circle.instIsTopologicalGroup._proof_1
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
z : ℂ
hz : z ≠ 0
rw : ‖z‖ ≠ 0
⊢ ‖HDiv.hDiv (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z‖ = 1

Tactic:
rw [norm_div, RCLike.norm_conj, div_self]

Premises used: RCLike.norm_conj, norm_div, div_self
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
z : ℂ
hz : z ≠ 0
⊢ ‖z‖ ≠ 0

Tactic:
norm_ne_zero_iff.mpr hz

Premises used: Iff.mpr, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
z : ℂ
hz : z ≠ 0
⊢ ‖z‖ ≠ 0

Tactic:
exact norm_ne_zero_iff.mpr hz

Premises used: Iff.mpr, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
t : ℝ
⊢ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) (cexp ((↑t : ℂ) * I))

Tactic:
simp [Submonoid.unitSphere, exp_mul_I, norm_cos_add_sin_mul_I]

Premises used: Complex.norm_cos_add_sin_mul_I, Complex.exp_mul_I, Submonoid.unitSphere
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
⊢ Continuous (Y := ℂ) fun (t : ℝ) ↦ cexp ((↑t : ℂ) * I)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
⊢ ∀ (x : ℝ), Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) (cexp ((↑x : ℂ) * I))

Tactic:
simp [Submonoid.unitSphere, exp_mul_I, norm_cos_add_sin_mul_I]

Premises used: Complex.norm_cos_add_sin_mul_I, Complex.exp_mul_I, Submonoid.unitSphere
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
t : ℝ
⊢ (↑((exp : (a : ℝ) → Circle) t) : ℂ) = cexp ((↑t : ℂ) * I)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
rw : cexp ((↑0 : ℂ) * I) = (↑1 : ℂ)
rw₁ : cexp (0 * I) = (↑1 : ℂ)
rw₂ : cexp 0 = (↑1 : ℂ)
rw₃ : Eq (α := ℂ) 1 (↑1 : ℂ)
rw₄ rw₅ : Eq (α := ℂ) 1 1
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) 0) : ℂ) (↑1 : ℂ)

Tactic:
rw [coe_exp, ofReal_zero, zero_mul, Complex.exp_zero, coe_one]

Premises used: Complex.exp_zero, MulZeroClass.zero_mul, Complex.ofReal_zero, Circle.coe_exp, Circle.coe_one
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : ℝ
⊢ (↑((exp : (a : ℝ) → Circle) (x + y)) : ℂ) =
    (↑(HMul.hMul (α := Circle) (β := Circle) ((exp : (a : ℝ) → Circle) x : Circle)
          ((exp : (a : ℝ) → Circle) y : Circle)) :
      ℂ)

Tactic:
simp only [coe_exp, ofReal_add, add_mul, Complex.exp_add, coe_mul]

Premises used: add_mul, Complex.exp_add, Complex.ofReal_add, Circle.coe_mul, Circle.coe_exp
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : ℝ
⊢ (exp : (a : ℝ) → Circle) (x - y) =
    HDiv.hDiv (α := Circle) (β := Circle) ((exp : (a : ℝ) → Circle) x : Circle) ((exp : (a : ℝ) → Circle) y : Circle)

Tactic:
expHom.map_sub x y

Premises used: Circle.expHom, Additive, Circle, AddMonoidHom.map_sub
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
⊢ Eq (α := Circle) ((exp : (a : ℝ) → Circle) (-x) : Circle) (((exp : (a : ℝ) → Circle) x)⁻¹ : Circle)

Tactic:
expHom.map_neg x

Premises used: Circle.expHom, Additive, AddMonoidHom.map_neg, Circle
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
n : ℕ
⊢ (exp : (a : ℝ) → Circle) (n • x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n

Tactic:
expHom.map_nsmul n x

Premises used: Circle.expHom, Additive, AddMonoidHom.map_nsmul, Circle
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
z : ℤ
⊢ (exp : (a : ℝ) → Circle) (z • x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z

Tactic:
expHom.map_zsmul z x

Premises used: Circle.expHom, AddMonoidHom.map_zsmul, Additive, Circle
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
n : ℕ
rw : (exp : (a : ℝ) → Circle) (n • x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n
rw₁ rw₂ :
  HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n =
    HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n
⊢ (exp : (a : ℝ) → Circle) ((↑n : ℝ) * x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) n

Tactic:
rw [← nsmul_eq_mul, exp_nsmul]

Premises used: nsmul_eq_mul, Circle.exp_nsmul
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
z : ℤ
rw : (exp : (a : ℝ) → Circle) (z • x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z
rw₁ rw₂ :
  HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z =
    HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z
⊢ (exp : (a : ℝ) → Circle) ((↑z : ℝ) * x) = HPow.hPow (α := Circle) ((exp : (a : ℝ) → Circle) x : Circle) z

Tactic:
rw [← zsmul_eq_mul, exp_zsmul]

Premises used: zsmul_eq_mul, Circle.exp_zsmul
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
h : Eq (α := Circle) ((exp : (a : ℝ) → Circle) Real.pi : Circle) (1 : Circle)
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) Real.pi) : ℂ) 1

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
h : Eq (α := Circle) ((exp : (a : ℝ) → Circle) Real.pi : Circle) (1 : Circle)
⊢ Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) Real.pi) : ℂ) 1

Tactic:
have heq : (Circle.exp Real.pi : ℂ) = 1 := by simp [h]