-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
theorem injective_toCircle (hT : T ≠ 0) : Function.Injective (@toCircle T)

Proof state:
T : ℝ
hT : T ≠ 0
a b : AddCircle T
h : a.toCircle = b.toCircle
⊢ a = b

Tactic:
induction a using QuotientAddGroup.induction_on

Result:
case H
T : ℝ
hT : T ≠ 0
b : AddCircle T
z✝ : ℝ
h : toCircle ↑z✝ = b.toCircle
⊢ ↑z✝ = b

Proof state:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : toCircle ↑z✝¹ = toCircle ↑z✝
⊢ ↑z✝¹ = ↑z✝

Tactic:
simp_rw [toCircle_apply_mk] at h

Result:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
⊢ ↑z✝¹ = ↑z✝

Proof state:
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ↑z✝¹ = ↑z✝

Tactic:
rw [QuotientAddGroup.eq]

Result:
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ -z✝¹ + z✝ ∈ AddSubgroup.zmultiples T

Proof state:
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ↑m * T = -z✝¹ + z✝

Tactic:
field_simp at hm

Result:
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π * z✝ = 2 * π * z✝¹ + ↑m * (2 * π) * T
⊢ ↑m * T = -z✝¹ + z✝

Proof state:
case H
T : ℝ
hT : T ≠ 0
b : AddCircle T
z✝ : ℝ
h : toCircle ↑z✝ = b.toCircle
⊢ ↑z✝ = b

Tactic:
induction b using QuotientAddGroup.induction_on

Result:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : toCircle ↑z✝¹ = toCircle ↑z✝
⊢ ↑z✝¹ = ↑z✝

Proof state:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
⊢ ↑z✝¹ = ↑z✝

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

Result:
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ↑z✝¹ = ↑z✝

Proof state:
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π * z✝ = 2 * π * z✝¹ + ↑m * (2 * π) * T
⊢ ↑m * T = -z✝¹ + z✝

Tactic:
rw [← mul_right_inj' Real.two_pi_pos.ne']

Result:
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π * z✝ = 2 * π * z✝¹ + ↑m * (2 * π) * T
⊢ 2 * π * (↑m * T) = 2 * π * (-z✝¹ + z✝)

Proof state:
T : ℝ
hT : T ≠ 0
⊢ Injective toCircle

Tactic:
intro a b h

Result:
T : ℝ
hT : T ≠ 0
a b : AddCircle T
h : a.toCircle = b.toCircle
⊢ a = b

Proof state:
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ -z✝¹ + z✝ ∈ AddSubgroup.zmultiples T

Tactic:
simp_rw [AddSubgroup.mem_zmultiples_iff, zsmul_eq_mul]

Result:
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ∃ k, ↑k * T = -z✝¹ + z✝

Proof state:
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π * z✝ = 2 * π * z✝¹ + ↑m * (2 * π) * T
⊢ 2 * π * (↑m * T) = 2 * π * (-z✝¹ + z✝)

Tactic:
linarith

Result:
no goals

Proof state:
case H.H.intro
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ∃ k, ↑k * T = -z✝¹ + z✝

Tactic:
use m

Result:
case h
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ↑m * T = -z✝¹ + z✝