awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ Subset (α := Set Circle) {x, y}
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))

Tactic:
simp only [pair_subset_iff,
      (path x y).source_mem_range, (path x y).target_mem_range, and_self]

Premises used: and_self, Set.pair_subset_iff, Path.source_mem_range, Path.target_mem_range, Circle.path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
refine_1 :
  ¬Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle)) univ
⊢ ¬Subset (α := Set Circle) {x, y}ᶜ
      (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle))

Tactic:
rw [compl_subset_iff_union, union_eq_right.mpr (by simp only [pair_subset_iff,
      (path x y).source_mem_range, (path x y).target_mem_range, and_self])]

Premises used: Iff.mpr, Set.compl_subset_iff_union, Set.union_eq_right
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ ¬Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle)) univ

Tactic:
(range_path_ssubset_univ x y).ne

Premises used: Circle.range_path_ssubset_univ, HasSSubset.SSubset.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ ¬Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle)) univ

Tactic:
exact (range_path_ssubset_univ x y).ne

Premises used: Circle.range_path_ssubset_univ, HasSSubset.SSubset.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
refine_2 : Subset (α := Set Circle) {x, y}ᶜ univ
⊢ Subset (α := Set Circle) {x, y}ᶜ
    (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) ∪
      range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))

Tactic:
rw [range_path_union_range_path hxy]

Premises used: Circle.range_path_union_range_path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ Subset (α := Set Circle) {x, y}ᶜ univ

Tactic:
subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ Subset (α := Set Circle) {x, y}ᶜ univ

Tactic:
exact subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
refine_3 : Eq (α := Set Circle) ({x, y}ᶜ ∩ {x, y}) ∅
⊢ Eq (α := Set Circle)
    ({x, y}ᶜ ∩
      (range (ι := (↑unitInterval : Type)) (⇑(x.path y) : (a : (↑unitInterval : Type)) → Circle) ∩
        range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle)))
    ∅

Tactic:
rw [range_path_inter_range_path hxy]

Premises used: Circle.range_path_inter_range_path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ Eq (α := Set Circle) ({x, y}ᶜ ∩ {x, y}) ∅

Tactic:
compl_inter_self {x, y}

Premises used: Insert.insert, Set.compl_inter_self, Singleton.singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ Eq (α := Set Circle) ({x, y}ᶜ ∩ {x, y}) ∅

Tactic:
exact compl_inter_self {x, y}

Premises used: Insert.insert, Set.compl_inter_self, Singleton.singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ Subset (α := Set Circle) {x, y}
    (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))

Tactic:
simp only [pair_subset_iff,
      (path y x).source_mem_range, (path y x).target_mem_range, and_self]

Premises used: and_self, Set.pair_subset_iff, Path.source_mem_range, Path.target_mem_range, Circle.path
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
refine_4 :
  ¬Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle)) univ
⊢ ¬Subset (α := Set Circle) {x, y}ᶜ
      (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle))

Tactic:
rw [compl_subset_iff_union, union_eq_right.mpr (by simp only [pair_subset_iff,
      (path y x).source_mem_range, (path y x).target_mem_range, and_self])]

Premises used: Iff.mpr, Set.compl_subset_iff_union, Set.union_eq_right
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ ¬Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle)) univ

Tactic:
(range_path_ssubset_univ y x).ne

Premises used: Circle.range_path_ssubset_univ, HasSSubset.SSubset.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x y : Circle
hxy : x ≠ y
⊢ ¬Eq (α := Set Circle) (range (ι := (↑unitInterval : Type)) (⇑(y.path x) : (a : (↑unitInterval : Type)) → Circle)) univ

Tactic:
exact (range_path_ssubset_univ y x).ne

Premises used: Circle.range_path_ssubset_univ, HasSSubset.SSubset.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
⊢ (↑x : Angle).toCircle = (Circle.exp : (a : ℝ) → Circle) x

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, Real.Angle.toCircle, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
θ : Angle
h : ∀ (x : ℝ), (↑(↑x : Angle).toCircle : ℂ) = (↑(↑x : Angle).cos : ℂ) + (↑(↑x : Angle).sin : ℂ) * I
⊢ (↑θ.toCircle : ℂ) = (↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I

Tactic:
induction θ using Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
⊢ (↑(↑x : Angle).toCircle : ℂ) = (↑(↑x : Angle).cos : ℂ) + (↑(↑x : Angle).sin : ℂ) * I

Tactic:
simp [exp_mul_I]

Premises used: Complex.exp_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
rw : (↑0 : Angle).toCircle = 1
rw₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
rw₂ rw₃ : Eq (α := Circle) 1 1
⊢ toCircle 0 = 1

Tactic:
rw [← coe_zero, toCircle_coe, Circle.exp_zero]

Premises used: Real.Angle.toCircle_coe, Circle.exp_zero, Real.Angle.coe_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
θ : Angle
h : ∀ (x : ℝ), (-(↑x : Angle)).toCircle = (↑x : Angle).toCircle⁻¹
⊢ (-θ).toCircle = θ.toCircle⁻¹

Tactic:
induction θ using Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
h : (↑(-x) : Angle).toCircle = (↑x : Angle).toCircle⁻¹
h₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (-x) : Circle) (((Circle.exp : (a : ℝ) → Circle) x)⁻¹ : Circle)
⊢ (-(↑x : Angle)).toCircle = (↑x : Angle).toCircle⁻¹

Tactic:
simp_rw [← coe_neg, toCircle_coe, Circle.exp_neg]

Premises used: Circle.exp_neg, Real.Angle.toCircle_coe, Real.Angle.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
θ₁ θ₂ : Angle
h : ∀ (x : ℝ), ((↑x : Angle) + θ₂).toCircle = (↑x : Angle).toCircle * θ₂.toCircle
⊢ (θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle

Tactic:
induction θ₁ using Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
θ₂ : Angle
x : ℝ
h : ∀ (x_1 : ℝ), ((↑x : Angle) + (↑x_1 : Angle)).toCircle = (↑x : Angle).toCircle * (↑x_1 : Angle).toCircle
⊢ ((↑x : Angle) + θ₂).toCircle = (↑x : Angle).toCircle * θ₂.toCircle

Tactic:
induction θ₂ using Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x x_1 : ℝ
⊢ ((↑x : Angle) + (↑x_1 : Angle)).toCircle = (↑x : Angle).toCircle * (↑x_1 : Angle).toCircle

Tactic:
Circle.exp_add _ _

Premises used: Quotient.liftOn', Function.Periodic.lift, Circle.exp_add, Real.Angle.toCircle
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x x_1 : ℝ
⊢ ((↑x : Angle) + (↑x_1 : Angle)).toCircle = (↑x : Angle).toCircle * (↑x_1 : Angle).toCircle

Tactic:
exact Circle.exp_add _ _

Premises used: Circle.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
θ : Angle
h : ∀ (x : ℝ), (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)
⊢ (↑(↑θ.toCircle : ℂ).arg : Angle) = θ

Tactic:
induction θ using Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
h : (↑(arg (↑((Circle.exp : (a : ℝ) → Circle) x) : ℂ)) : Angle) = (↑x : Angle)
h₁ : (↑(cexp ((↑x : ℂ) * I)).arg : Angle) = (↑x : Angle)
h₂ : (↑(Complex.cos (↑x : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₃ : (↑((↑(Real.cos x) : ℂ) + Complex.sin (↑x : ℂ) * I).arg : Angle) = (↑x : Angle)
h₄ : (↑((↑(Real.cos x) : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
h₅ : (↑((↑(↑x : Angle).cos : ℂ) + (↑(Real.sin x) : ℂ) * I).arg : Angle) = (↑x : Angle)
h₆ : (↑((↑(↑x : Angle).cos : ℂ) + (↑(↑x : Angle).sin : ℂ) * I).arg : Angle) = (↑x : Angle)
h₇ h₈ : (↑x : Angle) = (↑x : Angle)
⊢ (↑(↑(↑x : Angle).toCircle : ℂ).arg : Angle) = (↑x : Angle)

Tactic:
rw [toCircle_coe, Circle.coe_exp, exp_mul_I, ← ofReal_cos, ← ofReal_sin, ←
    Angle.cos_coe, ← Angle.sin_coe, arg_cos_add_sin_mul_I_coe_angle]

Premises used: Complex.arg_cos_add_sin_mul_I_coe_angle, Real.Angle.toCircle_coe, Real.Angle.sin_coe, Real.Angle.cos_coe, Complex.ofReal_cos, Complex.ofReal_sin, Circle.coe_exp, Complex.exp_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
inl : Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / 0 * x)) 0
inr : ∀ (hT : T ≠ 0), Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / T * x)) T
⊢ Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / T * x)) T

Tactic:
rcases eq_or_ne T 0 with (rfl | hT)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ Periodic (β := Circle) (fun (x : ℝ) ↦ (Circle.exp : (a : ℝ) → Circle) (2 * π / 0 * x)) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
x : ℝ
inr :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x + 2 * π / T * T) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
⊢ Eq (α := Circle) ((fun (x : ℝ) ↦ ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)) (x + T))
    ((fun (x : ℝ) ↦ ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)) x)

Tactic:
simp_rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
x : ℝ
inr :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x + 2 * π) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
inr₁ inr₂ :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)
⊢ Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x + 2 * π / T * T) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * x) : Circle)

Tactic:
rw [div_mul_cancel₀ _ hT, Circle.periodic_exp]

Premises used: Circle.periodic_exp, div_mul_cancel₀
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T x : ℝ
⊢ toCircle (T := T) (↑x : ℝ ⧸ AddSubgroup.zmultiples T) = (Circle.exp : (a : ℝ) → Circle) (2 * π / T * x)

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, AddCircle.toCircle, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x y : AddCircle T
H :
  ∀ (z : ℝ),
    ((↑z : ℝ ⧸ AddSubgroup.zmultiples T) + y).toCircle =
      toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * y.toCircle
⊢ (x + y).toCircle = x.toCircle * y.toCircle

Tactic:
induction x using QuotientAddGroup.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
y : AddCircle T
z : ℝ
H :
  ∀ (z_1 : ℝ),
    (HAdd.hAdd (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)).toCircle =
      toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ ((↑z : ℝ ⧸ AddSubgroup.zmultiples T) + y).toCircle =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * y.toCircle

Tactic:
induction y using QuotientAddGroup.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T z z_1 : ℝ
H :
  toCircle (T := T) (↑(z + z_1) : ℝ ⧸ AddSubgroup.zmultiples T) =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
H₁ :
  (Circle.exp : (a : ℝ) → Circle) (2 * π / T * (z + z_1)) =
    HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
      ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
H₂ :
  (Circle.exp : (a : ℝ) → Circle) (2 * π / T * z + 2 * π / T * z_1) =
    HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
      ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
⊢ (HAdd.hAdd (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)).toCircle =
    toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) * toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)

Tactic:
simp_rw [← coe_add, toCircle_apply_mk, mul_add, Circle.exp_add]

Premises used: Circle.exp_add, AddCircle.toCircle_apply_mk, mul_add, AddCircle.coe_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
rw : toCircle (T := T) (↑0 : ℝ ⧸ AddSubgroup.zmultiples T) = 1
rw₁ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * 0) : Circle) (1 : Circle)
rw₂ : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
rw₃ rw₄ : Eq (α := Circle) 1 1
⊢ toCircle (T := T) 0 = 1

Tactic:
rw [← QuotientAddGroup.mk_zero, toCircle_apply_mk, mul_zero, Circle.exp_zero]

Premises used: MulZeroClass.mul_zero, AddCircle.toCircle_apply_mk, QuotientAddGroup.mk_zero, Circle.exp_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : AddCircle T
⊢ (-x).toCircle * x.toCircle = x.toCircle⁻¹ * x.toCircle

Tactic:
simp [← toCircle_add]

Premises used: AddCircle.toCircle_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : AddCircle T
⊢ (HSMul.hSMul (α := ℕ) 0 x).toCircle = HPow.hPow (β := ℕ) x.toCircle 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : AddCircle T
n : ℕ
ih : (n • x).toCircle = x.toCircle ^ n
succ : (n • x + x).toCircle = x.toCircle ^ (n + 1)
succ₁ : (n • x).toCircle * x.toCircle = x.toCircle ^ (n + 1)
succ₂ : x.toCircle ^ n * x.toCircle = x.toCircle ^ (n + 1)
succ₃ succ₄ : x.toCircle ^ n * x.toCircle = x.toCircle ^ n * x.toCircle
⊢ ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)

Tactic:
rw [succ_nsmul, toCircle_add, ih, pow_succ]

Premises used: AddCircle.toCircle_add, pow_succ, succ_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : AddCircle T
n : ℕ
zero : (HSMul.hSMul (α := ℕ) 0 x).toCircle = HPow.hPow (β := ℕ) x.toCircle 0
succ : ∀ (n : ℕ) (ih : (n • x).toCircle = x.toCircle ^ n), ((n + 1) • x).toCircle = x.toCircle ^ (n + 1)
⊢ (n • x).toCircle = x.toCircle ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [succ_nsmul, toCircle_add, ih, pow_succ]

Premises used: AddCircle.toCircle_add, pow_succ, succ_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : AddCircle T
n : ℤ
ofNat : ∀ (a : ℕ), (Int.ofNat a • x).toCircle = x.toCircle ^ Int.ofNat a
negSucc : ∀ (a : ℕ), (Int.negSucc a • x).toCircle = x.toCircle ^ Int.negSucc a
⊢ (n • x).toCircle = x.toCircle ^ n

Tactic:
cases n
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : AddCircle T
a : ℕ
⊢ (Int.ofNat a • x).toCircle = x.toCircle ^ Int.ofNat a

Tactic:
simp [toCircle_nsmul, toCircle_neg]

Premises used: AddCircle.toCircle_nsmul, AddCircle.toCircle_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : AddCircle T
a : ℕ
⊢ (Int.negSucc a • x).toCircle = x.toCircle ^ Int.negSucc a

Tactic:
simp [toCircle_nsmul, toCircle_neg]

Premises used: AddCircle.toCircle_nsmul, AddCircle.toCircle_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
⊢ Continuous (X := ℝ) (HMul.hMul (2 * π / T))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
a b : AddCircle T
h : a.toCircle = b.toCircle
H :
  ∀ (z : ℝ) (h : toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = b.toCircle),
    (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = b
⊢ a = b

Tactic:
induction a using QuotientAddGroup.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
b : AddCircle T
z : ℝ
h : toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = b.toCircle
H :
  ∀ (z_1 : ℝ)
    (h :
      toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = toCircle (T := T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)),
    Eq (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ (↑z : ℝ ⧸ AddSubgroup.zmultiples T) = b

Tactic:
induction b using QuotientAddGroup.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
H :
  ∀ (m : ℤ) (hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)),
    Eq (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ Eq (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)

Tactic:
obtain ⟨m, hm⟩ := Circle.exp_eq_exp.mp h.symm

Premises used: Circle.exp_eq_exp, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)
H : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples T) (-z + z_1)
⊢ Eq (α := AddCircle T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) (↑z_1 : ℝ ⧸ AddSubgroup.zmultiples T)

Tactic:
rw [QuotientAddGroup.eq]

Premises used: QuotientAddGroup.eq
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)
H : ∃ (k : ℤ), (↑k : ℝ) * T = -z + z_1
⊢ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples T) (-z + z_1)

Tactic:
simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul]

Premises used: zsmul_eq_mul, AddSubgroup.mem_zmultiples_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)
h₁ : (↑m : ℝ) * T = -z + z_1
⊢ ∃ (k : ℤ), (↑k : ℝ) * T = -z + z_1

Tactic:
use m
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : 2 * π / T * z_1 = 2 * π / T * z + (↑m : ℝ) * (2 * π)
⊢ z_1 = z + T * (↑m : ℝ)

Tactic:
field_simp at hm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
z z_1 : ℝ
h :
  Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z_1) : Circle)
m : ℤ
hm : z_1 = z + T * (↑m : ℝ)
linarith : (↑m : ℝ) * T < -z + z_1 → z_1 - (z + T * (↑m : ℝ)) + ((↑m : ℝ) * T - (-z + z_1)) = 0
linarith₁ : -z + z_1 < (↑m : ℝ) * T → -(z_1 - (z + T * (↑m : ℝ))) + (-z + z_1 - (↑m : ℝ) * T) = 0
⊢ (↑m : ℝ) * T = -z + z_1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
rw :
  ∀ (x : Circle),
    ContinuousAt (Y := AddCircle (2 * π)) (fun (x : Circle) ↦ (↑(↑x : ℂ).arg : ℝ ⧸ AddSubgroup.zmultiples (2 * π))) x
⊢ Continuous (Y := AddCircle (2 * π)) fun (x : Circle) ↦ (↑(↑x : ℂ).arg : ℝ ⧸ AddSubgroup.zmultiples (2 * π))

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : Circle
⊢ ContinuousAt (Y := AddCircle (2 * π)) (fun (x : Circle) ↦ (↑(↑x : ℂ).arg : ℝ ⧸ AddSubgroup.zmultiples (2 * π))) x

Tactic:
(continuousAt_arg_coe_angle x.coe_ne_zero).comp continuousAt_subtype_val

Premises used: Real.Angle, Real.Angle.coe, continuousAt_subtype_val, Complex.continuousAt_arg_coe_angle, Circle.coe_ne_zero, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
x : Circle
⊢ ContinuousAt (Y := AddCircle (2 * π)) (fun (x : Circle) ↦ (↑(↑x : ℂ).arg : ℝ ⧸ AddSubgroup.zmultiples (2 * π))) x

Tactic:
exact (continuousAt_arg_coe_angle x.coe_ne_zero).comp continuousAt_subtype_val

Premises used: continuousAt_subtype_val, Complex.continuousAt_arg_coe_angle, Circle.coe_ne_zero, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
x : ℝ
⊢ Eq (α := Circle)
    ((homeomorphCircle' : (a : AddCircle (2 * π)) → Circle) (↑x : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) x : Circle)

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, Real.Angle.toCircle, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
⊢ 2 * π ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
x : AddCircle T
H :
  ∀ (z : ℝ),
    (homeomorphCircle hT : (a : AddCircle T) → Circle) (↑z : ℝ ⧸ AddSubgroup.zmultiples T) =
      toCircle (T := T) (↑z : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ (homeomorphCircle hT : (a : AddCircle T) → Circle) x = x.toCircle

Tactic:
cases x using QuotientAddGroup.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
T : ℝ
hT : T ≠ 0
z : ℝ
⊢ Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (z * (T⁻¹ * (2 * π))) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π / T * z) : Circle)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ IsAddQuotientCoveringMap (E := ℝ) (X := Circle)
    (comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
      (⇑(homeomorphCircle ⋯) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk)
    ↥(AddSubgroup.zmultiples (2 * π))

Tactic:
(isAddQuotientCoveringMap_coe _).homeomorph_comp (homeomorphCircle _)

Premises used: AddCircle.homeomorphCircle, IsAddQuotientCoveringMap.homeomorph_comp, AddCircle.isAddQuotientCoveringMap_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
h :
  Eq (α := ℝ → Circle) (⇑exp : (a : ℝ) → Circle)
    (comp (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
      (⇑(homeomorphCircle ⋯) : (a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) → Circle) QuotientAddGroup.mk)
convert_2 : 2 * π ≠ 0
⊢ IsAddQuotientCoveringMap (E := ℝ) (X := Circle) (⇑exp : (a : ℝ) → Circle) ↥(AddSubgroup.zmultiples (2 * π))

Tactic:
convert! (isAddQuotientCoveringMap_coe _).homeomorph_comp (homeomorphCircle _)

Premises used: AddCircle.homeomorphCircle, IsAddQuotientCoveringMap.homeomorph_comp, AddCircle.isAddQuotientCoveringMap_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ 2 * π ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle
Goal:
⊢ 2 * π ≠ 0

Tactic:
on_goal 2 => simp