θ ψ : Angle
h : toReal θ = toReal ψ
⊢ θ = ψ
⊢ Function.Injective toReal
intro θ ψ h
case h
ψ : Angle
x✝ : ℝ
h : toReal ↑x✝ = toReal ψ
⊢ ↑x✝ = ψ
θ ψ : Angle
h : toReal θ = toReal ψ
⊢ θ = ψ
induction θ using Real.Angle.induction_on
case h.h
x✝¹ x✝ : ℝ
h : toReal ↑x✝¹ = toReal ↑x✝
⊢ ↑x✝¹ = ↑x✝
case h
ψ : Angle
x✝ : ℝ
h : toReal ↑x✝ = toReal ψ
⊢ ↑x✝ = ψ
induction ψ using Real.Angle.induction_on
no goals
case h.h
x✝¹ x✝ : ℝ
h : toReal ↑x✝¹ = toReal ↑x✝
⊢ ↑x✝¹ = ↑x✝
simpa [toReal_coe, toIocMod_eq_toIocMod, zsmul_eq_mul, mul_comm _ (2 * π), ←
  angle_eq_iff_two_pi_dvd_sub, eq_comm] using h