awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
nth_rw : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp 0 * (cexp (-((↑x : ℂ) / 2) * I) - cexp ((↑x : ℂ) / 2 * I)) * I‖
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖(cexp (-((↑x : ℂ) / 2) * I) - cexp ((↑x : ℂ) / 2 * I)) * I‖

Tactic:
nth_rw 2 [← one_mul (_ - _), ← exp_zero]

Premises used: Complex.exp_zero, HSub.hSub, one_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw :
  ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑x : ℂ) / 2 * I)) *
          (cexp (((↑x : ℂ) / 2 + -((↑x : ℂ) / 2)) * I) - cexp (((↑x : ℂ) / 2 + (↑x : ℂ) / 2) * I)) *
        I‖
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp 0 * (cexp (-((↑x : ℂ) / 2) * I) - cexp ((↑x : ℂ) / 2 * I)) * I‖

Tactic:
rw [← neg_add_cancel (x / 2 * I), exp_add, mul_assoc _ _ (_ - _), mul_sub, ← exp_add, ← exp_add,
    ← add_mul, ← add_mul]

Premises used: add_mul, HMul.hMul, Complex.exp_add, mul_sub, mul_assoc, HSub.hSub, HDiv.hDiv, Complex.ofReal, neg_add_cancel, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
norm_cast :
  ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑(x / 2 + -(x / 2)) : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑x : ℂ) / 2 * I)) *
          (cexp (((↑x : ℂ) / 2 + -((↑x : ℂ) / 2)) * I) - cexp (((↑x : ℂ) / 2 + (↑x : ℂ) / 2) * I)) *
        I‖

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
norm_cast : -(x / 2) = -x / 2
⊢ -(↑(x / 2) : ℂ) = (↑(-x / 2) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ -(x / 2) = -x / 2

Tactic:
neg_div' 2 x

Premises used: neg_div', OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ -(x / 2) = -x / 2

Tactic:
exact neg_div' 2 x

Premises used: neg_div', OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw :
  ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑0 : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
rw₈ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖
rw₉ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₀ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp ((↑(-x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₁ : ‖cexp (I * (↑x : ℂ)) - 1‖ = 1 * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₃ : ‖-(cexp (I * (↑x : ℂ)) - 1)‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₄ : ‖1 - cexp (I * (↑x : ℂ))‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₅ rw₁₆ : ‖1 - cexp ((↑x : ℂ) * I)‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑(x / 2 + -(x / 2)) : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖

Tactic:
rw [add_neg_cancel, ofReal_zero, zero_mul, exp_zero, add_halves, ← neg_mul, Complex.norm_mul,
    norm_I, mul_one, Complex.norm_mul,
    show -(ofReal (x / 2)) = ofReal (-x / 2) by norm_cast; exact neg_div' 2 x,
    norm_exp_ofReal_mul_I, one_mul, ← norm_neg, neg_sub, mul_comm]

Premises used: add_neg_cancel, neg_sub, add_halves, Complex.exp_zero, MulZeroClass.zero_mul, Complex.ofReal_zero, norm_neg, Complex.norm_I, mul_comm, neg_mul, mul_one, Complex.norm_exp_ofReal_mul_I, Complex.norm_mul, one_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
z : ℂ
rw : ‖cexp (↑z.re : ℂ) * (cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I)‖ = Real.exp z.re
rw₁ : ‖cexp (↑z.re : ℂ)‖ * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
rw₂ : Real.exp z.re * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
rw₃ : Real.exp z.re * 1 = Real.exp z.re
rw₄ rw₅ : Real.exp z.re = Real.exp z.re
⊢ ‖cexp z‖ = Real.exp z.re

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
    mul_one]

Premises used: Complex.norm_cos_add_sin_mul_I, Complex.norm_exp_ofReal, Complex.exp_eq_exp_re_mul_sin_add_cos, mul_one, Complex.norm_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
rw : Real.exp x.re = ‖cexp y‖ ↔ x.re = y.re
rw₁ : Real.exp x.re = Real.exp y.re ↔ x.re = y.re
rw₂ rw₃ : x.re = y.re ↔ x.re = y.re
⊢ ‖cexp x‖ = ‖cexp y‖ ↔ x.re = y.re

Tactic:
rw [norm_exp, norm_exp, Real.exp_eq_exp]

Premises used: Real.exp_eq_exp, Complex.norm_exp
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ IsCancelMulZero 𝔻

Tactic:
inferInstanceAs <| IsCancelMulZero (ball _ _)

Premises used: _private.0.Complex.UnitDisc.instIsCancelMulZero._proof_1
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ Injective UnitDisc.coe

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective, Complex.UnitDisc, Complex.UnitDisc.coe
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z w : 𝔻
⊢ (↑z : ℂ) = (↑w : ℂ) ↔ z = w

Tactic:
Subtype.val_inj

Premises used: Subtype.val_inj, Complex.UnitDisc, Complex.UnitDisc.coe
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ Topology.IsEmbedding UnitDisc.coe

Tactic:
.subtypeVal

Premises used: Complex.UnitDisc, Complex.UnitDisc.coe, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ Continuous UnitDisc.coe

Tactic:
isEmbedding_coe.continuous

Premises used: Complex.UnitDisc.isEmbedding_coe, Topology.IsEmbedding.continuous
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ ‖(↑z : ℂ)‖ < 1

Tactic:
mem_ball_zero_iff.1 z.2

Premises used: Iff.mp, mem_ball_zero_iff, Subtype.property
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ ‖(↑z : ℂ)‖ ≠ 1

Tactic:
z.norm_lt_one.ne

Premises used: Complex.UnitDisc.norm_lt_one, LT.lt.ne
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
rw : ‖(↑z : ℂ)‖ < 1
⊢ HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 < 1

Tactic:
rw [sq_lt_one_iff_abs_lt_one, abs_norm]

Premises used: sq_lt_one_iff_abs_lt_one, abs_norm
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ ‖(↑z : ℂ)‖ < 1

Tactic:
z.norm_lt_one

Premises used: Complex.UnitDisc.norm_lt_one
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ ‖(↑z : ℂ)‖ < 1

Tactic:
exact z.norm_lt_one

Premises used: Complex.UnitDisc.norm_lt_one
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
rw : HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 < 1
⊢ LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)

Tactic:
rw [← Complex.norm_mul_self_eq_normSq, ← sq]

Premises used: Complex.norm_mul_self_eq_normSq, sq
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 < 1

Tactic:
z.sq_norm_lt_one

Premises used: Complex.UnitDisc.sq_norm_lt_one
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 < 1

Tactic:
exact z.sq_norm_lt_one

Premises used: Complex.UnitDisc.sq_norm_lt_one
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ Ne (α := ℝ) ((fun (x : ℂ) ↦ ‖x‖) (↑z : ℂ)) ((fun (x : ℂ) ↦ ‖x‖) 1)

Tactic:
simp [z.norm_ne_one]

Premises used: Complex.UnitDisc.norm_ne_one
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ Ne (α := ℝ) ((fun (x : ℂ) ↦ ‖x‖) (↑z : ℂ)) ((fun (x : ℂ) ↦ ‖x‖) (-1))

Tactic:
simpa [norm_neg] using z.norm_ne_one

Premises used: Complex.UnitDisc.norm_ne_one, norm_neg
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ 1 + (↑z : ℂ) ≠ 0

Tactic:
mt neg_eq_iff_add_eq_zero.2 z.coe_ne_neg_one.symm

Premises used: Iff.mpr, neg_eq_iff_add_eq_zero, mt, Ne.symm, Complex.UnitDisc.coe_ne_neg_one
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z w : 𝔻
⊢ (↑(z * w) : ℂ) = (↑z : ℂ) * (↑w : ℂ)

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (↑(-z) : ℂ) = -(↑z : ℂ)

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
motive : 𝔻 → Sort u_1
mk' : (z : ℂ) → (hz : ‖z‖ < 1) → motive (mk z hz)
z : ℂ
hz : ‖z‖ < 1
⊢ UnitDisc.casesOn (motive := fun (x : 𝔻) ↦ motive x) mk' (mk z hz) = mk' z hz

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, Complex.UnitDisc.casesOn, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ (↑(mk z hz) : ℂ) = z

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
hz : ‖(↑z : ℂ)‖ < 1
⊢ mk (↑z : ℂ) hz = z

Tactic:
Subtype.eta _ _

Premises used: Complex.UnitDisc, Complex.UnitDisc.coe, Subtype.eta, Complex.UnitDisc.mk
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z w : ℂ
hz : ‖z‖ < 1
hw : ‖w‖ < 1
⊢ mk z hz = mk w hw ↔ z = w

Tactic:
Subtype.mk_eq_mk

Premises used: Subtype.mk_eq_mk, Complex.UnitDisc, Complex.UnitDisc.mk
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
p : 𝔻 → Prop
⊢ (∀ (z : 𝔻), p z) ↔ ∀ (z : ℂ) (hz : ‖z‖ < 1), p (mk z hz)

Tactic:
⟨fun h z hz ↦ h (mk z hz), fun h z ↦ h z z.norm_lt_one⟩

Premises used: Iff.intro, Complex.UnitDisc.norm_lt_one, Complex.UnitDisc.coe, Complex.UnitDisc.mk
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
p : 𝔻 → Prop
⊢ (∃ (z : 𝔻), p z) ↔ ∃ (z : ℂ) (hz : ‖z‖ < 1), p (mk z hz)

Tactic:
⟨fun ⟨z, hz⟩ ↦ ⟨z, z.norm_lt_one, hz⟩, fun ⟨z, hz, h⟩ ↦ ⟨mk z hz, h⟩⟩

Premises used: Exists, _private.0.Complex.UnitDisc.exists.match_1, _private.0.Complex.UnitDisc.exists.match_2, Iff.intro, Exists.intro, Complex.UnitDisc.norm_lt_one, Complex.UnitDisc.coe, Complex.UnitDisc.mk
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : ℂ
hz : ‖-z‖ < 1
⊢ mk (-z) hz = -mk z ⋯

Tactic:
rfl

Premises used: Subtype.map, Set.Mem, setOf, Metric.ball, rfl, Complex.UnitDisc.mk
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ (↑0 : ℂ) = 0

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (↑z : ℂ) = 0 ↔ z = 0

Tactic:
coe_injective.eq_iff' coe_zero

Premises used: Function.Injective.eq_iff', Complex.UnitDisc.coe_injective, Complex.UnitDisc.coe_zero
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ norm (E := ℂ) 0 < 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ mk 0 mk_zero._proof_1 = 0

Tactic:
rfl

Premises used: Set.Mem, setOf, Metric.ball, rfl, Complex.UnitDisc.mk
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ mk z hz = 0 ↔ z = 0

Tactic:
simp [← coe_inj]

Premises used: Complex.UnitDisc.coe_inj
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ IsScalarTower Circle Circle 𝔻

Tactic:
inferInstanceAs <| IsScalarTower (sphere _ _) (sphere _ _) (ball _ _)

Premises used: _private.0.Complex.UnitDisc.instIsScalarTower_circle_circle._proof_1
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ IsScalarTower Circle 𝔻 𝔻

Tactic:
inferInstanceAs <| IsScalarTower (sphere _ _) (ball _ _) (ball _ _)

Premises used: _private.0.Complex.UnitDisc.instIsScalarTower_circle._proof_1
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ SMulCommClass Circle 𝔻 𝔻

Tactic:
inferInstanceAs <| SMulCommClass (sphere _ _) (ball _ _) (ball _ _)

Premises used: _private.0.Complex.UnitDisc.instSMulCommClass_circle_left._proof_1
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ SMulCommClass 𝔻 Circle 𝔻

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : Circle
w : 𝔻
⊢ (↑(z • w) : ℂ) = (↑z : ℂ) * (↑w : ℂ)

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ IsScalarTower (↑(closedBall 0 1) : Type) (↑(closedBall 0 1) : Type) 𝔻

Tactic:
inferInstanceAs <| IsScalarTower (closedBall _ _) (closedBall _ _) (ball _ _)

Premises used: _private.0.Complex.UnitDisc.instIsScalarTower_closedBall_closedBall._proof_1
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ IsScalarTower (↑(closedBall 0 1) : Type) 𝔻 𝔻

Tactic:
inferInstanceAs <| IsScalarTower (closedBall _ _) (ball _ _) (ball _ _)

Premises used: _private.0.Complex.UnitDisc.instIsScalarTower_closedBall._proof_1
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ SMulCommClass (↑(closedBall 0 1) : Type) 𝔻 𝔻

Tactic:
⟨fun _ _ _ => Subtype.ext <| mul_left_comm _ _ _⟩

Premises used: mul_left_comm, SMulCommClass.mk, Subtype.val, Subtype.ext
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ SMulCommClass 𝔻 (↑(closedBall 0 1) : Type) 𝔻

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ SMulCommClass Circle (↑(closedBall 0 1) : Type) 𝔻

Tactic:
inferInstanceAs <| SMulCommClass (sphere _ _) (closedBall _ _) (ball _ _)

Premises used: _private.0.Complex.UnitDisc.instSMulCommClass_circle_closedBall._proof_1
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ SMulCommClass (↑(closedBall 0 1) : Type) Circle 𝔻

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : (↑(closedBall 0 1) : Type)
w : 𝔻
⊢ (↑(z • w) : ℂ) = (↑z : ℂ) * (↑w : ℂ)

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
n : ℕ+
⊢ Membership.mem (γ := Subsemigroup ℂ) (Subsemigroup.unitBall ℂ) ((↑z : ℂ) ^ (↑n : ℕ))

Tactic:
simp [pow_lt_one_iff_of_nonneg, z.norm_lt_one]

Premises used: pow_lt_one_iff_of_nonneg, Complex.UnitDisc.norm_lt_one
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
n : ℕ+
⊢ (↑(z ^ n) : ℂ) = (↑z : ℂ) ^ (↑n : ℕ)

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
n : ℕ+
simp : Continuous (Y := ℂ) fun (x : 𝔻) ↦ (↑x : ℂ) ^ (↑n : ℕ)
⊢ Continuous (Y := 𝔻) fun (x : 𝔻) ↦ x ^ n

Tactic:
simp only [isEmbedding_coe.continuous_iff, Function.comp_def, coe_pow]

Premises used: Complex.UnitDisc.coe_pow, Complex.UnitDisc.isEmbedding_coe, Function.comp_def, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
n : ℕ+
⊢ Continuous (Y := ℂ) fun (x : 𝔻) ↦ (↑x : ℂ) ^ (↑n : ℕ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
n : ℕ+
rw : (↑z : ℂ) ^ (↑n : ℕ) = (↑0 : ℂ) ↔ z = 0
⊢ z ^ n = 0 ↔ z = 0

Tactic:
rw [← coe_inj, coe_pow]

Premises used: Complex.UnitDisc.coe_pow, Complex.UnitDisc.coe_inj
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
n : ℕ+
⊢ (↑z : ℂ) ^ (↑n : ℕ) = (↑0 : ℂ) ↔ z = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ HPow.hPow (β := ℕ+) z 1 = z

Tactic:
simp [← coe_inj]

Premises used: Complex.UnitDisc.coe_inj
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
simp : Tendsto (fun (x : ℕ+) ↦ (↑z : ℂ) ^ (↑x : ℕ)) atTop (𝓝 (↑0 : ℂ))
⊢ Tendsto (β := 𝔻) (fun (n : ℕ+) ↦ z ^ n) atTop (𝓝 0)

Tactic:
simp only [isEmbedding_coe.tendsto_nhds_iff, comp_def, coe_pow]

Premises used: Complex.UnitDisc.coe_pow, Complex.UnitDisc.isEmbedding_coe, Function.comp_def, Topology.IsEmbedding.tendsto_nhds_iff
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ Tendsto (fun (x : ℕ+) ↦ (↑z : ℂ) ^ (↑x : ℕ)) atTop (𝓝 (↑0 : ℂ))

Tactic:
tendsto_pow_atTop_nhds_zero_iff_norm_lt_one.mpr z.norm_lt_one
    |>.comp tendsto_PNat_val_atTop_atTop

Premises used: Iff.mpr, tendsto_PNat_val_atTop_atTop, tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, Complex.UnitDisc.norm_lt_one, Complex.UnitDisc.coe, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ Tendsto (fun (x : ℕ+) ↦ (↑z : ℂ) ^ (↑x : ℕ)) atTop (𝓝 (↑0 : ℂ))

Tactic:
exact tendsto_pow_atTop_nhds_zero_iff_norm_lt_one.mpr z.norm_lt_one
    |>.comp tendsto_PNat_val_atTop_atTop

Premises used: Iff.mpr, tendsto_PNat_val_atTop_atTop, tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, Complex.UnitDisc.norm_lt_one, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (↑z : ℂ).re = z.re

Tactic:
rfl

Premises used: Complex.UnitDisc.re, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (↑z : ℂ).im = z.im

Tactic:
rfl

Premises used: Complex.UnitDisc.im, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (-z).re = -z.re

Tactic:
rfl

Premises used: Complex.UnitDisc.re, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (-z).im = -z.im

Tactic:
rfl

Premises used: Complex.UnitDisc.im, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ re 0 = 0

Tactic:
rfl

Premises used: Complex.UnitDisc.re, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ im 0 = 0

Tactic:
rfl

Premises used: Complex.UnitDisc.im, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (↑(star z) : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ)

Tactic:
rfl

Premises used: Complex.UnitDisc.coe, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ star z = 0 ↔ z = 0

Tactic:
simp [← coe_eq_zero]

Premises used: Complex.UnitDisc.coe_eq_zero
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
⊢ Eq (α := 𝔻) (star 0) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
a : (↑(star (star z)) : ℂ) = (↑z : ℂ)
⊢ star (star z) = z

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (↑(star (star z)) : ℂ) = (↑z : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ star (star z) = z

Tactic:
star_star z

Premises used: star_star
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ star (-z) = -star z

Tactic:
rfl

Premises used: Subtype.map, Set.Mem, setOf, Metric.ball, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (star z).re = z.re

Tactic:
rfl

Premises used: Complex.UnitDisc.re, Complex.UnitDisc, rfl, Complex.UnitDisc.mk
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z : 𝔻
⊢ (star z).im = -z.im

Tactic:
rfl

Premises used: Complex.UnitDisc.im, rfl
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z w : 𝔻
⊢ (↑(star (z * w)) : ℂ) = (↑(star w * star z) : ℂ)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Complex.UnitDisc.Basic
Goal:
z w : 𝔻
⊢ star (z * w) = star z * star w

Tactic:
star_mul' z w

Premises used: star_mul'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ 0 < Complex.I.im

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ 0 < { re := -1 / 2, im := √3 / 2 : ℂ }.im

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
simp : -1 / 2 * (-1 / 2) - √3 / 2 * (√3 / 2) = -(-1 / 2) - 1 ∧ -1 / 2 * (√3 / 2) + √3 / 2 * (-1 / 2) = -(√3 / 2)
⊢ HPow.hPow (β := ℕ) (↑ρ : ℂ) 2 = -(↑ρ : ℂ) - 1

Tactic:
simp [Complex.ext_iff, pow_two, ρ]

Premises used: pow_two, UpperHalfPlane.ρ, Complex.ext_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ -1 / 2 * (-1 / 2) - √3 / 2 * (√3 / 2) = -(-1 / 2) - 1 ∧ -1 / 2 * (√3 / 2) + √3 / 2 * (-1 / 2) = -(√3 / 2)

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ ‖(↑ρ : ℂ)‖ = 1

Tactic:
norm_num [norm_def, normSq, ← pow_two, ρ, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, Complex.normSq, Complex.norm_def, div_pow
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
a b : ℍ
⊢ (↑a : ℂ) = (↑b : ℂ) ↔ a = b

Tactic:
UpperHalfPlane.ext_iff.symm

Premises used: UpperHalfPlane.ext_iff, Iff.symm
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ Function.Injective UpperHalfPlane.coe

Tactic:
fun _ _ ↦ UpperHalfPlane.ext

Premises used: Function.Injective, UpperHalfPlane.ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
P : ℍ → Prop
⊢ (∀ (z : ℍ), P z) ↔ ∀ (z : ℂ) (hz : 0 < z.im), P { coe := z, coe_im_pos := hz }

Tactic:
⟨fun h z hz ↦ h ⟨z, hz⟩, fun h z ↦ h z.1 z.2⟩

Premises used: UpperHalfPlane.coe, UpperHalfPlane.mk, Iff.intro, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
P : ℍ → Prop
⊢ (∃ (z : ℍ), P z) ↔ ∃ (z : ℂ) (hz : 0 < z.im), P { coe := z, coe_im_pos := hz }

Tactic:
⟨fun ⟨⟨z, hz⟩, hP⟩ ↦ ⟨z, hz, hP⟩, fun ⟨z, hz, hP⟩ ↦ ⟨⟨z, hz⟩, hP⟩⟩

Premises used: _private.0.UpperHalfPlane.exists.match_1, _private.0.UpperHalfPlane.exists.match_2, Exists, UpperHalfPlane.mk, Iff.intro, Exists.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
a b : ℍ
hre : a.re = b.re
him : a.im = b.im
⊢ a = b

Tactic:
UpperHalfPlane.ext <| Complex.ext hre him

Premises used: Complex.ext, UpperHalfPlane.ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ (↑z : ℂ).im = z.im

Tactic:
rfl

Premises used: UpperHalfPlane.im, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ (↑z : ℂ).re = z.re

Tactic:
rfl

Premises used: UpperHalfPlane.re, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℂ
h : 0 < z.im
⊢ { coe := z, coe_im_pos := h : ℍ }.re = z.re

Tactic:
rfl

Premises used: UpperHalfPlane.re, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℂ
h : 0 < z.im
⊢ { coe := z, coe_im_pos := h : ℍ }.im = z.im

Tactic:
rfl

Premises used: UpperHalfPlane.im, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℂ
h : 0 < z.im
⊢ (↑{ coe := z, coe_im_pos := h : ℍ } : ℂ) = z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
h : 0 < (↑z : ℂ).im
⊢ { coe := (↑z : ℂ), coe_im_pos := h : ℍ } = z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ I.im = 1

Tactic:
Complex.I_im

Premises used: Complex.I_im, UpperHalfPlane.im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ I.re = 0

Tactic:
Complex.I_re

Premises used: Complex.I_re, UpperHalfPlane.re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ (↑I : ℂ) = Complex.I

Tactic:
rfl

Premises used: rfl, Complex.I
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℂ
hz : 0 < z.im
⊢ (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) = z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ (↑z.re : ℂ) + (↑z.im : ℂ) * Complex.I = (↑z : ℂ)

Tactic:
Complex.re_add_im z

Premises used: UpperHalfPlane.coe, UpperHalfPlane.im, Complex.re_add_im, UpperHalfPlane.re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ 0 < z.im

Tactic:
z.coe_im_pos

Premises used: UpperHalfPlane.im, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ z.im ≠ 0

Tactic:
z.im_pos.ne'

Premises used: UpperHalfPlane.im_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ (↑z : ℂ) ≠ 0

Tactic:
mt (congr_arg Complex.im) z.im_ne_zero

Premises used: UpperHalfPlane.im_ne_zero, Complex.im, mt, congr_arg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ (↑z : ℂ) ∈ slitPlane

Tactic:
simp [Complex.slitPlane, im_ne_zero z]

Premises used: UpperHalfPlane.im_ne_zero, Complex.slitPlane
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
τ τ' : ℍ
hre : τ.re = τ'.re
hnorm : ‖(↑τ : ℂ)‖ = ‖(↑τ' : ℂ)‖
⊢ HPow.hPow (β := ℕ) ‖(↑τ : ℂ)‖ 2 = HPow.hPow (β := ℕ) ‖(↑τ' : ℂ)‖ 2

Tactic:
apply_fun (· ^ 2) at hnorm

Premises used: HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
τ τ' : ℍ
hre : τ.re = τ'.re
hnorm : HPow.hPow (β := ℕ) ‖(↑τ : ℂ)‖ 2 = HPow.hPow (β := ℕ) ‖(↑τ' : ℂ)‖ 2
⊢ τ = τ'

Tactic:
simpa [UpperHalfPlane.ext_iff, Complex.ext_iff, hre, Complex.normSq, Complex.sq_norm,
    ← pow_two, pow_left_inj₀ τ.im_pos.le τ'.im_pos.le two_ne_zero] using hnorm

Premises used: UpperHalfPlane.im_pos, pow_two, UpperHalfPlane.ext_iff, Complex.sq_norm, pow_left_inj₀, LT.lt.le, Complex.normSq, Complex.ext_iff, two_ne_zero