Decasting variables

Stream: new members

[Shadman Sakib]

How would I decast the x and pi in hn to match the goal, or opposingly, how can I cast the x and the pi to complex numbers in the goal to match hn?

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric

example {x : ℝ} (n : ℤ)
  (hn : (x : ℂ) = ↑n * (2 * ↑π)) :
  x = ↑n * (2 * π) :=
begin
  admit,
end

[Ruben Van de Velde]

  norm_cast at hn,
  exact hn,

gets you home

[Ruben Van de Velde]

Or

  rw [←complex.of_real_inj, hn],
  simp,

[Ruben Van de Velde]

With the least magic:

  rw [←complex.of_real_inj, hn],
  rw [complex.of_real_mul, complex.of_real_mul, complex.of_real_int_cast, complex.of_real_bit0, complex.of_real_one],

[Kevin Buzzard]

Does exact_mod_cast close the goal?

[Shadman Sakib]

Thank you so much, Ruben, for showing exactly how Lean carries out each step of your suggestion! And, yup, exact_mod_cast hn closes the goal!

[Yakov Pechersky]

You can even do assumption_mod_cast

[Shadman Sakib]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric

example (R : Type u_1) (n m : ℤ)
  [linear_ordered_ring R]
  (a : R)
  (h : a < 1)
  (h₀ : 0 < a)
  (n1 : 1 ≤ n) :
  a < ↑n :=
begin
  admit,
end

[Shadman Sakib]

How about this one? How do I avoid the casting problem that exact lt_of_lt_of_le h n1, gives?

[Kevin Buzzard]

import analysis.complex.circle
import group_theory.specific_groups.dihedral
import analysis.special_functions.trigonometric

example (R : Type*) (n m : ℤ)
  [linear_ordered_ring R]
  (a : R)
  (h : a < 1)
  (h₀ : 0 < a)
  (n1 : 1 ≤ n) :
  a < ↑n :=
begin
  refine lt_of_lt_of_le h _,
  assumption_mod_cast,
end

[Kevin Buzzard]

(PS you should check your mwes compile! That one didn't)

[Shadman Sakib]

Ah yes the Type*, I realized the error after I sent it. You are too quick! Thank you